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 37574 |
. 2
⊢ (𝐾 ∈ HL → (𝑋 ∈ 𝐶 ↔ (𝑋 ⊆ (Atoms‘𝐾) ∧
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋))) |
5 | | hlop 36999 |
. . . . . . . . 9
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) |
6 | 5 | adantr 484 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ (Atoms‘𝐾)) → 𝐾 ∈ OP) |
7 | | hlclat 36995 |
. . . . . . . . . 10
⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat) |
8 | 7 | adantr 484 |
. . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ (Atoms‘𝐾)) → 𝐾 ∈ CLat) |
9 | 1, 2 | polssatN 37545 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ (Atoms‘𝐾)) →
((⊥𝑃‘𝐾)‘𝑋) ⊆ (Atoms‘𝐾)) |
10 | | pmapsubcl.b |
. . . . . . . . . . 11
⊢ 𝐵 = (Base‘𝐾) |
11 | 10, 1 | atssbase 36927 |
. . . . . . . . . 10
⊢
(Atoms‘𝐾)
⊆ 𝐵 |
12 | 9, 11 | sstrdi 3889 |
. . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ (Atoms‘𝐾)) →
((⊥𝑃‘𝐾)‘𝑋) ⊆ 𝐵) |
13 | | eqid 2738 |
. . . . . . . . . 10
⊢
(lub‘𝐾) =
(lub‘𝐾) |
14 | 10, 13 | clatlubcl 17838 |
. . . . . . . . 9
⊢ ((𝐾 ∈ CLat ∧
((⊥𝑃‘𝐾)‘𝑋) ⊆ 𝐵) → ((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) ∈ 𝐵) |
15 | 8, 12, 14 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ (Atoms‘𝐾)) → ((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) ∈ 𝐵) |
16 | | eqid 2738 |
. . . . . . . . 9
⊢
(oc‘𝐾) =
(oc‘𝐾) |
17 | 10, 16 | opoccl 36831 |
. . . . . . . 8
⊢ ((𝐾 ∈ OP ∧
((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) ∈ 𝐵) → ((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))) ∈ 𝐵) |
18 | 6, 15, 17 | syl2anc 587 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ (Atoms‘𝐾)) → ((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))) ∈ 𝐵) |
19 | 18 | ex 416 |
. . . . . 6
⊢ (𝐾 ∈ HL → (𝑋 ⊆ (Atoms‘𝐾) → ((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))) ∈ 𝐵)) |
20 | 19 | adantrd 495 |
. . . . 5
⊢ (𝐾 ∈ HL → ((𝑋 ⊆ (Atoms‘𝐾) ∧
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋) → ((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))) ∈ 𝐵)) |
21 | | pmapsubcl.m |
. . . . . . . . . 10
⊢ 𝑀 = (pmap‘𝐾) |
22 | 13, 16, 1, 21, 2 | polval2N 37543 |
. . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧
((⊥𝑃‘𝐾)‘𝑋) ⊆ (Atoms‘𝐾)) →
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))))) |
23 | 9, 22 | syldan 594 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ (Atoms‘𝐾)) →
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))))) |
24 | 23 | ex 416 |
. . . . . . 7
⊢ (𝐾 ∈ HL → (𝑋 ⊆ (Atoms‘𝐾) →
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)))))) |
25 | | eqeq1 2742 |
. . . . . . . 8
⊢
(((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋 →
(((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)))) ↔ 𝑋 = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)))))) |
26 | 25 | biimpcd 252 |
. . . . . . 7
⊢
(((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)))) →
(((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋 → 𝑋 = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)))))) |
27 | 24, 26 | syl6 35 |
. . . . . 6
⊢ (𝐾 ∈ HL → (𝑋 ⊆ (Atoms‘𝐾) →
(((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋 → 𝑋 = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))))))) |
28 | 27 | impd 414 |
. . . . 5
⊢ (𝐾 ∈ HL → ((𝑋 ⊆ (Atoms‘𝐾) ∧
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋) → 𝑋 = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)))))) |
29 | 20, 28 | jcad 516 |
. . . 4
⊢ (𝐾 ∈ HL → ((𝑋 ⊆ (Atoms‘𝐾) ∧
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋) → (((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))) ∈ 𝐵 ∧ 𝑋 = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))))))) |
30 | | fveq2 6674 |
. . . . 5
⊢ (𝑦 = ((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))) → (𝑀‘𝑦) = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))))) |
31 | 30 | rspceeqv 3541 |
. . . 4
⊢
((((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))) ∈ 𝐵 ∧ 𝑋 = (𝑀‘((oc‘𝐾)‘((lub‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋))))) → ∃𝑦 ∈ 𝐵 𝑋 = (𝑀‘𝑦)) |
32 | 29, 31 | syl6 35 |
. . 3
⊢ (𝐾 ∈ HL → ((𝑋 ⊆ (Atoms‘𝐾) ∧
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋) → ∃𝑦 ∈ 𝐵 𝑋 = (𝑀‘𝑦))) |
33 | 10, 1, 21 | pmapssat 37396 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑦 ∈ 𝐵) → (𝑀‘𝑦) ⊆ (Atoms‘𝐾)) |
34 | 10, 21, 2 | 2polpmapN 37550 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑦 ∈ 𝐵) →
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘(𝑀‘𝑦))) = (𝑀‘𝑦)) |
35 | | sseq1 3902 |
. . . . . . 7
⊢ (𝑋 = (𝑀‘𝑦) → (𝑋 ⊆ (Atoms‘𝐾) ↔ (𝑀‘𝑦) ⊆ (Atoms‘𝐾))) |
36 | | 2fveq3 6679 |
. . . . . . . 8
⊢ (𝑋 = (𝑀‘𝑦) →
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = ((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘(𝑀‘𝑦)))) |
37 | | id 22 |
. . . . . . . 8
⊢ (𝑋 = (𝑀‘𝑦) → 𝑋 = (𝑀‘𝑦)) |
38 | 36, 37 | eqeq12d 2754 |
. . . . . . 7
⊢ (𝑋 = (𝑀‘𝑦) →
(((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋 ↔ ((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘(𝑀‘𝑦))) = (𝑀‘𝑦))) |
39 | 35, 38 | anbi12d 634 |
. . . . . 6
⊢ (𝑋 = (𝑀‘𝑦) → ((𝑋 ⊆ (Atoms‘𝐾) ∧
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋) ↔ ((𝑀‘𝑦) ⊆ (Atoms‘𝐾) ∧ ((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘(𝑀‘𝑦))) = (𝑀‘𝑦)))) |
40 | 39 | biimprcd 253 |
. . . . 5
⊢ (((𝑀‘𝑦) ⊆ (Atoms‘𝐾) ∧
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘(𝑀‘𝑦))) = (𝑀‘𝑦)) → (𝑋 = (𝑀‘𝑦) → (𝑋 ⊆ (Atoms‘𝐾) ∧ ((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋))) |
41 | 33, 34, 40 | syl2anc 587 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑦 ∈ 𝐵) → (𝑋 = (𝑀‘𝑦) → (𝑋 ⊆ (Atoms‘𝐾) ∧
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋))) |
42 | 41 | rexlimdva 3194 |
. . 3
⊢ (𝐾 ∈ HL → (∃𝑦 ∈ 𝐵 𝑋 = (𝑀‘𝑦) → (𝑋 ⊆ (Atoms‘𝐾) ∧
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋))) |
43 | 32, 42 | impbid 215 |
. 2
⊢ (𝐾 ∈ HL → ((𝑋 ⊆ (Atoms‘𝐾) ∧
((⊥𝑃‘𝐾)‘((⊥𝑃‘𝐾)‘𝑋)) = 𝑋) ↔ ∃𝑦 ∈ 𝐵 𝑋 = (𝑀‘𝑦))) |
44 | 4, 43 | bitrd 282 |
1
⊢ (𝐾 ∈ HL → (𝑋 ∈ 𝐶 ↔ ∃𝑦 ∈ 𝐵 𝑋 = (𝑀‘𝑦))) |