Metamath Proof Explorer

Theorem lhpexle3lem

Description: There exists atom under a co-atom different from any three other atoms. TODO: study if adant*, simp* usage can be improved. (Contributed by NM, 9-Jul-2013)

Ref Expression
Hypotheses lhpex1.l 
|- .<_ = ( le ` K )
lhpex1.a 
|- A = ( Atoms ` K )
lhpex1.h 
|- H = ( LHyp ` K )
Assertion lhpexle3lem 
|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) -> E. p e. A ( p .<_ W /\ ( p =/= X /\ p =/= Y /\ p =/= Z ) ) )

Proof

Step Hyp Ref Expression
1 lhpex1.l 
 |-  .<_ = ( le ` K )
2 lhpex1.a 
 |-  A = ( Atoms ` K )
3 lhpex1.h 
 |-  H = ( LHyp ` K )
4 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X = Y ) -> ( K e. HL /\ W e. H ) )
5 1 2 3 lhpexle2 
 |-  ( ( K e. HL /\ W e. H ) -> E. p e. A ( p .<_ W /\ p =/= X /\ p =/= Z ) )
6 4 5 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X = Y ) -> E. p e. A ( p .<_ W /\ p =/= X /\ p =/= Z ) )
7 simp31 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X = Y ) /\ p e. A /\ ( p .<_ W /\ p =/= X /\ p =/= Z ) ) -> p .<_ W )
8 simp32 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X = Y ) /\ p e. A /\ ( p .<_ W /\ p =/= X /\ p =/= Z ) ) -> p =/= X )
9 simp1r 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X = Y ) /\ p e. A /\ ( p .<_ W /\ p =/= X /\ p =/= Z ) ) -> X = Y )
10 8 9 neeqtrd 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X = Y ) /\ p e. A /\ ( p .<_ W /\ p =/= X /\ p =/= Z ) ) -> p =/= Y )
11 simp33 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X = Y ) /\ p e. A /\ ( p .<_ W /\ p =/= X /\ p =/= Z ) ) -> p =/= Z )
12 8 10 11 3jca 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X = Y ) /\ p e. A /\ ( p .<_ W /\ p =/= X /\ p =/= Z ) ) -> ( p =/= X /\ p =/= Y /\ p =/= Z ) )
13 7 12 jca 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X = Y ) /\ p e. A /\ ( p .<_ W /\ p =/= X /\ p =/= Z ) ) -> ( p .<_ W /\ ( p =/= X /\ p =/= Y /\ p =/= Z ) ) )
14 13 3exp 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X = Y ) -> ( p e. A -> ( ( p .<_ W /\ p =/= X /\ p =/= Z ) -> ( p .<_ W /\ ( p =/= X /\ p =/= Y /\ p =/= Z ) ) ) ) )
15 14 reximdvai 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X = Y ) -> ( E. p e. A ( p .<_ W /\ p =/= X /\ p =/= Z ) -> E. p e. A ( p .<_ W /\ ( p =/= X /\ p =/= Y /\ p =/= Z ) ) ) )
16 6 15 mpd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X = Y ) -> E. p e. A ( p .<_ W /\ ( p =/= X /\ p =/= Y /\ p =/= Z ) ) )
17 simprrr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( -. p .<_ ( X ( join ` K ) Y ) /\ p .<_ W ) ) ) -> p .<_ W )
18 simp11l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ Z .<_ ( X ( join ` K ) Y ) ) -> K e. HL )
19 18 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( -. p .<_ ( X ( join ` K ) Y ) /\ p .<_ W ) ) ) -> K e. HL )
20 19 hllatd 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( -. p .<_ ( X ( join ` K ) Y ) /\ p .<_ W ) ) ) -> K e. Lat )
21 eqid 
 |-  ( Base ` K ) = ( Base ` K )
