Proof of Theorem ispsubcl2N
Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . 3
⊢
(Atoms‘𝐾) =
(Atoms‘𝐾) |
2 | | eqid 2738 |
. . 3
⊢
(⊥𝑃‘𝐾) = (⊥𝑃‘𝐾) |
3 | | pmapsubcl.c |
. . 3
⊢ 𝐶 = (PSubCl‘𝐾) |
4 | 1, 2, 3 | ispsubclN 37951 |
. 2
⊢ (𝐾 ∈ HL → (𝑋 ∈ 𝐶 ↔ (𝑋 ⊆ (Atoms‘𝐾) ∧
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋))) |
5 | | hlop 37376 |
. . . . . . . . 9
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) |
6 | 5 | adantr 481 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ (Atoms‘𝐾)) → 𝐾 ∈ OP) |
7 | | hlclat 37372 |
. . . . . . . . . 10
⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat) |
8 | 7 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ (Atoms‘𝐾)) → 𝐾 ∈ CLat) |
9 | 1, 2 | polssatN 37922 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ (Atoms‘𝐾)) →
((⊥𝑃‘𝐾)‘𝑋) ⊆ (Atoms‘𝐾)) |
10 | | pmapsubcl.b |
. . . . . . . . . . 11
⊢ 𝐵 = (Base‘𝐾) |
11 | 10, 1 | atssbase 37304 |
. . . . . . . . . 10
⊢
(Atoms‘𝐾)
⊆ 𝐵 |
12 | 9, 11 | sstrdi 3933 |
. . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ (Atoms‘𝐾)) →
((⊥𝑃‘𝐾)‘𝑋) ⊆ 𝐵) |
13 | | eqid 2738 |
. . . . . . . . . 10
⊢
(lub‘𝐾) =
(lub‘𝐾) |
14 | 10, 13 | clatlubcl 18221 |
. . . . . . . . 9
⊢ ((𝐾 ∈ CLat ∧
((⊥𝑃‘𝐾)‘𝑋) ⊆ 𝐵) → ((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) ∈ 𝐵) |
15 | 8, 12, 14 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ (Atoms‘𝐾)) → ((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) ∈ 𝐵) |
16 | | eqid 2738 |
. . . . . . . . 9
⊢
(oc‘𝐾) =
(oc‘𝐾) |
17 | 10, 16 | opoccl 37208 |
. . . . . . . 8
⊢ ((𝐾 ∈ OP ∧
((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) ∈ 𝐵) → ((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))) ∈ 𝐵) |
18 | 6, 15, 17 | syl2anc 584 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ (Atoms‘𝐾)) → ((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))) ∈ 𝐵) |
19 | 18 | ex 413 |
. . . . . 6
⊢ (𝐾 ∈ HL → (𝑋 ⊆ (Atoms‘𝐾) → ((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))) ∈ 𝐵)) |
20 | 19 | adantrd 492 |
. . . . 5
⊢ (𝐾 ∈ HL → ((𝑋 ⊆ (Atoms‘𝐾) ∧
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋) → ((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))) ∈ 𝐵)) |
21 | | pmapsubcl.m |
. . . . . . . . . 10
⊢ 𝑀 = (pmap‘𝐾) |
22 | 13, 16, 1, 21, 2 | polval2N 37920 |
. . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧
((⊥𝑃‘𝐾)‘𝑋) ⊆ (Atoms‘𝐾)) →
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))))) |
23 | 9, 22 | syldan 591 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ (Atoms‘𝐾)) →
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))))) |
24 | 23 | ex 413 |
. . . . . . 7
⊢ (𝐾 ∈ HL → (𝑋 ⊆ (Atoms‘𝐾) →
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)))))) |
25 | | eqeq1 2742 |
. . . . . . . 8
⊢
(((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋 →
(((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)))) ↔ 𝑋 = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)))))) |
26 | 25 | biimpcd 248 |
. . . . . . 7
⊢
(((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)))) →
(((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋 → 𝑋 = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)))))) |
27 | 24, 26 | syl6 35 |
. . . . . 6
⊢ (𝐾 ∈ HL → (𝑋 ⊆ (Atoms‘𝐾) →
(((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋 → 𝑋 = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))))))) |
28 | 27 | impd 411 |
. . . . 5
⊢ (𝐾 ∈ HL → ((𝑋 ⊆ (Atoms‘𝐾) ∧
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋) → 𝑋 = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)))))) |
29 | 20, 28 | jcad 513 |
. . . 4
⊢ (𝐾 ∈ HL → ((𝑋 ⊆ (Atoms‘𝐾) ∧
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋) → (((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))) ∈ 𝐵 ∧ 𝑋 = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))))))) |
30 | | fveq2 6774 |
. . . . 5
⊢ (𝑦 = ((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))) → (𝑀‘𝑦) = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))))) |
31 | 30 | rspceeqv 3575 |
. . . 4
⊢
((((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))) ∈ 𝐵 ∧ 𝑋 = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))))) → ∃𝑦 ∈ 𝐵 𝑋 = (𝑀‘𝑦)) |
32 | 29, 31 | syl6 35 |
. . 3
⊢ (𝐾 ∈ HL → ((𝑋 ⊆ (Atoms‘𝐾) ∧
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋) → ∃𝑦 ∈ 𝐵 𝑋 = (𝑀‘𝑦))) |
33 | 10, 1, 21 | pmapssat 37773 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑦 ∈ 𝐵) → (𝑀‘𝑦) ⊆ (Atoms‘𝐾)) |
34 | 10, 21, 2 | 2polpmapN 37927 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑦 ∈ 𝐵) →
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘(𝑀‘𝑦))) = (𝑀‘𝑦)) |
35 | | sseq1 3946 |
. . . . . . 7
⊢ (𝑋 = (𝑀‘𝑦) → (𝑋 ⊆ (Atoms‘𝐾) ↔ (𝑀‘𝑦) ⊆ (Atoms‘𝐾))) |
36 | | 2fveq3 6779 |
. . . . . . . 8
⊢ (𝑋 = (𝑀‘𝑦) →
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = ((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘(𝑀‘𝑦)))) |
37 | | id 22 |
. . . . . . . 8
⊢ (𝑋 = (𝑀‘𝑦) → 𝑋 = (𝑀‘𝑦)) |
38 | 36, 37 | eqeq12d 2754 |
. . . . . . 7
⊢ (𝑋 = (𝑀‘𝑦) →
(((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋 ↔ ((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘(𝑀‘𝑦))) = (𝑀‘𝑦))) |
39 | 35, 38 | anbi12d 631 |
. . . . . 6
⊢ (𝑋 = (𝑀‘𝑦) → ((𝑋 ⊆ (Atoms‘𝐾) ∧
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋) ↔ ((𝑀‘𝑦) ⊆ (Atoms‘𝐾) ∧ ((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘(𝑀‘𝑦))) = (𝑀‘𝑦)))) |
40 | 39 | biimprcd 249 |
. . . . 5
⊢ (((𝑀‘𝑦) ⊆ (Atoms‘𝐾) ∧
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘(𝑀‘𝑦))) = (𝑀‘𝑦)) → (𝑋 = (𝑀‘𝑦) → (𝑋 ⊆ (Atoms‘𝐾) ∧ ((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋))) |
41 | 33, 34, 40 | syl2anc 584 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑦 ∈ 𝐵) → (𝑋 = (𝑀‘𝑦) → (𝑋 ⊆ (Atoms‘𝐾) ∧
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋))) |
42 | 41 | rexlimdva 3213 |
. . 3
⊢ (𝐾 ∈ HL → (∃𝑦 ∈ 𝐵 𝑋 = (𝑀‘𝑦) → (𝑋 ⊆ (Atoms‘𝐾) ∧
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋))) |
43 | 32, 42 | impbid 211 |
. 2
⊢ (𝐾 ∈ HL → ((𝑋 ⊆ (Atoms‘𝐾) ∧
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋) ↔ ∃𝑦 ∈ 𝐵 𝑋 = (𝑀‘𝑦))) |
44 | 4, 43 | bitrd 278 |
1
⊢ (𝐾 ∈ HL → (𝑋 ∈ 𝐶 ↔ ∃𝑦 ∈ 𝐵 𝑋 = (𝑀‘𝑦))) |