Step |
Hyp |
Ref |
Expression |
1 |
|
dihglblem.b |
|- B = ( Base ` K ) |
2 |
|
dihglblem.l |
|- .<_ = ( le ` K ) |
3 |
|
dihglblem.m |
|- ./\ = ( meet ` K ) |
4 |
|
dihglblem.g |
|- G = ( glb ` K ) |
5 |
|
dihglblem.h |
|- H = ( LHyp ` K ) |
6 |
|
dihglblem.t |
|- T = { u e. B | E. v e. S u = ( v ./\ W ) } |
7 |
|
dihglblem.i |
|- J = ( ( DIsoB ` K ) ` W ) |
8 |
|
dihglblem.ih |
|- I = ( ( DIsoH ` K ) ` W ) |
9 |
|
hlclat |
|- ( K e. HL -> K e. CLat ) |
10 |
9
|
ad3antrrr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ x e. S ) -> K e. CLat ) |
11 |
|
simplrl |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ x e. S ) -> S C_ B ) |
12 |
|
simpr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ x e. S ) -> x e. S ) |
13 |
1 2 4
|
clatglble |
|- ( ( K e. CLat /\ S C_ B /\ x e. S ) -> ( G ` S ) .<_ x ) |
14 |
10 11 12 13
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ x e. S ) -> ( G ` S ) .<_ x ) |
15 |
|
simpll |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ x e. S ) -> ( K e. HL /\ W e. H ) ) |
16 |
1 4
|
clatglbcl |
|- ( ( K e. CLat /\ S C_ B ) -> ( G ` S ) e. B ) |
17 |
10 11 16
|
syl2anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ x e. S ) -> ( G ` S ) e. B ) |
18 |
11 12
|
sseldd |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ x e. S ) -> x e. B ) |
19 |
1 2 5 8
|
dihord |
|- ( ( ( K e. HL /\ W e. H ) /\ ( G ` S ) e. B /\ x e. B ) -> ( ( I ` ( G ` S ) ) C_ ( I ` x ) <-> ( G ` S ) .<_ x ) ) |
20 |
15 17 18 19
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ x e. S ) -> ( ( I ` ( G ` S ) ) C_ ( I ` x ) <-> ( G ` S ) .<_ x ) ) |
21 |
14 20
|
mpbird |
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) /\ x e. S ) -> ( I ` ( G ` S ) ) C_ ( I ` x ) ) |
22 |
21
|
ralrimiva |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) -> A. x e. S ( I ` ( G ` S ) ) C_ ( I ` x ) ) |
23 |
|
ssiin |
|- ( ( I ` ( G ` S ) ) C_ |^|_ x e. S ( I ` x ) <-> A. x e. S ( I ` ( G ` S ) ) C_ ( I ` x ) ) |
24 |
22 23
|
sylibr |
|- ( ( ( K e. HL /\ W e. H ) /\ ( S C_ B /\ S =/= (/) ) ) -> ( I ` ( G ` S ) ) C_ |^|_ x e. S ( I ` x ) ) |