Metamath Proof Explorer

Theorem cvlcvr1

Description: The covering property. Proposition 1(ii) in Kalmbach p. 140 (and its converse). ( chcv1 analog.) (Contributed by NM, 5-Nov-2012)

Ref Expression
Hypotheses cvlcvr1.b 
|- B = ( Base ` K )
cvlcvr1.l 
|- .<_ = ( le ` K )
cvlcvr1.j 
|- .\/ = ( join ` K )
cvlcvr1.c 
|- C = (
cvlcvr1.a 
|- A = ( Atoms ` K )
Assertion cvlcvr1 
|- ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) -> ( -. P .<_ X <-> X C ( X .\/ P ) ) )

Proof

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