Step |
Hyp |
Ref |
Expression |
1 |
|
pmapsubcl.b |
|- B = ( Base ` K ) |
2 |
|
pmapsubcl.m |
|- M = ( pmap ` K ) |
3 |
|
pmapsubcl.c |
|- C = ( PSubCl ` K ) |
4 |
|
eqid |
|- ( Atoms ` K ) = ( Atoms ` K ) |
5 |
|
eqid |
|- ( _|_P ` K ) = ( _|_P ` K ) |
6 |
4 5 3
|
ispsubclN |
|- ( K e. HL -> ( X e. C <-> ( X C_ ( Atoms ` K ) /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X ) ) ) |
7 |
|
hlop |
|- ( K e. HL -> K e. OP ) |
8 |
7
|
adantr |
|- ( ( K e. HL /\ X C_ ( Atoms ` K ) ) -> K e. OP ) |
9 |
|
hlclat |
|- ( K e. HL -> K e. CLat ) |
10 |
9
|
adantr |
|- ( ( K e. HL /\ X C_ ( Atoms ` K ) ) -> K e. CLat ) |
11 |
4 5
|
polssatN |
|- ( ( K e. HL /\ X C_ ( Atoms ` K ) ) -> ( ( _|_P ` K ) ` X ) C_ ( Atoms ` K ) ) |
12 |
1 4
|
atssbase |
|- ( Atoms ` K ) C_ B |
13 |
11 12
|
sstrdi |
|- ( ( K e. HL /\ X C_ ( Atoms ` K ) ) -> ( ( _|_P ` K ) ` X ) C_ B ) |
14 |
|
eqid |
|- ( lub ` K ) = ( lub ` K ) |
15 |
1 14
|
clatlubcl |
|- ( ( K e. CLat /\ ( ( _|_P ` K ) ` X ) C_ B ) -> ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) e. B ) |
16 |
10 13 15
|
syl2anc |
|- ( ( K e. HL /\ X C_ ( Atoms ` K ) ) -> ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) e. B ) |
17 |
|
eqid |
|- ( oc ` K ) = ( oc ` K ) |
18 |
1 17
|
opoccl |
|- ( ( K e. OP /\ ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) e. B ) -> ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) e. B ) |
19 |
8 16 18
|
syl2anc |
|- ( ( K e. HL /\ X C_ ( Atoms ` K ) ) -> ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) e. B ) |
20 |
19
|
ex |
|- ( K e. HL -> ( X C_ ( Atoms ` K ) -> ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) e. B ) ) |
21 |
20
|
adantrd |
|- ( K e. HL -> ( ( X C_ ( Atoms ` K ) /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X ) -> ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) e. B ) ) |
22 |
14 17 4 2 5
|
polval2N |
|- ( ( K e. HL /\ ( ( _|_P ` K ) ` X ) C_ ( Atoms ` K ) ) -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = ( M ` ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) ) ) |
23 |
11 22
|
syldan |
|- ( ( K e. HL /\ X C_ ( Atoms ` K ) ) -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = ( M ` ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) ) ) |
24 |
23
|
ex |
|- ( K e. HL -> ( X C_ ( Atoms ` K ) -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = ( M ` ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) ) ) ) |
25 |
|
eqeq1 |
|- ( ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X -> ( ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = ( M ` ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) ) <-> X = ( M ` ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) ) ) ) |
26 |
25
|
biimpcd |
|- ( ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = ( M ` ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) ) -> ( ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X -> X = ( M ` ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) ) ) ) |
27 |
24 26
|
syl6 |
|- ( K e. HL -> ( X C_ ( Atoms ` K ) -> ( ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X -> X = ( M ` ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) ) ) ) ) |
28 |
27
|
impd |
|- ( K e. HL -> ( ( X C_ ( Atoms ` K ) /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X ) -> X = ( M ` ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) ) ) ) |
29 |
21 28
|
jcad |
|- ( K e. HL -> ( ( X C_ ( Atoms ` K ) /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X ) -> ( ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) e. B /\ X = ( M ` ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) ) ) ) ) |
30 |
|
fveq2 |
|- ( y = ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) -> ( M ` y ) = ( M ` ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) ) ) |
31 |
30
|
rspceeqv |
|- ( ( ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) e. B /\ X = ( M ` ( ( oc ` K ) ` ( ( lub ` K ) ` ( ( _|_P ` K ) ` X ) ) ) ) ) -> E. y e. B X = ( M ` y ) ) |
32 |
29 31
|
syl6 |
|- ( K e. HL -> ( ( X C_ ( Atoms ` K ) /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X ) -> E. y e. B X = ( M ` y ) ) ) |
33 |
1 4 2
|
pmapssat |
|- ( ( K e. HL /\ y e. B ) -> ( M ` y ) C_ ( Atoms ` K ) ) |
34 |
1 2 5
|
2polpmapN |
|- ( ( K e. HL /\ y e. B ) -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` ( M ` y ) ) ) = ( M ` y ) ) |
35 |
|
sseq1 |
|- ( X = ( M ` y ) -> ( X C_ ( Atoms ` K ) <-> ( M ` y ) C_ ( Atoms ` K ) ) ) |
36 |
|
2fveq3 |
|- ( X = ( M ` y ) -> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` ( M ` y ) ) ) ) |
37 |
|
id |
|- ( X = ( M ` y ) -> X = ( M ` y ) ) |
38 |
36 37
|
eqeq12d |
|- ( X = ( M ` y ) -> ( ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X <-> ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` ( M ` y ) ) ) = ( M ` y ) ) ) |
39 |
35 38
|
anbi12d |
|- ( X = ( M ` y ) -> ( ( X C_ ( Atoms ` K ) /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X ) <-> ( ( M ` y ) C_ ( Atoms ` K ) /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` ( M ` y ) ) ) = ( M ` y ) ) ) ) |
40 |
39
|
biimprcd |
|- ( ( ( M ` y ) C_ ( Atoms ` K ) /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` ( M ` y ) ) ) = ( M ` y ) ) -> ( X = ( M ` y ) -> ( X C_ ( Atoms ` K ) /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X ) ) ) |
41 |
33 34 40
|
syl2anc |
|- ( ( K e. HL /\ y e. B ) -> ( X = ( M ` y ) -> ( X C_ ( Atoms ` K ) /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X ) ) ) |
42 |
41
|
rexlimdva |
|- ( K e. HL -> ( E. y e. B X = ( M ` y ) -> ( X C_ ( Atoms ` K ) /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X ) ) ) |
43 |
32 42
|
impbid |
|- ( K e. HL -> ( ( X C_ ( Atoms ` K ) /\ ( ( _|_P ` K ) ` ( ( _|_P ` K ) ` X ) ) = X ) <-> E. y e. B X = ( M ` y ) ) ) |
44 |
6 43
|
bitrd |
|- ( K e. HL -> ( X e. C <-> E. y e. B X = ( M ` y ) ) ) |