Proof of Theorem ispsubcl2N
Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . 3
⊢
(Atoms‘𝐾) =
(Atoms‘𝐾) |
2 | | eqid 2622 |
. . 3
⊢
(⊥𝑃‘𝐾) = (⊥𝑃‘𝐾) |
3 | | pmapsubcl.c |
. . 3
⊢ 𝐶 = (PSubCl‘𝐾) |
4 | 1, 2, 3 | ispsubclN 35223 |
. 2
⊢ (𝐾 ∈ HL → (𝑋 ∈ 𝐶 ↔ (𝑋 ⊆ (Atoms‘𝐾) ∧
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋))) |
5 | | hlop 34649 |
. . . . . . . . 9
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) |
6 | 5 | adantr 481 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ (Atoms‘𝐾)) → 𝐾 ∈ OP) |
7 | | hlclat 34645 |
. . . . . . . . . 10
⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat) |
8 | 7 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ (Atoms‘𝐾)) → 𝐾 ∈ CLat) |
9 | 1, 2 | polssatN 35194 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ (Atoms‘𝐾)) →
((⊥𝑃‘𝐾)‘𝑋) ⊆ (Atoms‘𝐾)) |
10 | | pmapsubcl.b |
. . . . . . . . . . 11
⊢ 𝐵 = (Base‘𝐾) |
11 | 10, 1 | atssbase 34577 |
. . . . . . . . . 10
⊢
(Atoms‘𝐾)
⊆ 𝐵 |
12 | 9, 11 | syl6ss 3615 |
. . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ (Atoms‘𝐾)) →
((⊥𝑃‘𝐾)‘𝑋) ⊆ 𝐵) |
13 | | eqid 2622 |
. . . . . . . . . 10
⊢
(lub‘𝐾) =
(lub‘𝐾) |
14 | 10, 13 | clatlubcl 17112 |
. . . . . . . . 9
⊢ ((𝐾 ∈ CLat ∧
((⊥𝑃‘𝐾)‘𝑋) ⊆ 𝐵) → ((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) ∈ 𝐵) |
15 | 8, 12, 14 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ (Atoms‘𝐾)) → ((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) ∈ 𝐵) |
16 | | eqid 2622 |
. . . . . . . . 9
⊢
(oc‘𝐾) =
(oc‘𝐾) |
17 | 10, 16 | opoccl 34481 |
. . . . . . . 8
⊢ ((𝐾 ∈ OP ∧
((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) ∈ 𝐵) → ((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))) ∈ 𝐵) |
18 | 6, 15, 17 | syl2anc 693 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ (Atoms‘𝐾)) → ((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))) ∈ 𝐵) |
19 | 18 | ex 450 |
. . . . . 6
⊢ (𝐾 ∈ HL → (𝑋 ⊆ (Atoms‘𝐾) → ((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))) ∈ 𝐵)) |
20 | 19 | adantrd 484 |
. . . . 5
⊢ (𝐾 ∈ HL → ((𝑋 ⊆ (Atoms‘𝐾) ∧
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋) → ((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))) ∈ 𝐵)) |
21 | | pmapsubcl.m |
. . . . . . . . . 10
⊢ 𝑀 = (pmap‘𝐾) |
22 | 13, 16, 1, 21, 2 | polval2N 35192 |
. . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧
((⊥𝑃‘𝐾)‘𝑋) ⊆ (Atoms‘𝐾)) →
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))))) |
23 | 9, 22 | syldan 487 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ (Atoms‘𝐾)) →
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))))) |
24 | 23 | ex 450 |
. . . . . . 7
⊢ (𝐾 ∈ HL → (𝑋 ⊆ (Atoms‘𝐾) →
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)))))) |
25 | | eqeq1 2626 |
. . . . . . . 8
⊢
(((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋 →
(((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)))) ↔ 𝑋 = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)))))) |
26 | 25 | biimpcd 239 |
. . . . . . 7
⊢
(((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)))) →
(((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋 → 𝑋 = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)))))) |
27 | 24, 26 | syl6 35 |
. . . . . 6
⊢ (𝐾 ∈ HL → (𝑋 ⊆ (Atoms‘𝐾) →
(((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋 → 𝑋 = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))))))) |
28 | 27 | impd 447 |
. . . . 5
⊢ (𝐾 ∈ HL → ((𝑋 ⊆ (Atoms‘𝐾) ∧
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋) → 𝑋 = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)))))) |
29 | 20, 28 | jcad 555 |
. . . 4
⊢ (𝐾 ∈ HL → ((𝑋 ⊆ (Atoms‘𝐾) ∧
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋) → (((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))) ∈ 𝐵 ∧ 𝑋 = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))))))) |
30 | | fveq2 6191 |
. . . . . 6
⊢ (𝑦 = ((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))) → (𝑀‘𝑦) = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))))) |
31 | 30 | eqeq2d 2632 |
. . . . 5
⊢ (𝑦 = ((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))) → (𝑋 = (𝑀‘𝑦) ↔ 𝑋 = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)))))) |
32 | 31 | rspcev 3309 |
. . . 4
⊢
((((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))) ∈ 𝐵 ∧ 𝑋 = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))))) → ∃𝑦 ∈ 𝐵 𝑋 = (𝑀‘𝑦)) |
33 | 29, 32 | syl6 35 |
. . 3
⊢ (𝐾 ∈ HL → ((𝑋 ⊆ (Atoms‘𝐾) ∧
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋) → ∃𝑦 ∈ 𝐵 𝑋 = (𝑀‘𝑦))) |
34 | 10, 1, 21 | pmapssat 35045 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑦 ∈ 𝐵) → (𝑀‘𝑦) ⊆ (Atoms‘𝐾)) |
35 | 10, 21, 2 | 2polpmapN 35199 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑦 ∈ 𝐵) →
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘(𝑀‘𝑦))) = (𝑀‘𝑦)) |
36 | | sseq1 3626 |
. . . . . . 7
⊢ (𝑋 = (𝑀‘𝑦) → (𝑋 ⊆ (Atoms‘𝐾) ↔ (𝑀‘𝑦) ⊆ (Atoms‘𝐾))) |
37 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑋 = (𝑀‘𝑦) →
((⊥𝑃‘𝐾)‘𝑋) =
((⊥𝑃‘𝐾)‘(𝑀‘𝑦))) |
38 | 37 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑋 = (𝑀‘𝑦) →
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = ((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘(𝑀‘𝑦)))) |
39 | | id 22 |
. . . . . . . 8
⊢ (𝑋 = (𝑀‘𝑦) → 𝑋 = (𝑀‘𝑦)) |
40 | 38, 39 | eqeq12d 2637 |
. . . . . . 7
⊢ (𝑋 = (𝑀‘𝑦) →
(((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋 ↔ ((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘(𝑀‘𝑦))) = (𝑀‘𝑦))) |
41 | 36, 40 | anbi12d 747 |
. . . . . 6
⊢ (𝑋 = (𝑀‘𝑦) → ((𝑋 ⊆ (Atoms‘𝐾) ∧
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋) ↔ ((𝑀‘𝑦) ⊆ (Atoms‘𝐾) ∧ ((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘(𝑀‘𝑦))) = (𝑀‘𝑦)))) |
42 | 41 | biimprcd 240 |
. . . . 5
⊢ (((𝑀‘𝑦) ⊆ (Atoms‘𝐾) ∧
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘(𝑀‘𝑦))) = (𝑀‘𝑦)) → (𝑋 = (𝑀‘𝑦) → (𝑋 ⊆ (Atoms‘𝐾) ∧ ((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋))) |
43 | 34, 35, 42 | syl2anc 693 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑦 ∈ 𝐵) → (𝑋 = (𝑀‘𝑦) → (𝑋 ⊆ (Atoms‘𝐾) ∧
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋))) |
44 | 43 | rexlimdva 3031 |
. . 3
⊢ (𝐾 ∈ HL → (∃𝑦 ∈ 𝐵 𝑋 = (𝑀‘𝑦) → (𝑋 ⊆ (Atoms‘𝐾) ∧
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋))) |
45 | 33, 44 | impbid 202 |
. 2
⊢ (𝐾 ∈ HL → ((𝑋 ⊆ (Atoms‘𝐾) ∧
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋) ↔ ∃𝑦 ∈ 𝐵 𝑋 = (𝑀‘𝑦))) |
46 | 4, 45 | bitrd 268 |
1
⊢ (𝐾 ∈ HL → (𝑋 ∈ 𝐶 ↔ ∃𝑦 ∈ 𝐵 𝑋 = (𝑀‘𝑦))) |