22 21 2 atbase 
 |-  ( p e. A -> p e. ( Base ` K ) )
23 22 ad2antrl 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( -. p .<_ ( X ( join ` K ) Y ) /\ p .<_ W ) ) ) -> p e. ( Base ` K ) )
24 simp121 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ Z .<_ ( X ( join ` K ) Y ) ) -> X e. A )
25 24 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( -. p .<_ ( X ( join ` K ) Y ) /\ p .<_ W ) ) ) -> X e. A )
26 21 2 atbase 
 |-  ( X e. A -> X e. ( Base ` K ) )
27 25 26 syl 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( -. p .<_ ( X ( join ` K ) Y ) /\ p .<_ W ) ) ) -> X e. ( Base ` K ) )
28 simp122 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ Z .<_ ( X ( join ` K ) Y ) ) -> Y e. A )
29 28 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( -. p .<_ ( X ( join ` K ) Y ) /\ p .<_ W ) ) ) -> Y e. A )
30 21 2 atbase 
 |-  ( Y e. A -> Y e. ( Base ` K ) )
31 29 30 syl 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( -. p .<_ ( X ( join ` K ) Y ) /\ p .<_ W ) ) ) -> Y e. ( Base ` K ) )
32 simprrl 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( -. p .<_ ( X ( join ` K ) Y ) /\ p .<_ W ) ) ) -> -. p .<_ ( X ( join ` K ) Y ) )
33 eqid 
 |-  ( join ` K ) = ( join ` K )
34 21 1 33 latnlej1l 
 |-  ( ( K e. Lat /\ ( p e. ( Base ` K ) /\ X e. ( Base ` K ) /\ Y e. ( Base ` K ) ) /\ -. p .<_ ( X ( join ` K ) Y ) ) -> p =/= X )
35 20 23 27 31 32 34 syl131anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( -. p .<_ ( X ( join ` K ) Y ) /\ p .<_ W ) ) ) -> p =/= X )
36 21 1 33 latnlej1r 
 |-  ( ( K e. Lat /\ ( p e. ( Base ` K ) /\ X e. ( Base ` K ) /\ Y e. ( Base ` K ) ) /\ -. p .<_ ( X ( join ` K ) Y ) ) -> p =/= Y )
37 20 23 27 31 32 36 syl131anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( -. p .<_ ( X ( join ` K ) Y ) /\ p .<_ W ) ) ) -> p =/= Y )
38 simpl3 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( -. p .<_ ( X ( join ` K ) Y ) /\ p .<_ W ) ) ) -> Z .<_ ( X ( join ` K ) Y ) )
39 nbrne2 
 |-  ( ( Z .<_ ( X ( join ` K ) Y ) /\ -. p .<_ ( X ( join ` K ) Y ) ) -> Z =/= p )
40 39 necomd 
 |-  ( ( Z .<_ ( X ( join ` K ) Y ) /\ -. p .<_ ( X ( join ` K ) Y ) ) -> p =/= Z )
41 38 32 40 syl2anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( -. p .<_ ( X ( join ` K ) Y ) /\ p .<_ W ) ) ) -> p =/= Z )
42 35 37 41 3jca 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( -. p .<_ ( X ( join ` K ) Y ) /\ p .<_ W ) ) ) -> ( p =/= X /\ p =/= Y /\ p =/= Z ) )
43 17 42 jca 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( -. p .<_ ( X ( join ` K ) Y ) /\ p .<_ W ) ) ) -> ( p .<_ W /\ ( p =/= X /\ p =/= Y /\ p =/= Z ) ) )
44 simp11 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ Z .<_ ( X ( join ` K ) Y ) ) -> ( K e. HL /\ W e. H ) )
45 simp131 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ Z .<_ ( X ( join ` K ) Y ) ) -> X .<_ W )
46 simp132 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ Z .<_ ( X ( join ` K ) Y ) ) -> Y .<_ W )
47 eqid 
 |-  ( lt ` K ) = ( lt ` K )
48 1 47 33 2 3 lhp2lt 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) -> ( X ( join ` K ) Y ) ( lt ` K ) W )
49 44 24 45 28 46 48 syl122anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ Z .<_ ( X ( join ` K ) Y ) ) -> ( X ( join ` K ) Y ) ( lt ` K ) W )
50 21 33 2 hlatjcl 
 |-  ( ( K e. HL /\ X e. A /\ Y e. A ) -> ( X ( join ` K ) Y ) e. ( Base ` K ) )
51 18 24 28 50 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ Z .<_ ( X ( join ` K ) Y ) ) -> ( X ( join ` K ) Y ) e. ( Base ` K ) )
52 simp11r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ Z .<_ ( X ( join ` K ) Y ) ) -> W e. H )
53 21 3 lhpbase 
 |-  ( W e. H -> W e. ( Base ` K ) )
54 52 53 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ Z .<_ ( X ( join ` K ) Y ) ) -> W e. ( Base ` K ) )
55 21 1 47 2 hlrelat1 
 |-  ( ( K e. HL /\ ( X ( join ` K ) Y ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( X ( join ` K ) Y ) ( lt ` K ) W -> E. p e. A ( -. p .<_ ( X ( join ` K ) Y ) /\ p .<_ W ) ) )
56 18 51 54 55 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ Z .<_ ( X ( join ` K ) Y ) ) -> ( ( X ( join ` K ) Y ) ( lt ` K ) W -> E. p e. A ( -. p .<_ ( X ( join ` K ) Y ) /\ p .<_ W ) ) )
57 49 56 mpd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ Z .<_ ( X ( join ` K ) Y ) ) -> E. p e. A ( -. p .<_ ( X ( join ` K ) Y ) /\ p .<_ W ) )
58 43 57 reximddv 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ Z .<_ ( X ( join ` K ) Y ) ) -> E. p e. A ( p .<_ W /\ ( p =/= X /\ p =/= Y /\ p =/= Z ) ) )
59 58 3expa 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y ) /\ Z .<_ ( X ( join ` K ) Y ) ) -> E. p e. A ( p .<_ W /\ ( p =/= X /\ p =/= Y /\ p =/= Z ) ) )
60 simp11l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ -. Z .<_ ( X ( join ` K ) Y ) ) -> K e. HL )
61 60 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ -. Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> K e. HL )
62 61 hllatd 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ -. Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> K e. Lat )
63 22 ad2antrl 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ -. Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> p e. ( Base ` K ) )
64 simp121 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ -. Z .<_ ( X ( join ` K ) Y ) ) -> X e. A )
65 64 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ -. Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> X e. A )
66 simp122 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ -. Z .<_ ( X ( join ` K ) Y ) ) -> Y e. A )
67 66 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ -. Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> Y e. A )
68 61 65 67 50 syl3anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ -. Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> ( X ( join ` K ) Y ) e. ( Base ` K ) )
69 simp11r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ -. Z .<_ ( X ( join ` K ) Y ) ) -> W e. H )
70 69 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ -. Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> W e. H )
71 70 53 syl 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ -. Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> W e. ( Base ` K ) )
72 simprr3 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ -. Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> p .<_ ( X ( join ` K ) Y ) )
73 simp131 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ -. Z .<_ ( X ( join ` K ) Y ) ) -> X .<_ W )
74 73 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ -. Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> X .<_ W )
75 simp132 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ -. Z .<_ ( X ( join ` K ) Y ) ) -> Y .<_ W )
76 75 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ -. Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> Y .<_ W )
77 65 26 syl 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ -. Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> X e. ( Base ` K ) )
78 67 30 syl 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ -. Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> Y e. ( Base ` K ) )
79 21 1 33 latjle12 
 |-  ( ( K e. Lat /\ ( X e. ( Base ` K ) /\ Y e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( X .<_ W /\ Y .<_ W ) <-> ( X ( join ` K ) Y ) .<_ W ) )
