Metamath Proof Explorer

Theorem athgt

Description: A Hilbert lattice, whose height is at least 4, has a chain of 4 successively covering atom joins. (Contributed by NM, 3-May-2012)

Ref Expression
Hypotheses athgt.j 
|- .\/ = ( join ` K )
athgt.c 
|- C = (
athgt.a 
|- A = ( Atoms ` K )
Assertion athgt 
|- ( K e. HL -> E. p e. A E. q e. A ( p C ( p .\/ q ) /\ E. r e. A ( ( p .\/ q ) C ( ( p .\/ q ) .\/ r ) /\ E. s e. A ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) )

Proof

Step Hyp Ref Expression
1 athgt.j 
 |-  .\/ = ( join ` K )
2 athgt.c 
 |-  C = (
3 athgt.a 
 |-  A = ( Atoms ` K )
4 eqid 
 |-  ( Base ` K ) = ( Base ` K )
5 eqid 
 |-  ( lt ` K ) = ( lt ` K )
6 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
7 eqid 
 |-  ( 1. ` K ) = ( 1. ` K )
8 4 5 6 7 hlhgt4 
 |-  ( K e. HL -> E. x e. ( Base ` K ) E. y e. ( Base ` K ) E. z e. ( Base ` K ) ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) )
9 simpl1 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) ) -> K e. HL )
10 hlop 
 |-  ( K e. HL -> K e. OP )
11 4 6 op0cl 
 |-  ( K e. OP -> ( 0. ` K ) e. ( Base ` K ) )
12 9 10 11 3syl 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) ) -> ( 0. ` K ) e. ( Base ` K ) )
13 simpl2l 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) ) -> x e. ( Base ` K ) )
14 simprll 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) ) -> ( 0. ` K ) ( lt ` K ) x )
15 eqid 
 |-  ( le ` K ) = ( le ` K )
16 4 15 5 1 2 3 hlrelat3 
 |-  ( ( ( K e. HL /\ ( 0. ` K ) e. ( Base ` K ) /\ x e. ( Base ` K ) ) /\ ( 0. ` K ) ( lt ` K ) x ) -> E. p e. A ( ( 0. ` K ) C ( ( 0. ` K ) .\/ p ) /\ ( ( 0. ` K ) .\/ p ) ( le ` K ) x ) )
17 9 12 13 14 16 syl31anc 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) ) -> E. p e. A ( ( 0. ` K ) C ( ( 0. ` K ) .\/ p ) /\ ( ( 0. ` K ) .\/ p ) ( le ` K ) x ) )
18 simp11 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) /\ p e. A ) -> K e. HL )
19 simp3 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) /\ p e. A ) -> p e. A )
20 6 2 3 atcvr0 
 |-  ( ( K e. HL /\ p e. A ) -> ( 0. ` K ) C p )
21 18 19 20 syl2anc 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) /\ p e. A ) -> ( 0. ` K ) C p )
22 hlol 
 |-  ( K e. HL -> K e. OL )
23 18 22 syl 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) /\ p e. A ) -> K e. OL )
24 4 3 atbase 
 |-  ( p e. A -> p e. ( Base ` K ) )
