Step |
Hyp |
Ref |
Expression |
1 |
|
pmapsubcl.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
2 |
|
pmapsubcl.m |
⊢ 𝑀 = ( pmap ‘ 𝐾 ) |
3 |
|
pmapsubcl.c |
⊢ 𝐶 = ( PSubCl ‘ 𝐾 ) |
4 |
|
eqid |
⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 ) |
5 |
|
eqid |
⊢ ( ⊥𝑃 ‘ 𝐾 ) = ( ⊥𝑃 ‘ 𝐾 ) |
6 |
4 5 3
|
ispsubclN |
⊢ ( 𝐾 ∈ HL → ( 𝑋 ∈ 𝐶 ↔ ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 ) ) ) |
7 |
|
hlop |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP ) |
8 |
7
|
adantr |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ) → 𝐾 ∈ OP ) |
9 |
|
hlclat |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ CLat ) |
10 |
9
|
adantr |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ) → 𝐾 ∈ CLat ) |
11 |
4 5
|
polssatN |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ) → ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ⊆ ( Atoms ‘ 𝐾 ) ) |
12 |
1 4
|
atssbase |
⊢ ( Atoms ‘ 𝐾 ) ⊆ 𝐵 |
13 |
11 12
|
sstrdi |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ) → ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ⊆ 𝐵 ) |
14 |
|
eqid |
⊢ ( lub ‘ 𝐾 ) = ( lub ‘ 𝐾 ) |
15 |
1 14
|
clatlubcl |
⊢ ( ( 𝐾 ∈ CLat ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ⊆ 𝐵 ) → ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ∈ 𝐵 ) |
16 |
10 13 15
|
syl2anc |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ) → ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ∈ 𝐵 ) |
17 |
|
eqid |
⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 ) |
18 |
1 17
|
opoccl |
⊢ ( ( 𝐾 ∈ OP ∧ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ∈ 𝐵 ) |
19 |
8 16 18
|
syl2anc |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ∈ 𝐵 ) |
20 |
19
|
ex |
⊢ ( 𝐾 ∈ HL → ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ∈ 𝐵 ) ) |
21 |
20
|
adantrd |
⊢ ( 𝐾 ∈ HL → ( ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ∈ 𝐵 ) ) |
22 |
14 17 4 2 5
|
polval2N |
⊢ ( ( 𝐾 ∈ HL ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ⊆ ( Atoms ‘ 𝐾 ) ) → ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ) ) |
23 |
11 22
|
syldan |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ) → ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ) ) |
24 |
23
|
ex |
⊢ ( 𝐾 ∈ HL → ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) → ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ) ) ) |
25 |
|
eqeq1 |
⊢ ( ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 → ( ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ) ↔ 𝑋 = ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ) ) ) |
26 |
25
|
biimpcd |
⊢ ( ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ) → ( ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 → 𝑋 = ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ) ) ) |
27 |
24 26
|
syl6 |
⊢ ( 𝐾 ∈ HL → ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) → ( ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 → 𝑋 = ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ) ) ) ) |
28 |
27
|
impd |
⊢ ( 𝐾 ∈ HL → ( ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 ) → 𝑋 = ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ) ) ) |
29 |
21 28
|
jcad |
⊢ ( 𝐾 ∈ HL → ( ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 ) → ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ∈ 𝐵 ∧ 𝑋 = ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ) ) ) ) |
30 |
|
fveq2 |
⊢ ( 𝑦 = ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) → ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ) ) |
31 |
30
|
rspceeqv |
⊢ ( ( ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ∈ 𝐵 ∧ 𝑋 = ( 𝑀 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( lub ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) ) ) ) → ∃ 𝑦 ∈ 𝐵 𝑋 = ( 𝑀 ‘ 𝑦 ) ) |
32 |
29 31
|
syl6 |
⊢ ( 𝐾 ∈ HL → ( ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 ) → ∃ 𝑦 ∈ 𝐵 𝑋 = ( 𝑀 ‘ 𝑦 ) ) ) |
33 |
1 4 2
|
pmapssat |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑦 ) ⊆ ( Atoms ‘ 𝐾 ) ) |
34 |
1 2 5
|
2polpmapN |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ 𝐵 ) → ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( 𝑀 ‘ 𝑦 ) ) ) = ( 𝑀 ‘ 𝑦 ) ) |
35 |
|
sseq1 |
⊢ ( 𝑋 = ( 𝑀 ‘ 𝑦 ) → ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ↔ ( 𝑀 ‘ 𝑦 ) ⊆ ( Atoms ‘ 𝐾 ) ) ) |
36 |
|
2fveq3 |
⊢ ( 𝑋 = ( 𝑀 ‘ 𝑦 ) → ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( 𝑀 ‘ 𝑦 ) ) ) ) |
37 |
|
id |
⊢ ( 𝑋 = ( 𝑀 ‘ 𝑦 ) → 𝑋 = ( 𝑀 ‘ 𝑦 ) ) |
38 |
36 37
|
eqeq12d |
⊢ ( 𝑋 = ( 𝑀 ‘ 𝑦 ) → ( ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 ↔ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( 𝑀 ‘ 𝑦 ) ) ) = ( 𝑀 ‘ 𝑦 ) ) ) |
39 |
35 38
|
anbi12d |
⊢ ( 𝑋 = ( 𝑀 ‘ 𝑦 ) → ( ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 ) ↔ ( ( 𝑀 ‘ 𝑦 ) ⊆ ( Atoms ‘ 𝐾 ) ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( 𝑀 ‘ 𝑦 ) ) ) = ( 𝑀 ‘ 𝑦 ) ) ) ) |
40 |
39
|
biimprcd |
⊢ ( ( ( 𝑀 ‘ 𝑦 ) ⊆ ( Atoms ‘ 𝐾 ) ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( 𝑀 ‘ 𝑦 ) ) ) = ( 𝑀 ‘ 𝑦 ) ) → ( 𝑋 = ( 𝑀 ‘ 𝑦 ) → ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 ) ) ) |
41 |
33 34 40
|
syl2anc |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ 𝐵 ) → ( 𝑋 = ( 𝑀 ‘ 𝑦 ) → ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 ) ) ) |
42 |
41
|
rexlimdva |
⊢ ( 𝐾 ∈ HL → ( ∃ 𝑦 ∈ 𝐵 𝑋 = ( 𝑀 ‘ 𝑦 ) → ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 ) ) ) |
43 |
32 42
|
impbid |
⊢ ( 𝐾 ∈ HL → ( ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ ( ( ⊥𝑃 ‘ 𝐾 ) ‘ 𝑋 ) ) = 𝑋 ) ↔ ∃ 𝑦 ∈ 𝐵 𝑋 = ( 𝑀 ‘ 𝑦 ) ) ) |
44 |
6 43
|
bitrd |
⊢ ( 𝐾 ∈ HL → ( 𝑋 ∈ 𝐶 ↔ ∃ 𝑦 ∈ 𝐵 𝑋 = ( 𝑀 ‘ 𝑦 ) ) ) |