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