25 24 3ad2ant3 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) /\ p e. A ) -> p e. ( Base ` K ) )
26 4 1 6 olj02 
 |-  ( ( K e. OL /\ p e. ( Base ` K ) ) -> ( ( 0. ` K ) .\/ p ) = p )
27 23 25 26 syl2anc 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) /\ p e. A ) -> ( ( 0. ` K ) .\/ p ) = p )
28 21 27 breqtrrd 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) /\ p e. A ) -> ( 0. ` K ) C ( ( 0. ` K ) .\/ p ) )
29 28 biantrurd 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) /\ p e. A ) -> ( ( ( 0. ` K ) .\/ p ) ( le ` K ) x <-> ( ( 0. ` K ) C ( ( 0. ` K ) .\/ p ) /\ ( ( 0. ` K ) .\/ p ) ( le ` K ) x ) ) )
30 27 breq1d 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) /\ p e. A ) -> ( ( ( 0. ` K ) .\/ p ) ( le ` K ) x <-> p ( le ` K ) x ) )
31 29 30 bitr3d 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) /\ p e. A ) -> ( ( ( 0. ` K ) C ( ( 0. ` K ) .\/ p ) /\ ( ( 0. ` K ) .\/ p ) ( le ` K ) x ) <-> p ( le ` K ) x ) )
32 31 3expa 
 |-  ( ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) ) /\ p e. A ) -> ( ( ( 0. ` K ) C ( ( 0. ` K ) .\/ p ) /\ ( ( 0. ` K ) .\/ p ) ( le ` K ) x ) <-> p ( le ` K ) x ) )
33 32 rexbidva 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) ) -> ( E. p e. A ( ( 0. ` K ) C ( ( 0. ` K ) .\/ p ) /\ ( ( 0. ` K ) .\/ p ) ( le ` K ) x ) <-> E. p e. A p ( le ` K ) x ) )
34 17 33 mpbid 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) ) -> E. p e. A p ( le ` K ) x )
35 simp11 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) /\ ( p e. A /\ p ( le ` K ) x ) ) -> K e. HL )
36 25 3adant3r 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) /\ ( p e. A /\ p ( le ` K ) x ) ) -> p e. ( Base ` K ) )
37 simp12r 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) /\ ( p e. A /\ p ( le ` K ) x ) ) -> y e. ( Base ` K ) )
38 simp3r 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) /\ ( p e. A /\ p ( le ` K ) x ) ) -> p ( le ` K ) x )
39 simp2lr 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) /\ ( p e. A /\ p ( le ` K ) x ) ) -> x ( lt ` K ) y )
40 hlpos 
 |-  ( K e. HL -> K e. Poset )
41 35 40 syl 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) /\ ( p e. A /\ p ( le ` K ) x ) ) -> K e. Poset )
42 simp12l 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) /\ ( p e. A /\ p ( le ` K ) x ) ) -> x e. ( Base ` K ) )
43 4 15 5 plelttr 
 |-  ( ( K e. Poset /\ ( p e. ( Base ` K ) /\ x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> ( ( p ( le ` K ) x /\ x ( lt ` K ) y ) -> p ( lt ` K ) y ) )
44 41 36 42 37 43 syl13anc 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) /\ ( p e. A /\ p ( le ` K ) x ) ) -> ( ( p ( le ` K ) x /\ x ( lt ` K ) y ) -> p ( lt ` K ) y ) )
45 38 39 44 mp2and 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) /\ ( p e. A /\ p ( le ` K ) x ) ) -> p ( lt ` K ) y )
46 4 15 5 1 2 3 hlrelat3 
 |-  ( ( ( K e. HL /\ p e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ p ( lt ` K ) y ) -> E. q e. A ( p C ( p .\/ q ) /\ ( p .\/ q ) ( le ` K ) y ) )
47 35 36 37 45 46 syl31anc 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) /\ ( p e. A /\ p ( le ` K ) x ) ) -> E. q e. A ( p C ( p .\/ q ) /\ ( p .\/ q ) ( le ` K ) y ) )
48 simp11 
 |-  ( ( ( K e. HL /\ y e. ( Base ` K ) /\ z e. ( Base ` K ) ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) ) -> K e. HL )
49 48 hllatd 
 |-  ( ( ( K e. HL /\ y e. ( Base ` K ) /\ z e. ( Base ` K ) ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) ) -> K e. Lat )
50 simp3ll 
 |-  ( ( ( K e. HL /\ y e. ( Base ` K ) /\ z e. ( Base ` K ) ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) ) -> p e. A )
51 50 24 syl 
 |-  ( ( ( K e. HL /\ y e. ( Base ` K ) /\ z e. ( Base ` K ) ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) ) -> p e. ( Base ` K ) )
52 simp3lr 
 |-  ( ( ( K e. HL /\ y e. ( Base ` K ) /\ z e. ( Base ` K ) ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) ) -> q e. A )
53 4 3 atbase 
 |-  ( q e. A -> q e. ( Base ` K ) )
54 52 53 syl 
 |-  ( ( ( K e. HL /\ y e. ( Base ` K ) /\ z e. ( Base ` K ) ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) ) -> q e. ( Base ` K ) )
