Metamath Proof Explorer


Theorem llncvrlpln2

Description: A lattice line under a lattice plane is covered by it. (Contributed by NM, 24-Jun-2012)

Ref Expression
Hypotheses llncvrlpln2.l
|- .<_ = ( le ` K )
llncvrlpln2.c
|- C = ( 
llncvrlpln2.n
|- N = ( LLines ` K )
llncvrlpln2.p
|- P = ( LPlanes ` K )
Assertion llncvrlpln2
|- ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ X .<_ Y ) -> X C Y )

Proof

Step Hyp Ref Expression
1 llncvrlpln2.l
 |-  .<_ = ( le ` K )
2 llncvrlpln2.c
 |-  C = ( 
3 llncvrlpln2.n
 |-  N = ( LLines ` K )
4 llncvrlpln2.p
 |-  P = ( LPlanes ` K )
5 simpr
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ X .<_ Y ) -> X .<_ Y )
6 simpl1
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ X .<_ Y ) -> K e. HL )
7 simpl3
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ X .<_ Y ) -> Y e. P )
8 3 4 lplnnelln
 |-  ( ( K e. HL /\ Y e. P ) -> -. Y e. N )
9 6 7 8 syl2anc
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ X .<_ Y ) -> -. Y e. N )
10 simpl2
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ X .<_ Y ) -> X e. N )
11 eleq1
 |-  ( X = Y -> ( X e. N <-> Y e. N ) )
12 10 11 syl5ibcom
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ X .<_ Y ) -> ( X = Y -> Y e. N ) )
13 12 necon3bd
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ X .<_ Y ) -> ( -. Y e. N -> X =/= Y ) )
14 9 13 mpd
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ X .<_ Y ) -> X =/= Y )
15 eqid
 |-  ( lt ` K ) = ( lt ` K )
16 1 15 pltval
 |-  ( ( K e. HL /\ X e. N /\ Y e. P ) -> ( X ( lt ` K ) Y <-> ( X .<_ Y /\ X =/= Y ) ) )
17 16 adantr
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ X .<_ Y ) -> ( X ( lt ` K ) Y <-> ( X .<_ Y /\ X =/= Y ) ) )
18 5 14 17 mpbir2and
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ X .<_ Y ) -> X ( lt ` K ) Y )
19 simpl1
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ X ( lt ` K ) Y ) -> K e. HL )
20 simpl2
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ X ( lt ` K ) Y ) -> X e. N )
21 eqid
 |-  ( Base ` K ) = ( Base ` K )
22 21 3 llnbase
 |-  ( X e. N -> X e. ( Base ` K ) )
23 20 22 syl
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ X ( lt ` K ) Y ) -> X e. ( Base ` K ) )
24 simpl3
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ X ( lt ` K ) Y ) -> Y e. P )
25 21 4 lplnbase
 |-  ( Y e. P -> Y e. ( Base ` K ) )
26 24 25 syl
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ X ( lt ` K ) Y ) -> Y e. ( Base ` K ) )
27 simpr
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ X ( lt ` K ) Y ) -> X ( lt ` K ) Y )
28 eqid
 |-  ( join ` K ) = ( join ` K )
29 eqid
 |-  ( Atoms ` K ) = ( Atoms ` K )
30 21 1 15 28 2 29 hlrelat3
 |-  ( ( ( K e. HL /\ X e. ( Base ` K ) /\ Y e. ( Base ` K ) ) /\ X ( lt ` K ) Y ) -> E. r e. ( Atoms ` K ) ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) )
31 19 23 26 27 30 syl31anc
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ X ( lt ` K ) Y ) -> E. r e. ( Atoms ` K ) ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) )
32 21 1 28 29 4 islpln2
 |-  ( K e. HL -> ( Y e. P <-> ( Y e. ( Base ` K ) /\ E. s e. ( Atoms ` K ) E. t e. ( Atoms ` K ) E. u e. ( Atoms ` K ) ( s =/= t /\ -. u .<_ ( s ( join ` K ) t ) /\ Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) ) ) ) )
33 32 adantr
 |-  ( ( K e. HL /\ X e. N ) -> ( Y e. P <-> ( Y e. ( Base ` K ) /\ E. s e. ( Atoms ` K ) E. t e. ( Atoms ` K ) E. u e. ( Atoms ` K ) ( s =/= t /\ -. u .<_ ( s ( join ` K ) t ) /\ Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) ) ) ) )