80 62 77 78 71 79 syl13anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ -. Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> ( ( X .<_ W /\ Y .<_ W ) <-> ( X ( join ` K ) Y ) .<_ W ) )
81 74 76 80 mpbi2and 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ -. Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> ( X ( join ` K ) Y ) .<_ W )
82 21 1 62 63 68 71 72 81 lattrd 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ -. Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> p .<_ W )
83 simprr1 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ -. Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> p =/= X )
84 simprr2 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ -. Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> p =/= Y )
85 simpl3 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ -. Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> -. Z .<_ ( X ( join ` K ) Y ) )
86 nbrne2 
 |-  ( ( p .<_ ( X ( join ` K ) Y ) /\ -. Z .<_ ( X ( join ` K ) Y ) ) -> p =/= Z )
87 72 85 86 syl2anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ -. Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> p =/= Z )
88 83 84 87 3jca 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ -. Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> ( p =/= X /\ p =/= Y /\ p =/= Z ) )
89 82 88 jca 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ -. Z .<_ ( X ( join ` K ) Y ) ) /\ ( p e. A /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> ( p .<_ W /\ ( p =/= X /\ p =/= Y /\ p =/= Z ) ) )
90 simp2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ -. Z .<_ ( X ( join ` K ) Y ) ) -> X =/= Y )
91 1 33 2 hlsupr 
 |-  ( ( ( K e. HL /\ X e. A /\ Y e. A ) /\ X =/= Y ) -> E. p e. A ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) )
92 60 64 66 90 91 syl31anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ -. Z .<_ ( X ( join ` K ) Y ) ) -> E. p e. A ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) )
93 89 92 reximddv 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y /\ -. Z .<_ ( X ( join ` K ) Y ) ) -> E. p e. A ( p .<_ W /\ ( p =/= X /\ p =/= Y /\ p =/= Z ) ) )
94 93 3expa 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y ) /\ -. Z .<_ ( X ( join ` K ) Y ) ) -> E. p e. A ( p .<_ W /\ ( p =/= X /\ p =/= Y /\ p =/= Z ) ) )
95 59 94 pm2.61dan 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) /\ X =/= Y ) -> E. p e. A ( p .<_ W /\ ( p =/= X /\ p =/= Y /\ p =/= Z ) ) )
96 16 95 pm2.61dane 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) -> E. p e. A ( p .<_ W /\ ( p =/= X /\ p =/= Y /\ p =/= Z ) ) )