55 4 1 latjcl 
 |-  ( ( K e. Lat /\ p e. ( Base ` K ) /\ q e. ( Base ` K ) ) -> ( p .\/ q ) e. ( Base ` K ) )
56 49 51 54 55 syl3anc 
 |-  ( ( ( K e. HL /\ y e. ( Base ` K ) /\ z e. ( Base ` K ) ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) ) -> ( p .\/ q ) e. ( Base ` K ) )
57 simp13 
 |-  ( ( ( K e. HL /\ y e. ( Base ` K ) /\ z e. ( Base ` K ) ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) ) -> z e. ( Base ` K ) )
58 simp3r 
 |-  ( ( ( K e. HL /\ y e. ( Base ` K ) /\ z e. ( Base ` K ) ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) ) -> ( p .\/ q ) ( le ` K ) y )
59 simp2l 
 |-  ( ( ( K e. HL /\ y e. ( Base ` K ) /\ z e. ( Base ` K ) ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) ) -> y ( lt ` K ) z )
60 48 40 syl 
 |-  ( ( ( K e. HL /\ y e. ( Base ` K ) /\ z e. ( Base ` K ) ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) ) -> K e. Poset )
61 simp12 
 |-  ( ( ( K e. HL /\ y e. ( Base ` K ) /\ z e. ( Base ` K ) ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) ) -> y e. ( Base ` K ) )
62 4 15 5 plelttr 
 |-  ( ( K e. Poset /\ ( ( p .\/ q ) e. ( Base ` K ) /\ y e. ( Base ` K ) /\ z e. ( Base ` K ) ) ) -> ( ( ( p .\/ q ) ( le ` K ) y /\ y ( lt ` K ) z ) -> ( p .\/ q ) ( lt ` K ) z ) )
63 60 56 61 57 62 syl13anc 
 |-  ( ( ( K e. HL /\ y e. ( Base ` K ) /\ z e. ( Base ` K ) ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) ) -> ( ( ( p .\/ q ) ( le ` K ) y /\ y ( lt ` K ) z ) -> ( p .\/ q ) ( lt ` K ) z ) )
64 58 59 63 mp2and 
 |-  ( ( ( K e. HL /\ y e. ( Base ` K ) /\ z e. ( Base ` K ) ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) ) -> ( p .\/ q ) ( lt ` K ) z )
65 4 15 5 1 2 3 hlrelat3 
 |-  ( ( ( K e. HL /\ ( p .\/ q ) e. ( Base ` K ) /\ z e. ( Base ` K ) ) /\ ( p .\/ q ) ( lt ` K ) z ) -> E. r e. A ( ( p .\/ q ) C ( ( p .\/ q ) .\/ r ) /\ ( ( p .\/ q ) .\/ r ) ( le ` K ) z ) )
66 48 56 57 64 65 syl31anc 
 |-  ( ( ( K e. HL /\ y e. ( Base ` K ) /\ z e. ( Base ` K ) ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) ) -> E. r e. A ( ( p .\/ q ) C ( ( p .\/ q ) .\/ r ) /\ ( ( p .\/ q ) .\/ r ) ( le ` K ) z ) )
67 simp1ll 
 |-  ( ( ( ( K e. HL /\ z e. ( Base ` K ) ) /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) /\ ( r e. A /\ ( ( p .\/ q ) .\/ r ) ( le ` K ) z ) ) -> K e. HL )
68 67 hllatd 
 |-  ( ( ( ( K e. HL /\ z e. ( Base ` K ) ) /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) /\ ( r e. A /\ ( ( p .\/ q ) .\/ r ) ( le ` K ) z ) ) -> K e. Lat )
69 simp2ll 
 |-  ( ( ( ( K e. HL /\ z e. ( Base ` K ) ) /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) /\ ( r e. A /\ ( ( p .\/ q ) .\/ r ) ( le ` K ) z ) ) -> p e. A )
70 69 24 syl 
 |-  ( ( ( ( K e. HL /\ z e. ( Base ` K ) ) /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) /\ ( r e. A /\ ( ( p .\/ q ) .\/ r ) ( le ` K ) z ) ) -> p e. ( Base ` K ) )
