Metamath Proof Explorer

Theorem dihord5b

Description: Part of proof that isomorphism H is order-preserving. TODO: eliminate 3ad2ant1; combine with other way to have one lhpmcvr2 . (Contributed by NM, 7-Mar-2014)

Ref Expression
Hypotheses dihord3.b 
|- B = ( Base ` K )
dihord3.l 
|- .<_ = ( le ` K )
dihord3.h 
|- H = ( LHyp ` K )
dihord3.i 
|- I = ( ( DIsoH ` K ) ` W )
Assertion dihord5b 
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) -> ( I ` X ) C_ ( I ` Y ) )

Proof

Step Hyp Ref Expression
1 dihord3.b 
 |-  B = ( Base ` K )
2 dihord3.l 
 |-  .<_ = ( le ` K )
3 dihord3.h 
 |-  H = ( LHyp ` K )
4 dihord3.i 
 |-  I = ( ( DIsoH ` K ) ` W )
5 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) -> ( K e. HL /\ W e. H ) )
6 simpl3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) -> ( Y e. B /\ -. Y .<_ W ) )
7 eqid 
 |-  ( join ` K ) = ( join ` K )
8 eqid 
 |-  ( meet ` K ) = ( meet ` K )
9 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
10 1 2 7 8 9 3 lhpmcvr2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Y e. B /\ -. Y .<_ W ) ) -> E. r e. ( Atoms ` K ) ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) )
11 5 6 10 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) -> E. r e. ( Atoms ` K ) ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) )
12 simp1r 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) /\ ( r e. ( Atoms ` K ) /\ -. r .<_ W ) /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) -> X .<_ Y )
13 simpl2r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) -> X .<_ W )
14 13 3ad2ant1 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) /\ ( r e. ( Atoms ` K ) /\ -. r .<_ W ) /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) -> X .<_ W )
15 simpl1l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) -> K e. HL )
16 15 3ad2ant1 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) /\ ( r e. ( Atoms ` K ) /\ -. r .<_ W ) /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) -> K e. HL )
17 16 hllatd 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) /\ ( r e. ( Atoms ` K ) /\ -. r .<_ W ) /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) -> K e. Lat )
18 simpl2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) -> X e. B )
19 18 3ad2ant1 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) /\ ( r e. ( Atoms ` K ) /\ -. r .<_ W ) /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) -> X e. B )
20 simpl3l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) -> Y e. B )
21 20 3ad2ant1 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) /\ ( r e. ( Atoms ` K ) /\ -. r .<_ W ) /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) -> Y e. B )
22 simpl1r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) -> W e. H )
23 22 3ad2ant1 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) /\ ( r e. ( Atoms ` K ) /\ -. r .<_ W ) /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) -> W e. H )
24 1 3 lhpbase 
 |-  ( W e. H -> W e. B )
25 23 24 syl 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) /\ ( r e. ( Atoms ` K ) /\ -. r .<_ W ) /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) -> W e. B )
26 1 2 8 latlem12 
 |-  ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ W e. B ) ) -> ( ( X .<_ Y /\ X .<_ W ) <-> X .<_ ( Y ( meet ` K ) W ) ) )
27 17 19 21 25 26 syl13anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) /\ ( r e. ( Atoms ` K ) /\ -. r .<_ W ) /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) -> ( ( X .<_ Y /\ X .<_ W ) <-> X .<_ ( Y ( meet ` K ) W ) ) )
28 12 14 27 mpbi2and 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) /\ ( r e. ( Atoms ` K ) /\ -. r .<_ W ) /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) -> X .<_ ( Y ( meet ` K ) W ) )
29 simp1l1 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) /\ ( r e. ( Atoms ` K ) /\ -. r .<_ W ) /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) -> ( K e. HL /\ W e. H ) )
30 simp1l2 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) /\ ( r e. ( Atoms ` K ) /\ -. r .<_ W ) /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) -> ( X e. B /\ X .<_ W ) )
31 1 8 latmcl 
 |-  ( ( K e. Lat /\ Y e. B /\ W e. B ) -> ( Y ( meet ` K ) W ) e. B )