34 simp3
 |-  ( ( s =/= t /\ -. u .<_ ( s ( join ` K ) t ) /\ Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) ) -> Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) )
35 21 28 29 3 islln2
 |-  ( K e. HL -> ( X e. N <-> ( X e. ( Base ` K ) /\ E. p e. ( Atoms ` K ) E. q e. ( Atoms ` K ) ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) ) )
36 simp3l
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) /\ ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) ) /\ ( u e. ( Atoms ` K ) /\ Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) /\ r e. ( Atoms ` K ) ) /\ ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) ) -> X C ( X ( join ` K ) r ) )
37 simp3r
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) /\ ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) ) /\ ( u e. ( Atoms ` K ) /\ Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) /\ r e. ( Atoms ` K ) ) /\ ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) ) -> ( X ( join ` K ) r ) .<_ Y )
38 simp12r
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) /\ ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) ) /\ ( u e. ( Atoms ` K ) /\ Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) /\ r e. ( Atoms ` K ) ) /\ ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) ) -> X = ( p ( join ` K ) q ) )
39 38 oveq1d
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) /\ ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) ) /\ ( u e. ( Atoms ` K ) /\ Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) /\ r e. ( Atoms ` K ) ) /\ ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) ) -> ( X ( join ` K ) r ) = ( ( p ( join ` K ) q ) ( join ` K ) r ) )
40 simp22
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) /\ ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) ) /\ ( u e. ( Atoms ` K ) /\ Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) /\ r e. ( Atoms ` K ) ) /\ ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) ) -> Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) )
41 37 39 40 3brtr3d
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) /\ ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) ) /\ ( u e. ( Atoms ` K ) /\ Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) /\ r e. ( Atoms ` K ) ) /\ ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) ) -> ( ( p ( join ` K ) q ) ( join ` K ) r ) .<_ ( ( s ( join ` K ) t ) ( join ` K ) u ) )
42 simp111
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) /\ ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) ) /\ ( u e. ( Atoms ` K ) /\ Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) /\ r e. ( Atoms ` K ) ) /\ ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) ) -> K e. HL )
43 simp112
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) /\ ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) ) /\ ( u e. ( Atoms ` K ) /\ Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) /\ r e. ( Atoms ` K ) ) /\ ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) ) -> p e. ( Atoms ` K ) )
44 simp113
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) /\ ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) ) /\ ( u e. ( Atoms ` K ) /\ Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) /\ r e. ( Atoms ` K ) ) /\ ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) ) -> q e. ( Atoms ` K ) )
45 simp23
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) /\ ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) ) /\ ( u e. ( Atoms ` K ) /\ Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) /\ r e. ( Atoms ` K ) ) /\ ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) ) -> r e. ( Atoms ` K ) )
46 43 44 45 3jca
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) /\ ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) ) /\ ( u e. ( Atoms ` K ) /\ Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) /\ r e. ( Atoms ` K ) ) /\ ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) ) -> ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) )
47 simp13l
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) /\ ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) ) /\ ( u e. ( Atoms ` K ) /\ Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) /\ r e. ( Atoms ` K ) ) /\ ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) ) -> s e. ( Atoms ` K ) )
48 simp13r
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) /\ ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) ) /\ ( u e. ( Atoms ` K ) /\ Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) /\ r e. ( Atoms ` K ) ) /\ ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) ) -> t e. ( Atoms ` K ) )
49 simp21
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) /\ ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) ) /\ ( u e. ( Atoms ` K ) /\ Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) /\ r e. ( Atoms ` K ) ) /\ ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) ) -> u e. ( Atoms ` K ) )
50 47 48 49 3jca
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) /\ ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) ) /\ ( u e. ( Atoms ` K ) /\ Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) /\ r e. ( Atoms ` K ) ) /\ ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) ) -> ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) )
51 36 38 39 3brtr3d
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) /\ ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) ) /\ ( u e. ( Atoms ` K ) /\ Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) /\ r e. ( Atoms ` K ) ) /\ ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) ) -> ( p ( join ` K ) q ) C ( ( p ( join ` K ) q ) ( join ` K ) r ) )
52 21 28 29 hlatjcl
 |-  ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) -> ( p ( join ` K ) q ) e. ( Base ` K ) )
53 42 43 44 52 syl3anc
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) /\ ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) ) /\ ( u e. ( Atoms ` K ) /\ Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) /\ r e. ( Atoms ` K ) ) /\ ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) ) -> ( p ( join ` K ) q ) e. ( Base ` K ) )
54 21 1 28 2 29 cvr1
 |-  ( ( K e. HL /\ ( p ( join ` K ) q ) e. ( Base ` K ) /\ r e. ( Atoms ` K ) ) -> ( -. r .<_ ( p ( join ` K ) q ) <-> ( p ( join ` K ) q ) C ( ( p ( join ` K ) q ) ( join ` K ) r ) ) )