71 simp2lr 
 |-  ( ( ( ( K e. HL /\ z e. ( Base ` K ) ) /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) /\ ( r e. A /\ ( ( p .\/ q ) .\/ r ) ( le ` K ) z ) ) -> q e. A )
72 71 53 syl 
 |-  ( ( ( ( K e. HL /\ z e. ( Base ` K ) ) /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) /\ ( r e. A /\ ( ( p .\/ q ) .\/ r ) ( le ` K ) z ) ) -> q e. ( Base ` K ) )
73 68 70 72 55 syl3anc 
 |-  ( ( ( ( K e. HL /\ z e. ( Base ` K ) ) /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) /\ ( r e. A /\ ( ( p .\/ q ) .\/ r ) ( le ` K ) z ) ) -> ( p .\/ q ) e. ( Base ` K ) )
74 simp3l 
 |-  ( ( ( ( K e. HL /\ z e. ( Base ` K ) ) /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) /\ ( r e. A /\ ( ( p .\/ q ) .\/ r ) ( le ` K ) z ) ) -> r e. A )
75 4 3 atbase 
 |-  ( r e. A -> r e. ( Base ` K ) )
76 74 75 syl 
 |-  ( ( ( ( K e. HL /\ z e. ( Base ` K ) ) /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) /\ ( r e. A /\ ( ( p .\/ q ) .\/ r ) ( le ` K ) z ) ) -> r e. ( Base ` K ) )
77 4 1 latjcl 
 |-  ( ( K e. Lat /\ ( p .\/ q ) e. ( Base ` K ) /\ r e. ( Base ` K ) ) -> ( ( p .\/ q ) .\/ r ) e. ( Base ` K ) )
78 68 73 76 77 syl3anc 
 |-  ( ( ( ( K e. HL /\ z e. ( Base ` K ) ) /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) /\ ( r e. A /\ ( ( p .\/ q ) .\/ r ) ( le ` K ) z ) ) -> ( ( p .\/ q ) .\/ r ) e. ( Base ` K ) )
79 4 7 op1cl 
 |-  ( K e. OP -> ( 1. ` K ) e. ( Base ` K ) )
80 67 10 79 3syl 
 |-  ( ( ( ( K e. HL /\ z e. ( Base ` K ) ) /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) /\ ( r e. A /\ ( ( p .\/ q ) .\/ r ) ( le ` K ) z ) ) -> ( 1. ` K ) e. ( Base ` K ) )
81 simp3r 
 |-  ( ( ( ( K e. HL /\ z e. ( Base ` K ) ) /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) /\ ( r e. A /\ ( ( p .\/ q ) .\/ r ) ( le ` K ) z ) ) -> ( ( p .\/ q ) .\/ r ) ( le ` K ) z )
82 simp1r 
 |-  ( ( ( ( K e. HL /\ z e. ( Base ` K ) ) /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) /\ ( r e. A /\ ( ( p .\/ q ) .\/ r ) ( le ` K ) z ) ) -> z ( lt ` K ) ( 1. ` K ) )
83 67 40 syl 
 |-  ( ( ( ( K e. HL /\ z e. ( Base ` K ) ) /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) /\ ( r e. A /\ ( ( p .\/ q ) .\/ r ) ( le ` K ) z ) ) -> K e. Poset )
84 simp1lr 
 |-  ( ( ( ( K e. HL /\ z e. ( Base ` K ) ) /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) /\ ( r e. A /\ ( ( p .\/ q ) .\/ r ) ( le ` K ) z ) ) -> z e. ( Base ` K ) )