32 17 21 25 31 syl3anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) /\ ( r e. ( Atoms ` K ) /\ -. r .<_ W ) /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) -> ( Y ( meet ` K ) W ) e. B )
33 1 2 8 latmle2 
 |-  ( ( K e. Lat /\ Y e. B /\ W e. B ) -> ( Y ( meet ` K ) W ) .<_ W )
34 17 21 25 33 syl3anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) /\ ( r e. ( Atoms ` K ) /\ -. r .<_ W ) /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) -> ( Y ( meet ` K ) W ) .<_ W )
35 eqid 
 |-  ( ( DIsoB ` K ) ` W ) = ( ( DIsoB ` K ) ` W )
36 1 2 3 35 dibord 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( ( Y ( meet ` K ) W ) e. B /\ ( Y ( meet ` K ) W ) .<_ W ) ) -> ( ( ( ( DIsoB ` K ) ` W ) ` X ) C_ ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) <-> X .<_ ( Y ( meet ` K ) W ) ) )
37 29 30 32 34 36 syl112anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) /\ ( r e. ( Atoms ` K ) /\ -. r .<_ W ) /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) -> ( ( ( ( DIsoB ` K ) ` W ) ` X ) C_ ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) <-> X .<_ ( Y ( meet ` K ) W ) ) )
38 28 37 mpbird 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) /\ ( r e. ( Atoms ` K ) /\ -. r .<_ W ) /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) -> ( ( ( DIsoB ` K ) ` W ) ` X ) C_ ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) )
39 eqid 
 |-  ( ( DVecH ` K ) ` W ) = ( ( DVecH ` K ) ` W )
40 3 39 29 dvhlmod 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) /\ ( r e. ( Atoms ` K ) /\ -. r .<_ W ) /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) -> ( ( DVecH ` K ) ` W ) e. LMod )
41 eqid 
 |-  ( LSubSp ` ( ( DVecH ` K ) ` W ) ) = ( LSubSp ` ( ( DVecH ` K ) ` W ) )
42 41 lsssssubg 
 |-  ( ( ( DVecH ` K ) ` W ) e. LMod -> ( LSubSp ` ( ( DVecH ` K ) ` W ) ) C_ ( SubGrp ` ( ( DVecH ` K ) ` W ) ) )
43 40 42 syl 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) /\ ( r e. ( Atoms ` K ) /\ -. r .<_ W ) /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) -> ( LSubSp ` ( ( DVecH ` K ) ` W ) ) C_ ( SubGrp ` ( ( DVecH ` K ) ` W ) ) )
44 simp2 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) /\ ( r e. ( Atoms ` K ) /\ -. r .<_ W ) /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) -> ( r e. ( Atoms ` K ) /\ -. r .<_ W ) )
45 eqid 
 |-  ( ( DIsoC ` K ) ` W ) = ( ( DIsoC ` K ) ` W )
46 2 9 3 39 45 41 diclss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( r e. ( Atoms ` K ) /\ -. r .<_ W ) ) -> ( ( ( DIsoC ` K ) ` W ) ` r ) e. ( LSubSp ` ( ( DVecH ` K ) ` W ) ) )
47 29 44 46 syl2anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) /\ ( r e. ( Atoms ` K ) /\ -. r .<_ W ) /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) -> ( ( ( DIsoC ` K ) ` W ) ` r ) e. ( LSubSp ` ( ( DVecH ` K ) ` W ) ) )
48 43 47 sseldd 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) /\ ( r e. ( Atoms ` K ) /\ -. r .<_ W ) /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) -> ( ( ( DIsoC ` K ) ` W ) ` r ) e. ( SubGrp ` ( ( DVecH ` K ) ` W ) ) )
49 1 2 3 39 35 41 diblss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( Y ( meet ` K ) W ) e. B /\ ( Y ( meet ` K ) W ) .<_ W ) ) -> ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) e. ( LSubSp ` ( ( DVecH ` K ) ` W ) ) )
50 29 32 34 49 syl12anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) /\ ( r e. ( Atoms ` K ) /\ -. r .<_ W ) /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) -> ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) e. ( LSubSp ` ( ( DVecH ` K ) ` W ) ) )
51 43 50 sseldd 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) /\ ( r e. ( Atoms ` K ) /\ -. r .<_ W ) /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) -> ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) e. ( SubGrp ` ( ( DVecH ` K ) ` W ) ) )
52 eqid 
 |-  ( LSSum ` ( ( DVecH ` K ) ` W ) ) = ( LSSum ` ( ( DVecH ` K ) ` W ) )
53 52 lsmub2 
 |-  ( ( ( ( ( DIsoC ` K ) ` W ) ` r ) e. ( SubGrp ` ( ( DVecH ` K ) ` W ) ) /\ ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) e. ( SubGrp ` ( ( DVecH ` K ) ` W ) ) ) -> ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) C_ ( ( ( ( DIsoC ` K ) ` W ) ` r ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) ) )