55 42 53 45 54 syl3anc
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) /\ ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) ) /\ ( u e. ( Atoms ` K ) /\ Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) /\ r e. ( Atoms ` K ) ) /\ ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) ) -> ( -. r .<_ ( p ( join ` K ) q ) <-> ( p ( join ` K ) q ) C ( ( p ( join ` K ) q ) ( join ` K ) r ) ) )
56 51 55 mpbird
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) /\ ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) ) /\ ( u e. ( Atoms ` K ) /\ Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) /\ r e. ( Atoms ` K ) ) /\ ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) ) -> -. r .<_ ( p ( join ` K ) q ) )
57 simp12l
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) /\ ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) ) /\ ( u e. ( Atoms ` K ) /\ Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) /\ r e. ( Atoms ` K ) ) /\ ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) ) -> p =/= q )
58 1 28 29 3at
 |-  ( ( ( K e. HL /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) ) ) /\ ( -. r .<_ ( p ( join ` K ) q ) /\ p =/= q ) ) -> ( ( ( p ( join ` K ) q ) ( join ` K ) r ) .<_ ( ( s ( join ` K ) t ) ( join ` K ) u ) <-> ( ( p ( join ` K ) q ) ( join ` K ) r ) = ( ( s ( join ` K ) t ) ( join ` K ) u ) ) )
59 42 46 50 56 57 58 syl32anc
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) /\ ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) ) /\ ( u e. ( Atoms ` K ) /\ Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) /\ r e. ( Atoms ` K ) ) /\ ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) ) -> ( ( ( p ( join ` K ) q ) ( join ` K ) r ) .<_ ( ( s ( join ` K ) t ) ( join ` K ) u ) <-> ( ( p ( join ` K ) q ) ( join ` K ) r ) = ( ( s ( join ` K ) t ) ( join ` K ) u ) ) )
60 41 59 mpbid
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) /\ ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) ) /\ ( u e. ( Atoms ` K ) /\ Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) /\ r e. ( Atoms ` K ) ) /\ ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) ) -> ( ( p ( join ` K ) q ) ( join ` K ) r ) = ( ( s ( join ` K ) t ) ( join ` K ) u ) )
61 60 39 40 3eqtr4d
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) /\ ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) ) /\ ( u e. ( Atoms ` K ) /\ Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) /\ r e. ( Atoms ` K ) ) /\ ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) ) -> ( X ( join ` K ) r ) = Y )
62 36 61 breqtrd
 |-  ( ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) /\ ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) ) /\ ( u e. ( Atoms ` K ) /\ Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) /\ r e. ( Atoms ` K ) ) /\ ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) ) -> X C Y )
63 62 3exp
 |-  ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) /\ ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) ) -> ( ( u e. ( Atoms ` K ) /\ Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) /\ r e. ( Atoms ` K ) ) -> ( ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) -> X C Y ) ) )
64 63 3expd
 |-  ( ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) /\ ( p =/= q /\ X = ( p ( join ` K ) q ) ) /\ ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) ) -> ( u e. ( Atoms ` K ) -> ( Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) -> ( r e. ( Atoms ` K ) -> ( ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) -> X C Y ) ) ) ) )
65 64 3exp
 |-  ( ( K e. HL /\ p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) -> ( ( p =/= q /\ X = ( p ( join ` K ) q ) ) -> ( ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) -> ( u e. ( Atoms ` K ) -> ( Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) -> ( r e. ( Atoms ` K ) -> ( ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) -> X C Y ) ) ) ) ) ) )
66 65 3expib
 |-  ( K e. HL -> ( ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) -> ( ( p =/= q /\ X = ( p ( join ` K ) q ) ) -> ( ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) -> ( u e. ( Atoms ` K ) -> ( Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) -> ( r e. ( Atoms ` K ) -> ( ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) -> X C Y ) ) ) ) ) ) ) )