85 4 15 5 plelttr 
 |-  ( ( K e. Poset /\ ( ( ( p .\/ q ) .\/ r ) e. ( Base ` K ) /\ z e. ( Base ` K ) /\ ( 1. ` K ) e. ( Base ` K ) ) ) -> ( ( ( ( p .\/ q ) .\/ r ) ( le ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) -> ( ( p .\/ q ) .\/ r ) ( lt ` K ) ( 1. ` K ) ) )
86 83 78 84 80 85 syl13anc 
 |-  ( ( ( ( K e. HL /\ z e. ( Base ` K ) ) /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) /\ ( r e. A /\ ( ( p .\/ q ) .\/ r ) ( le ` K ) z ) ) -> ( ( ( ( p .\/ q ) .\/ r ) ( le ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) -> ( ( p .\/ q ) .\/ r ) ( lt ` K ) ( 1. ` K ) ) )
87 81 82 86 mp2and 
 |-  ( ( ( ( K e. HL /\ z e. ( Base ` K ) ) /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) /\ ( r e. A /\ ( ( p .\/ q ) .\/ r ) ( le ` K ) z ) ) -> ( ( p .\/ q ) .\/ r ) ( lt ` K ) ( 1. ` K ) )
88 4 15 5 1 2 3 hlrelat3 
 |-  ( ( ( K e. HL /\ ( ( p .\/ q ) .\/ r ) e. ( Base ` K ) /\ ( 1. ` K ) e. ( Base ` K ) ) /\ ( ( p .\/ q ) .\/ r ) ( lt ` K ) ( 1. ` K ) ) -> E. s e. A ( ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) /\ ( ( ( p .\/ q ) .\/ r ) .\/ s ) ( le ` K ) ( 1. ` K ) ) )
89 67 78 80 87 88 syl31anc 
 |-  ( ( ( ( K e. HL /\ z e. ( Base ` K ) ) /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) /\ ( r e. A /\ ( ( p .\/ q ) .\/ r ) ( le ` K ) z ) ) -> E. s e. A ( ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) /\ ( ( ( p .\/ q ) .\/ r ) .\/ s ) ( le ` K ) ( 1. ` K ) ) )
90 simpl 
 |-  ( ( ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) /\ ( ( ( p .\/ q ) .\/ r ) .\/ s ) ( le ` K ) ( 1. ` K ) ) -> ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) )
91 90 reximi 
 |-  ( E. s e. A ( ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) /\ ( ( ( p .\/ q ) .\/ r ) .\/ s ) ( le ` K ) ( 1. ` K ) ) -> E. s e. A ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) )
92 89 91 syl 
 |-  ( ( ( ( K e. HL /\ z e. ( Base ` K ) ) /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) /\ ( r e. A /\ ( ( p .\/ q ) .\/ r ) ( le ` K ) z ) ) -> E. s e. A ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) )
93 92 3exp 
 |-  ( ( ( K e. HL /\ z e. ( Base ` K ) ) /\ z ( lt ` K ) ( 1. ` K ) ) -> ( ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) -> ( ( r e. A /\ ( ( p .\/ q ) .\/ r ) ( le ` K ) z ) -> E. s e. A ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) )
94 93 exp4a 
 |-  ( ( ( K e. HL /\ z e. ( Base ` K ) ) /\ z ( lt ` K ) ( 1. ` K ) ) -> ( ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) -> ( r e. A -> ( ( ( p .\/ q ) .\/ r ) ( le ` K ) z -> E. s e. A ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) ) )
95 94 ex 
 |-  ( ( K e. HL /\ z e. ( Base ` K ) ) -> ( z ( lt ` K ) ( 1. ` K ) -> ( ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) -> ( r e. A -> ( ( ( p .\/ q ) .\/ r ) ( le ` K ) z -> E. s e. A ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) ) ) )
96 95 3adant2 
 |-  ( ( K e. HL /\ y e. ( Base ` K ) /\ z e. ( Base ` K ) ) -> ( z ( lt ` K ) ( 1. ` K ) -> ( ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) -> ( r e. A -> ( ( ( p .\/ q ) .\/ r ) ( le ` K ) z -> E. s e. A ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) ) ) )
97 96 3imp 
 |-  ( ( ( K e. HL /\ y e. ( Base ` K ) /\ z e. ( Base ` K ) ) /\ z ( lt ` K ) ( 1. ` K ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) ) -> ( r e. A -> ( ( ( p .\/ q ) .\/ r ) ( le ` K ) z -> E. s e. A ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) )
98 97 3adant2l 
 |-  ( ( ( K e. HL /\ y e. ( Base ` K ) /\ z e. ( Base ` K ) ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) ) -> ( r e. A -> ( ( ( p .\/ q ) .\/ r ) ( le ` K ) z -> E. s e. A ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) )
99 98 imp 
 |-  ( ( ( ( K e. HL /\ y e. ( Base ` K ) /\ z e. ( Base ` K ) ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) ) /\ r e. A ) -> ( ( ( p .\/ q ) .\/ r ) ( le ` K ) z -> E. s e. A ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) )
100 99 anim2d 
 |-  ( ( ( ( K e. HL /\ y e. ( Base ` K ) /\ z e. ( Base ` K ) ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) ) /\ r e. A ) -> ( ( ( p .\/ q ) C ( ( p .\/ q ) .\/ r ) /\ ( ( p .\/ q ) .\/ r ) ( le ` K ) z ) -> ( ( p .\/ q ) C ( ( p .\/ q ) .\/ r ) /\ E. s e. A ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) )
101 100 reximdva 
 |-  ( ( ( K e. HL /\ y e. ( Base ` K ) /\ z e. ( Base ` K ) ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) ) -> ( E. r e. A ( ( p .\/ q ) C ( ( p .\/ q ) .\/ r ) /\ ( ( p .\/ q ) .\/ r ) ( le ` K ) z ) -> E. r e. A ( ( p .\/ q ) C ( ( p .\/ q ) .\/ r ) /\ E. s e. A ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) )
102 66 101 mpd 
 |-  ( ( ( K e. HL /\ y e. ( Base ` K ) /\ z e. ( Base ` K ) ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) /\ ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) ) -> E. r e. A ( ( p .\/ q ) C ( ( p .\/ q ) .\/ r ) /\ E. s e. A ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) )
103 102 3exp 
 |-  ( ( K e. HL /\ y e. ( Base ` K ) /\ z e. ( Base ` K ) ) -> ( ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) -> ( ( ( p e. A /\ q e. A ) /\ ( p .\/ q ) ( le ` K ) y ) -> E. r e. A ( ( p .\/ q ) C ( ( p .\/ q ) .\/ r ) /\ E. s e. A ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) ) )
104 103 exp4a 
 |-  ( ( K e. HL /\ y e. ( Base ` K ) /\ z e. ( Base ` K ) ) -> ( ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) -> ( ( p e. A /\ q e. A ) -> ( ( p .\/ q ) ( le ` K ) y -> E. r e. A ( ( p .\/ q ) C ( ( p .\/ q ) .\/ r ) /\ E. s e. A ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) ) ) )
105 104 exp4a 
 |-  ( ( K e. HL /\ y e. ( Base ` K ) /\ z e. ( Base ` K ) ) -> ( ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) -> ( p e. A -> ( q e. A -> ( ( p .\/ q ) ( le ` K ) y -> E. r e. A ( ( p .\/ q ) C ( ( p .\/ q ) .\/ r ) /\ E. s e. A ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) ) ) ) )
106 105 3adant2l 
 |-  ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) -> ( ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) -> ( p e. A -> ( q e. A -> ( ( p .\/ q ) ( le ` K ) y -> E. r e. A ( ( p .\/ q ) C ( ( p .\/ q ) .\/ r ) /\ E. s e. A ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) ) ) ) )
107 106 3imp1 
 |-  ( ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) /\ p e. A ) /\ q e. A ) -> ( ( p .\/ q ) ( le ` K ) y -> E. r e. A ( ( p .\/ q ) C ( ( p .\/ q ) .\/ r ) /\ E. s e. A ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) )
108 107 anim2d 
 |-  ( ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) /\ p e. A ) /\ q e. A ) -> ( ( p C ( p .\/ q ) /\ ( p .\/ q ) ( le ` K ) y ) -> ( p C ( p .\/ q ) /\ E. r e. A ( ( p .\/ q ) C ( ( p .\/ q ) .\/ r ) /\ E. s e. A ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) ) )
109 108 reximdva 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) /\ p e. A ) -> ( E. q e. A ( p C ( p .\/ q ) /\ ( p .\/ q ) ( le ` K ) y ) -> E. q e. A ( p C ( p .\/ q ) /\ E. r e. A ( ( p .\/ q ) C ( ( p .\/ q ) .\/ r ) /\ E. s e. A ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) ) )
110 109 3adant2l 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) /\ p e. A ) -> ( E. q e. A ( p C ( p .\/ q ) /\ ( p .\/ q ) ( le ` K ) y ) -> E. q e. A ( p C ( p .\/ q ) /\ E. r e. A ( ( p .\/ q ) C ( ( p .\/ q ) .\/ r ) /\ E. s e. A ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) ) )
111 110 3adant3r 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) /\ ( p e. A /\ p ( le ` K ) x ) ) -> ( E. q e. A ( p C ( p .\/ q ) /\ ( p .\/ q ) ( le ` K ) y ) -> E. q e. A ( p C ( p .\/ q ) /\ E. r e. A ( ( p .\/ q ) C ( ( p .\/ q ) .\/ r ) /\ E. s e. A ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) ) )
112 47 111 mpd 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) /\ ( p e. A /\ p ( le ` K ) x ) ) -> E. q e. A ( p C ( p .\/ q ) /\ E. r e. A ( ( p .\/ q ) C ( ( p .\/ q ) .\/ r ) /\ E. s e. A ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) )
113 112 3expia 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) ) -> ( ( p e. A /\ p ( le ` K ) x ) -> E. q e. A ( p C ( p .\/ q ) /\ E. r e. A ( ( p .\/ q ) C ( ( p .\/ q ) .\/ r ) /\ E. s e. A ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) ) )
114 113 expd 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) ) -> ( p e. A -> ( p ( le ` K ) x -> E. q e. A ( p C ( p .\/ q ) /\ E. r e. A ( ( p .\/ q ) C ( ( p .\/ q ) .\/ r ) /\ E. s e. A ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) ) ) )
115 114 reximdvai 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) ) -> ( E. p e. A p ( le ` K ) x -> E. p e. A E. q e. A ( p C ( p .\/ q ) /\ E. r e. A ( ( p .\/ q ) C ( ( p .\/ q ) .\/ r ) /\ E. s e. A ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) ) )
116 34 115 mpd 
 |-  ( ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) /\ z e. ( Base ` K ) ) /\ ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) ) -> E. p e. A E. q e. A ( p C ( p .\/ q ) /\ E. r e. A ( ( p .\/ q ) C ( ( p .\/ q ) .\/ r ) /\ E. s e. A ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) )
