cvrexchlem

Description: Lemma for cvrexch . ( cvexchlem analog.) (Contributed by NM, 18-Nov-2011)

	Ref	Expression
Hypotheses	cvrexch.b	$⊢ B = {Base}_{K}$
	cvrexch.j	$⊢ \underset{˙}{\lor} = join (K)$
	cvrexch.m	$⊢ \underset{˙}{\land} = meet (K)$
	cvrexch.c	$⊢ C = ⋖_{K}$
Assertion	cvrexchlem	$⊢ (K \in HL \land X \in B \land Y \in B) \to ((X \underset{˙}{\land} Y) C Y \to X C (X \underset{˙}{\lor} Y))$

Proof

Step	Hyp	Ref	Expression
1		cvrexch.b	$⊢ B = {Base}_{K}$
2		cvrexch.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cvrexch.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cvrexch.c	$⊢ C = ⋖_{K}$
5		hllat	$⊢ K \in HL \to K \in Lat$
6	1 3	latmcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y \in B$
7	5 6	syl3an1	$⊢ (K \in HL \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y \in B$
8		eqid	$⊢ <_{K} = <_{K}$
9	1 8 4	cvrlt	$⊢ ((K \in HL \land X \underset{˙}{\land} Y \in B \land Y \in B) \land (X \underset{˙}{\land} Y) C Y) \to (X \underset{˙}{\land} Y) <_{K} Y$
10	9	ex	$⊢ (K \in HL \land X \underset{˙}{\land} Y \in B \land Y \in B) \to ((X \underset{˙}{\land} Y) C Y \to (X \underset{˙}{\land} Y) <_{K} Y)$
11	7 10	syld3an2	$⊢ (K \in HL \land X \in B \land Y \in B) \to ((X \underset{˙}{\land} Y) C Y \to (X \underset{˙}{\land} Y) <_{K} Y)$
12		eqid	$⊢ \leq_{K} = \leq_{K}$
13		eqid	$⊢ Atoms (K) = Atoms (K)$
14	1 12 8 13	hlrelat1	$⊢ (K \in HL \land X \underset{˙}{\land} Y \in B \land Y \in B) \to ((X \underset{˙}{\land} Y) <_{K} Y \to \exists p \in Atoms (K) (\neg p \leq_{K} (X \underset{˙}{\land} Y) \land p \leq_{K} Y))$
15	7 14	syld3an2	$⊢ (K \in HL \land X \in B \land Y \in B) \to ((X \underset{˙}{\land} Y) <_{K} Y \to \exists p \in Atoms (K) (\neg p \leq_{K} (X \underset{˙}{\land} Y) \land p \leq_{K} Y))$
16	11 15	syld	$⊢ (K \in HL \land X \in B \land Y \in B) \to ((X \underset{˙}{\land} Y) C Y \to \exists p \in Atoms (K) (\neg p \leq_{K} (X \underset{˙}{\land} Y) \land p \leq_{K} Y))$
17	16	imp	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) C Y) \to \exists p \in Atoms (K) (\neg p \leq_{K} (X \underset{˙}{\land} Y) \land p \leq_{K} Y)$
18		simpl1	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in Atoms (K)) \to K \in HL$
19	18	hllatd	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in Atoms (K)) \to K \in Lat$
20	1 13	atbase	$⊢ p \in Atoms (K) \to p \in B$
21	20	adantl	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in Atoms (K)) \to p \in B$
22		simpl2	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in Atoms (K)) \to X \in B$
23		simpl3	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in Atoms (K)) \to Y \in B$
24	1 12 3	latlem12	$⊢ (K \in Lat \land (p \in B \land X \in B \land Y \in B)) \to ((p \leq_{K} X \land p \leq_{K} Y) \leftrightarrow p \leq_{K} (X \underset{˙}{\land} Y))$
25	19 21 22 23 24	syl13anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in Atoms (K)) \to ((p \leq_{K} X \land p \leq_{K} Y) \leftrightarrow p \leq_{K} (X \underset{˙}{\land} Y))$
26	25	biimpd	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in Atoms (K)) \to ((p \leq_{K} X \land p \leq_{K} Y) \to p \leq_{K} (X \underset{˙}{\land} Y))$
27	26	expcomd	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in Atoms (K)) \to (p \leq_{K} Y \to (p \leq_{K} X \to p \leq_{K} (X \underset{˙}{\land} Y)))$
28		con3	$⊢ (p \leq_{K} X \to p \leq_{K} (X \underset{˙}{\land} Y)) \to (\neg p \leq_{K} (X \underset{˙}{\land} Y) \to \neg p \leq_{K} X)$
29	27 28	syl6	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in Atoms (K)) \to (p \leq_{K} Y \to (\neg p \leq_{K} (X \underset{˙}{\land} Y) \to \neg p \leq_{K} X))$
30	29	com23	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in Atoms (K)) \to (\neg p \leq_{K} (X \underset{˙}{\land} Y) \to (p \leq_{K} Y \to \neg p \leq_{K} X))$
31	30	a1d	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in Atoms (K)) \to ((X \underset{˙}{\land} Y) C Y \to (\neg p \leq_{K} (X \underset{˙}{\land} Y) \to (p \leq_{K} Y \to \neg p \leq_{K} X)))$
32	31	imp4d	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in Atoms (K)) \to (((X \underset{˙}{\land} Y) C Y \land (\neg p \leq_{K} (X \underset{˙}{\land} Y) \land p \leq_{K} Y)) \to \neg p \leq_{K} X)$
33		simpr	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in Atoms (K)) \to p \in Atoms (K)$
34	1 12 2 4 13	cvr1	$⊢ (K \in HL \land X \in B \land p \in Atoms (K)) \to (\neg p \leq_{K} X \leftrightarrow X C (X \underset{˙}{\lor} p))$
35	18 22 33 34	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in Atoms (K)) \to (\neg p \leq_{K} X \leftrightarrow X C (X \underset{˙}{\lor} p))$
36	32 35	sylibd	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in Atoms (K)) \to (((X \underset{˙}{\land} Y) C Y \land (\neg p \leq_{K} (X \underset{˙}{\land} Y) \land p \leq_{K} Y)) \to X C (X \underset{˙}{\lor} p))$
37	36	imp	$⊢ (((K \in HL \land X \in B \land Y \in B) \land p \in Atoms (K)) \land ((X \underset{˙}{\land} Y) C Y \land (\neg p \leq_{K} (X \underset{˙}{\land} Y) \land p \leq_{K} Y))) \to X C (X \underset{˙}{\lor} p)$
38		simpl1	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in B) \to K \in HL$
39	38	hllatd	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in B) \to K \in Lat$
40		simpl2	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in B) \to X \in B$
41		simpl3	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in B) \to Y \in B$
42	39 40 41 6	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in B) \to X \underset{˙}{\land} Y \in B$
43		simpr	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in B) \to p \in B$
44	1 2	latjass	$⊢ (K \in Lat \land (X \in B \land X \underset{˙}{\land} Y \in B \land p \in B)) \to (X \underset{˙}{\lor} (X \underset{˙}{\land} Y)) \underset{˙}{\lor} p = X \underset{˙}{\lor} ((X \underset{˙}{\land} Y) \underset{˙}{\lor} p)$
45	39 40 42 43 44	syl13anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in B) \to (X \underset{˙}{\lor} (X \underset{˙}{\land} Y)) \underset{˙}{\lor} p = X \underset{˙}{\lor} ((X \underset{˙}{\land} Y) \underset{˙}{\lor} p)$
46	1 2 3	latabs1	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\lor} (X \underset{˙}{\land} Y) = X$
47	5 46	syl3an1	$⊢ (K \in HL \land X \in B \land Y \in B) \to X \underset{˙}{\lor} (X \underset{˙}{\land} Y) = X$
48	47	adantr	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in B) \to X \underset{˙}{\lor} (X \underset{˙}{\land} Y) = X$
49	48	oveq1d	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in B) \to (X \underset{˙}{\lor} (X \underset{˙}{\land} Y)) \underset{˙}{\lor} p = X \underset{˙}{\lor} p$
50	45 49	eqtr3d	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in B) \to X \underset{˙}{\lor} ((X \underset{˙}{\land} Y) \underset{˙}{\lor} p) = X \underset{˙}{\lor} p$
51	50	adantr	$⊢ (((K \in HL \land X \in B \land Y \in B) \land p \in B) \land ((X \underset{˙}{\land} Y) C Y \land (\neg p \leq_{K} (X \underset{˙}{\land} Y) \land p \leq_{K} Y))) \to X \underset{˙}{\lor} ((X \underset{˙}{\land} Y) \underset{˙}{\lor} p) = X \underset{˙}{\lor} p$
52	1 12 8 2	latnle	$⊢ (K \in Lat \land X \underset{˙}{\land} Y \in B \land p \in B) \to (\neg p \leq_{K} (X \underset{˙}{\land} Y) \leftrightarrow (X \underset{˙}{\land} Y) <_{K} ((X \underset{˙}{\land} Y) \underset{˙}{\lor} p))$
53	39 42 43 52	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in B) \to (\neg p \leq_{K} (X \underset{˙}{\land} Y) \leftrightarrow (X \underset{˙}{\land} Y) <_{K} ((X \underset{˙}{\land} Y) \underset{˙}{\lor} p))$
54	1 12 3	latmle2	$⊢ (K \in Lat \land X \in B \land Y \in B) \to (X \underset{˙}{\land} Y) \leq_{K} Y$
55	39 40 41 54	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in B) \to (X \underset{˙}{\land} Y) \leq_{K} Y$
56	55	biantrurd	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in B) \to (p \leq_{K} Y \leftrightarrow ((X \underset{˙}{\land} Y) \leq_{K} Y \land p \leq_{K} Y))$
57	1 12 2	latjle12	$⊢ (K \in Lat \land (X \underset{˙}{\land} Y \in B \land p \in B \land Y \in B)) \to (((X \underset{˙}{\land} Y) \leq_{K} Y \land p \leq_{K} Y) \leftrightarrow ((X \underset{˙}{\land} Y) \underset{˙}{\lor} p) \leq_{K} Y)$
58	39 42 43 41 57	syl13anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in B) \to (((X \underset{˙}{\land} Y) \leq_{K} Y \land p \leq_{K} Y) \leftrightarrow ((X \underset{˙}{\land} Y) \underset{˙}{\lor} p) \leq_{K} Y)$
59	56 58	bitrd	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in B) \to (p \leq_{K} Y \leftrightarrow ((X \underset{˙}{\land} Y) \underset{˙}{\lor} p) \leq_{K} Y)$
60	53 59	anbi12d	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in B) \to ((\neg p \leq_{K} (X \underset{˙}{\land} Y) \land p \leq_{K} Y) \leftrightarrow ((X \underset{˙}{\land} Y) <_{K} ((X \underset{˙}{\land} Y) \underset{˙}{\lor} p) \land ((X \underset{˙}{\land} Y) \underset{˙}{\lor} p) \leq_{K} Y))$
61		hlpos	$⊢ K \in HL \to K \in Poset$
62	38 61	syl	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in B) \to K \in Poset$
63	1 2	latjcl	$⊢ (K \in Lat \land X \underset{˙}{\land} Y \in B \land p \in B) \to (X \underset{˙}{\land} Y) \underset{˙}{\lor} p \in B$
64	39 42 43 63	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in B) \to (X \underset{˙}{\land} Y) \underset{˙}{\lor} p \in B$
65	42 41 64	3jca	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in B) \to (X \underset{˙}{\land} Y \in B \land Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\lor} p \in B)$
66	1 12 8 4	cvrnbtwn2	$⊢ (K \in Poset \land (X \underset{˙}{\land} Y \in B \land Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\lor} p \in B) \land (X \underset{˙}{\land} Y) C Y) \to (((X \underset{˙}{\land} Y) <_{K} ((X \underset{˙}{\land} Y) \underset{˙}{\lor} p) \land ((X \underset{˙}{\land} Y) \underset{˙}{\lor} p) \leq_{K} Y) \leftrightarrow (X \underset{˙}{\land} Y) \underset{˙}{\lor} p = Y)$
67	66	biimpd	$⊢ (K \in Poset \land (X \underset{˙}{\land} Y \in B \land Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\lor} p \in B) \land (X \underset{˙}{\land} Y) C Y) \to (((X \underset{˙}{\land} Y) <_{K} ((X \underset{˙}{\land} Y) \underset{˙}{\lor} p) \land ((X \underset{˙}{\land} Y) \underset{˙}{\lor} p) \leq_{K} Y) \to (X \underset{˙}{\land} Y) \underset{˙}{\lor} p = Y)$
68	67	3exp	$⊢ K \in Poset \to ((X \underset{˙}{\land} Y \in B \land Y \in B \land (X \underset{˙}{\land} Y) \underset{˙}{\lor} p \in B) \to ((X \underset{˙}{\land} Y) C Y \to (((X \underset{˙}{\land} Y) <_{K} ((X \underset{˙}{\land} Y) \underset{˙}{\lor} p) \land ((X \underset{˙}{\land} Y) \underset{˙}{\lor} p) \leq_{K} Y) \to (X \underset{˙}{\land} Y) \underset{˙}{\lor} p = Y)))$
69	62 65 68	sylc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in B) \to ((X \underset{˙}{\land} Y) C Y \to (((X \underset{˙}{\land} Y) <_{K} ((X \underset{˙}{\land} Y) \underset{˙}{\lor} p) \land ((X \underset{˙}{\land} Y) \underset{˙}{\lor} p) \leq_{K} Y) \to (X \underset{˙}{\land} Y) \underset{˙}{\lor} p = Y))$
70	69	com23	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in B) \to (((X \underset{˙}{\land} Y) <_{K} ((X \underset{˙}{\land} Y) \underset{˙}{\lor} p) \land ((X \underset{˙}{\land} Y) \underset{˙}{\lor} p) \leq_{K} Y) \to ((X \underset{˙}{\land} Y) C Y \to (X \underset{˙}{\land} Y) \underset{˙}{\lor} p = Y))$
71	60 70	sylbid	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in B) \to ((\neg p \leq_{K} (X \underset{˙}{\land} Y) \land p \leq_{K} Y) \to ((X \underset{˙}{\land} Y) C Y \to (X \underset{˙}{\land} Y) \underset{˙}{\lor} p = Y))$
72	71	com23	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in B) \to ((X \underset{˙}{\land} Y) C Y \to ((\neg p \leq_{K} (X \underset{˙}{\land} Y) \land p \leq_{K} Y) \to (X \underset{˙}{\land} Y) \underset{˙}{\lor} p = Y))$
73	72	imp32	$⊢ (((K \in HL \land X \in B \land Y \in B) \land p \in B) \land ((X \underset{˙}{\land} Y) C Y \land (\neg p \leq_{K} (X \underset{˙}{\land} Y) \land p \leq_{K} Y))) \to (X \underset{˙}{\land} Y) \underset{˙}{\lor} p = Y$
74	73	oveq2d	$⊢ (((K \in HL \land X \in B \land Y \in B) \land p \in B) \land ((X \underset{˙}{\land} Y) C Y \land (\neg p \leq_{K} (X \underset{˙}{\land} Y) \land p \leq_{K} Y))) \to X \underset{˙}{\lor} ((X \underset{˙}{\land} Y) \underset{˙}{\lor} p) = X \underset{˙}{\lor} Y$
75	51 74	eqtr3d	$⊢ (((K \in HL \land X \in B \land Y \in B) \land p \in B) \land ((X \underset{˙}{\land} Y) C Y \land (\neg p \leq_{K} (X \underset{˙}{\land} Y) \land p \leq_{K} Y))) \to X \underset{˙}{\lor} p = X \underset{˙}{\lor} Y$
76	20 75	sylanl2	$⊢ (((K \in HL \land X \in B \land Y \in B) \land p \in Atoms (K)) \land ((X \underset{˙}{\land} Y) C Y \land (\neg p \leq_{K} (X \underset{˙}{\land} Y) \land p \leq_{K} Y))) \to X \underset{˙}{\lor} p = X \underset{˙}{\lor} Y$
77	37 76	breqtrd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land p \in Atoms (K)) \land ((X \underset{˙}{\land} Y) C Y \land (\neg p \leq_{K} (X \underset{˙}{\land} Y) \land p \leq_{K} Y))) \to X C (X \underset{˙}{\lor} Y)$
78	77	expr	$⊢ (((K \in HL \land X \in B \land Y \in B) \land p \in Atoms (K)) \land (X \underset{˙}{\land} Y) C Y) \to ((\neg p \leq_{K} (X \underset{˙}{\land} Y) \land p \leq_{K} Y) \to X C (X \underset{˙}{\lor} Y))$
79	78	an32s	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) C Y) \land p \in Atoms (K)) \to ((\neg p \leq_{K} (X \underset{˙}{\land} Y) \land p \leq_{K} Y) \to X C (X \underset{˙}{\lor} Y))$
80	79	rexlimdva	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) C Y) \to (\exists p \in Atoms (K) (\neg p \leq_{K} (X \underset{˙}{\land} Y) \land p \leq_{K} Y) \to X C (X \underset{˙}{\lor} Y))$
81	17 80	mpd	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (X \underset{˙}{\land} Y) C Y) \to X C (X \underset{˙}{\lor} Y)$
82	81	ex	$⊢ (K \in HL \land X \in B \land Y \in B) \to ((X \underset{˙}{\land} Y) C Y \to X C (X \underset{˙}{\lor} Y))$

Metamath Proof Explorer

Theorem cvrexchlem

Proof