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	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cvlcvr1.j	$⊢ \underset{˙}{\lor} = join (K)$
	cvlcvr1.c	$⊢ C = ⋖_{K}$
	cvlcvr1.a	$⊢ A = Atoms (K)$
Assertion	cvlcvr1	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land X \in B \land P \in A) \to (\neg P \underset{˙}{\leq} X \leftrightarrow X C (X \underset{˙}{\lor} P))$

Proof

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

Metamath Proof Explorer

Theorem cvlcvr1

Proof