117 116 3exp1 
 |-  ( K e. HL -> ( ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) -> ( z e. ( Base ` K ) -> ( ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) -> E. p e. A E. q e. A ( p C ( p .\/ q ) /\ E. r e. A ( ( p .\/ q ) C ( ( p .\/ q ) .\/ r ) /\ E. s e. A ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) ) ) ) )
118 117 imp 
 |-  ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> ( z e. ( Base ` K ) -> ( ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) -> E. p e. A E. q e. A ( p C ( p .\/ q ) /\ E. r e. A ( ( p .\/ q ) C ( ( p .\/ q ) .\/ r ) /\ E. s e. A ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) ) ) )
119 118 rexlimdv 
 |-  ( ( K e. HL /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> ( E. z e. ( Base ` K ) ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) -> E. p e. A E. q e. A ( p C ( p .\/ q ) /\ E. r e. A ( ( p .\/ q ) C ( ( p .\/ q ) .\/ r ) /\ E. s e. A ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) ) )
120 119 rexlimdvva 
 |-  ( K e. HL -> ( E. x e. ( Base ` K ) E. y e. ( Base ` K ) E. z e. ( Base ` K ) ( ( ( 0. ` K ) ( lt ` K ) x /\ x ( lt ` K ) y ) /\ ( y ( lt ` K ) z /\ z ( lt ` K ) ( 1. ` K ) ) ) -> E. p e. A E. q e. A ( p C ( p .\/ q ) /\ E. r e. A ( ( p .\/ q ) C ( ( p .\/ q ) .\/ r ) /\ E. s e. A ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) ) )
121 8 120 mpd 
 |-  ( K e. HL -> E. p e. A E. q e. A ( p C ( p .\/ q ) /\ E. r e. A ( ( p .\/ q ) C ( ( p .\/ q ) .\/ r ) /\ E. s e. A ( ( p .\/ q ) .\/ r ) C ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) )