54 48 51 53 syl2anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) /\ ( r e. ( Atoms ` K ) /\ -. r .<_ W ) /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) -> ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) C_ ( ( ( ( DIsoC ` K ) ` W ) ` r ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) ) )
55 38 54 sstrd 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) /\ ( r e. ( Atoms ` K ) /\ -. r .<_ W ) /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) -> ( ( ( DIsoB ` K ) ` W ) ` X ) C_ ( ( ( ( DIsoC ` K ) ` W ) ` r ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) ) )
56 1 2 3 4 35 dihvalb 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) ) -> ( I ` X ) = ( ( ( DIsoB ` K ) ` W ) ` X ) )
57 29 30 56 syl2anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) /\ ( r e. ( Atoms ` K ) /\ -. r .<_ W ) /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) -> ( I ` X ) = ( ( ( DIsoB ` K ) ` W ) ` X ) )
58 simp1l3 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) /\ ( r e. ( Atoms ` K ) /\ -. r .<_ W ) /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) -> ( Y e. B /\ -. Y .<_ W ) )
59 simp3 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) /\ ( r e. ( Atoms ` K ) /\ -. r .<_ W ) /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) -> ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y )
60 1 2 7 8 9 3 4 35 45 39 52 dihvalcq 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Y e. B /\ -. Y .<_ W ) /\ ( ( r e. ( Atoms ` K ) /\ -. r .<_ W ) /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) ) -> ( I ` Y ) = ( ( ( ( DIsoC ` K ) ` W ) ` r ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) ) )
61 29 58 44 59 60 syl112anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) /\ ( r e. ( Atoms ` K ) /\ -. r .<_ W ) /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) -> ( I ` Y ) = ( ( ( ( DIsoC ` K ) ` W ) ` r ) ( LSSum ` ( ( DVecH ` K ) ` W ) ) ( ( ( DIsoB ` K ) ` W ) ` ( Y ( meet ` K ) W ) ) ) )
62 55 57 61 3sstr4d 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) /\ ( r e. ( Atoms ` K ) /\ -. r .<_ W ) /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) -> ( I ` X ) C_ ( I ` Y ) )
63 62 3exp 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) -> ( ( r e. ( Atoms ` K ) /\ -. r .<_ W ) -> ( ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y -> ( I ` X ) C_ ( I ` Y ) ) ) )
64 63 expd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) -> ( r e. ( Atoms ` K ) -> ( -. r .<_ W -> ( ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y -> ( I ` X ) C_ ( I ` Y ) ) ) ) )
65 64 imp4a 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) -> ( r e. ( Atoms ` K ) -> ( ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) -> ( I ` X ) C_ ( I ` Y ) ) ) )
66 65 rexlimdv 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) -> ( E. r e. ( Atoms ` K ) ( -. r .<_ W /\ ( r ( join ` K ) ( Y ( meet ` K ) W ) ) = Y ) -> ( I ` X ) C_ ( I ` Y ) ) )
67 11 66 mpd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X .<_ W ) /\ ( Y e. B /\ -. Y .<_ W ) ) /\ X .<_ Y ) -> ( I ` X ) C_ ( I ` Y ) )