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 ) ) ) ) |