67 66 rexlimdvv
 |-  ( K e. HL -> ( E. p e. ( Atoms ` K ) E. q e. ( Atoms ` K ) ( p =/= q /\ X = ( p ( join ` K ) q ) ) -> ( ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) -> ( u e. ( Atoms ` K ) -> ( Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) -> ( r e. ( Atoms ` K ) -> ( ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) -> X C Y ) ) ) ) ) ) )
68 67 adantld
 |-  ( K e. HL -> ( ( X e. ( Base ` K ) /\ E. p e. ( Atoms ` K ) E. q e. ( Atoms ` K ) ( p =/= q /\ X = ( p ( join ` K ) q ) ) ) -> ( ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) -> ( u e. ( Atoms ` K ) -> ( Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) -> ( r e. ( Atoms ` K ) -> ( ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) -> X C Y ) ) ) ) ) ) )
69 35 68 sylbid
 |-  ( K e. HL -> ( X e. N -> ( ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) -> ( u e. ( Atoms ` K ) -> ( Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) -> ( r e. ( Atoms ` K ) -> ( ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) -> X C Y ) ) ) ) ) ) )
70 69 imp31
 |-  ( ( ( K e. HL /\ X e. N ) /\ ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) ) -> ( u e. ( Atoms ` K ) -> ( Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) -> ( r e. ( Atoms ` K ) -> ( ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) -> X C Y ) ) ) ) )
71 34 70 syl7
 |-  ( ( ( K e. HL /\ X e. N ) /\ ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) ) -> ( u e. ( Atoms ` K ) -> ( ( s =/= t /\ -. u .<_ ( s ( join ` K ) t ) /\ Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) ) -> ( r e. ( Atoms ` K ) -> ( ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) -> X C Y ) ) ) ) )
72 71 rexlimdv
 |-  ( ( ( K e. HL /\ X e. N ) /\ ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) ) -> ( E. u e. ( Atoms ` K ) ( s =/= t /\ -. u .<_ ( s ( join ` K ) t ) /\ Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) ) -> ( r e. ( Atoms ` K ) -> ( ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) -> X C Y ) ) ) )
73 72 rexlimdvva
 |-  ( ( K e. HL /\ X e. N ) -> ( E. s e. ( Atoms ` K ) E. t e. ( Atoms ` K ) E. u e. ( Atoms ` K ) ( s =/= t /\ -. u .<_ ( s ( join ` K ) t ) /\ Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) ) -> ( r e. ( Atoms ` K ) -> ( ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) -> X C Y ) ) ) )
74 73 adantld
 |-  ( ( K e. HL /\ X e. N ) -> ( ( Y e. ( Base ` K ) /\ E. s e. ( Atoms ` K ) E. t e. ( Atoms ` K ) E. u e. ( Atoms ` K ) ( s =/= t /\ -. u .<_ ( s ( join ` K ) t ) /\ Y = ( ( s ( join ` K ) t ) ( join ` K ) u ) ) ) -> ( r e. ( Atoms ` K ) -> ( ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) -> X C Y ) ) ) )
75 33 74 sylbid
 |-  ( ( K e. HL /\ X e. N ) -> ( Y e. P -> ( r e. ( Atoms ` K ) -> ( ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) -> X C Y ) ) ) )
76 75 3impia
 |-  ( ( K e. HL /\ X e. N /\ Y e. P ) -> ( r e. ( Atoms ` K ) -> ( ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) -> X C Y ) ) )
77 76 rexlimdv
 |-  ( ( K e. HL /\ X e. N /\ Y e. P ) -> ( E. r e. ( Atoms ` K ) ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) -> X C Y ) )
78 77 imp
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ E. r e. ( Atoms ` K ) ( X C ( X ( join ` K ) r ) /\ ( X ( join ` K ) r ) .<_ Y ) ) -> X C Y )
79 31 78 syldan
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ X ( lt ` K ) Y ) -> X C Y )
80 18 79 syldan
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. P ) /\ X .<_ Y ) -> X C Y )