Step |
Hyp |
Ref |
Expression |
1 |
|
cvlcvr1.b |
|- B = ( Base ` K ) |
2 |
|
cvlcvr1.l |
|- .<_ = ( le ` K ) |
3 |
|
cvlcvr1.j |
|- .\/ = ( join ` K ) |
4 |
|
cvlcvr1.c |
|- C = ( |
5 |
|
cvlcvr1.a |
|- A = ( Atoms ` K ) |
6 |
|
simp13 |
|- ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) -> K e. CvLat ) |
7 |
|
cvllat |
|- ( K e. CvLat -> K e. Lat ) |
8 |
6 7
|
syl |
|- ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) -> K e. Lat ) |
9 |
|
simp2 |
|- ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) -> X e. B ) |
10 |
1 5
|
atbase |
|- ( P e. A -> P e. B ) |
11 |
10
|
3ad2ant3 |
|- ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) -> P e. B ) |
12 |
|
eqid |
|- ( lt ` K ) = ( lt ` K ) |
13 |
1 2 12 3
|
latnle |
|- ( ( K e. Lat /\ X e. B /\ P e. B ) -> ( -. P .<_ X <-> X ( lt ` K ) ( X .\/ P ) ) ) |
14 |
8 9 11 13
|
syl3anc |
|- ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) -> ( -. P .<_ X <-> X ( lt ` K ) ( X .\/ P ) ) ) |
15 |
14
|
biimpd |
|- ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) -> ( -. P .<_ X -> X ( lt ` K ) ( X .\/ P ) ) ) |
16 |
|
simpl13 |
|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) -> K e. CvLat ) |
17 |
16 7
|
syl |
|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) -> K e. Lat ) |
18 |
|
simprll |
|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) -> z e. B ) |
19 |
|
simpl2 |
|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) -> X e. B ) |
20 |
|
simpl3 |
|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) -> P e. A ) |
21 |
20 10
|
syl |
|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) -> P e. B ) |
22 |
1 3
|
latjcl |
|- ( ( K e. Lat /\ X e. B /\ P e. B ) -> ( X .\/ P ) e. B ) |
23 |
17 19 21 22
|
syl3anc |
|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) -> ( X .\/ P ) e. B ) |
24 |
|
simprrr |
|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) -> z .<_ ( X .\/ P ) ) |
25 |
|
simprrl |
|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) -> X ( lt ` K ) z ) |
26 |
|
simpl11 |
|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) -> K e. OML ) |
27 |
|
simpl12 |
|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) -> K e. CLat ) |
28 |
|
cvlatl |
|- ( K e. CvLat -> K e. AtLat ) |
29 |
16 28
|
syl |
|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) -> K e. AtLat ) |
30 |
1 2 12 5
|
atlrelat1 |
|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ z e. B ) -> ( X ( lt ` K ) z -> E. q e. A ( -. q .<_ X /\ q .<_ z ) ) ) |
31 |
26 27 29 19 18 30
|
syl311anc |
|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) -> ( X ( lt ` K ) z -> E. q e. A ( -. q .<_ X /\ q .<_ z ) ) ) |
32 |
25 31
|
mpd |
|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) -> E. q e. A ( -. q .<_ X /\ q .<_ z ) ) |
33 |
17
|
adantr |
|- ( ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) /\ ( q e. A /\ ( -. q .<_ X /\ q .<_ z ) ) ) -> K e. Lat ) |
34 |
1 5
|
atbase |
|- ( q e. A -> q e. B ) |
35 |
34
|
ad2antrl |
|- ( ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) /\ ( q e. A /\ ( -. q .<_ X /\ q .<_ z ) ) ) -> q e. B ) |
36 |
18
|
adantr |
|- ( ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) /\ ( q e. A /\ ( -. q .<_ X /\ q .<_ z ) ) ) -> z e. B ) |
37 |
23
|
adantr |
|- ( ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) /\ ( q e. A /\ ( -. q .<_ X /\ q .<_ z ) ) ) -> ( X .\/ P ) e. B ) |
38 |
|
simprrr |
|- ( ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) /\ ( q e. A /\ ( -. q .<_ X /\ q .<_ z ) ) ) -> q .<_ z ) |
39 |
24
|
adantr |
|- ( ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) /\ ( q e. A /\ ( -. q .<_ X /\ q .<_ z ) ) ) -> z .<_ ( X .\/ P ) ) |
40 |
1 2 33 35 36 37 38 39
|
lattrd |
|- ( ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) /\ ( q e. A /\ ( -. q .<_ X /\ q .<_ z ) ) ) -> q .<_ ( X .\/ P ) ) |
41 |
16
|
adantr |
|- ( ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) /\ ( q e. A /\ ( -. q .<_ X /\ q .<_ z ) ) ) -> K e. CvLat ) |
42 |
|
simprl |
|- ( ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) /\ ( q e. A /\ ( -. q .<_ X /\ q .<_ z ) ) ) -> q e. A ) |
43 |
|
simpll3 |
|- ( ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) /\ ( q e. A /\ ( -. q .<_ X /\ q .<_ z ) ) ) -> P e. A ) |
44 |
|
simpll2 |
|- ( ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) /\ ( q e. A /\ ( -. q .<_ X /\ q .<_ z ) ) ) -> X e. B ) |
45 |
|
simprrl |
|- ( ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) /\ ( q e. A /\ ( -. q .<_ X /\ q .<_ z ) ) ) -> -. q .<_ X ) |
46 |
1 2 3 5
|
cvlexch1 |
|- ( ( K e. CvLat /\ ( q e. A /\ P e. A /\ X e. B ) /\ -. q .<_ X ) -> ( q .<_ ( X .\/ P ) -> P .<_ ( X .\/ q ) ) ) |
47 |
41 42 43 44 45 46
|
syl131anc |
|- ( ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) /\ ( q e. A /\ ( -. q .<_ X /\ q .<_ z ) ) ) -> ( q .<_ ( X .\/ P ) -> P .<_ ( X .\/ q ) ) ) |
48 |
40 47
|
mpd |
|- ( ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) /\ ( q e. A /\ ( -. q .<_ X /\ q .<_ z ) ) ) -> P .<_ ( X .\/ q ) ) |
49 |
|
simprlr |
|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) -> -. P .<_ X ) |
50 |
49
|
adantr |
|- ( ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) /\ ( q e. A /\ ( -. q .<_ X /\ q .<_ z ) ) ) -> -. P .<_ X ) |
51 |
1 2 3 5
|
cvlexchb1 |
|- ( ( K e. CvLat /\ ( P e. A /\ q e. A /\ X e. B ) /\ -. P .<_ X ) -> ( P .<_ ( X .\/ q ) <-> ( X .\/ P ) = ( X .\/ q ) ) ) |
52 |
41 43 42 44 50 51
|
syl131anc |
|- ( ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) /\ ( q e. A /\ ( -. q .<_ X /\ q .<_ z ) ) ) -> ( P .<_ ( X .\/ q ) <-> ( X .\/ P ) = ( X .\/ q ) ) ) |
53 |
48 52
|
mpbid |
|- ( ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) /\ ( q e. A /\ ( -. q .<_ X /\ q .<_ z ) ) ) -> ( X .\/ P ) = ( X .\/ q ) ) |
54 |
2 12
|
pltle |
|- ( ( K e. OML /\ X e. B /\ z e. B ) -> ( X ( lt ` K ) z -> X .<_ z ) ) |
55 |
26 19 18 54
|
syl3anc |
|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) -> ( X ( lt ` K ) z -> X .<_ z ) ) |
56 |
25 55
|
mpd |
|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) -> X .<_ z ) |
57 |
56
|
adantr |
|- ( ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) /\ ( q e. A /\ ( -. q .<_ X /\ q .<_ z ) ) ) -> X .<_ z ) |
58 |
1 2 3
|
latjle12 |
|- ( ( K e. Lat /\ ( X e. B /\ q e. B /\ z e. B ) ) -> ( ( X .<_ z /\ q .<_ z ) <-> ( X .\/ q ) .<_ z ) ) |
59 |
33 44 35 36 58
|
syl13anc |
|- ( ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) /\ ( q e. A /\ ( -. q .<_ X /\ q .<_ z ) ) ) -> ( ( X .<_ z /\ q .<_ z ) <-> ( X .\/ q ) .<_ z ) ) |
60 |
57 38 59
|
mpbi2and |
|- ( ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) /\ ( q e. A /\ ( -. q .<_ X /\ q .<_ z ) ) ) -> ( X .\/ q ) .<_ z ) |
61 |
53 60
|
eqbrtrd |
|- ( ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) /\ ( q e. A /\ ( -. q .<_ X /\ q .<_ z ) ) ) -> ( X .\/ P ) .<_ z ) |
62 |
32 61
|
rexlimddv |
|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) -> ( X .\/ P ) .<_ z ) |
63 |
1 2 17 18 23 24 62
|
latasymd |
|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ ( ( z e. B /\ -. P .<_ X ) /\ ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) ) ) -> z = ( X .\/ P ) ) |
64 |
63
|
exp44 |
|- ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) -> ( z e. B -> ( -. P .<_ X -> ( ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) -> z = ( X .\/ P ) ) ) ) ) |
65 |
64
|
imp |
|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ z e. B ) -> ( -. P .<_ X -> ( ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) -> z = ( X .\/ P ) ) ) ) |
66 |
65
|
ralrimdva |
|- ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) -> ( -. P .<_ X -> A. z e. B ( ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) -> z = ( X .\/ P ) ) ) ) |
67 |
15 66
|
jcad |
|- ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) -> ( -. P .<_ X -> ( X ( lt ` K ) ( X .\/ P ) /\ A. z e. B ( ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) -> z = ( X .\/ P ) ) ) ) ) |
68 |
8 9 11 22
|
syl3anc |
|- ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) -> ( X .\/ P ) e. B ) |
69 |
1 2 12 4
|
cvrval2 |
|- ( ( K e. Lat /\ X e. B /\ ( X .\/ P ) e. B ) -> ( X C ( X .\/ P ) <-> ( X ( lt ` K ) ( X .\/ P ) /\ A. z e. B ( ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) -> z = ( X .\/ P ) ) ) ) ) |
70 |
8 9 68 69
|
syl3anc |
|- ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) -> ( X C ( X .\/ P ) <-> ( X ( lt ` K ) ( X .\/ P ) /\ A. z e. B ( ( X ( lt ` K ) z /\ z .<_ ( X .\/ P ) ) -> z = ( X .\/ P ) ) ) ) ) |
71 |
67 70
|
sylibrd |
|- ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) -> ( -. P .<_ X -> X C ( X .\/ P ) ) ) |
72 |
8
|
adantr |
|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ X C ( X .\/ P ) ) -> K e. Lat ) |
73 |
|
simpl2 |
|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ X C ( X .\/ P ) ) -> X e. B ) |
74 |
68
|
adantr |
|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ X C ( X .\/ P ) ) -> ( X .\/ P ) e. B ) |
75 |
|
simpr |
|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ X C ( X .\/ P ) ) -> X C ( X .\/ P ) ) |
76 |
1 12 4
|
cvrlt |
|- ( ( ( K e. Lat /\ X e. B /\ ( X .\/ P ) e. B ) /\ X C ( X .\/ P ) ) -> X ( lt ` K ) ( X .\/ P ) ) |
77 |
72 73 74 75 76
|
syl31anc |
|- ( ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) /\ X C ( X .\/ P ) ) -> X ( lt ` K ) ( X .\/ P ) ) |
78 |
77
|
ex |
|- ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) -> ( X C ( X .\/ P ) -> X ( lt ` K ) ( X .\/ P ) ) ) |
79 |
78 14
|
sylibrd |
|- ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) -> ( X C ( X .\/ P ) -> -. P .<_ X ) ) |
80 |
71 79
|
impbid |
|- ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) -> ( -. P .<_ X <-> X C ( X .\/ P ) ) ) |