cvrval5

Description: Binary relation expressing X covers X ./\ Y . (Contributed by NM, 7-Dec-2012)

	Ref	Expression
Hypotheses	cvrval5.b	$⊢ B = {Base}_{K}$
	cvrval5.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cvrval5.j	$⊢ \underset{˙}{\lor} = join (K)$
	cvrval5.m	$⊢ \underset{˙}{\land} = meet (K)$
	cvrval5.c	$⊢ C = ⋖_{K}$
	cvrval5.a	$⊢ A = Atoms (K)$
Assertion	cvrval5	$⊢ (K \in HL \land X \in B \land Y \in B) \to ((X \underset{˙}{\land} Y) C X \leftrightarrow \exists p \in A (\neg p \underset{˙}{\leq} Y \land p \underset{˙}{\lor} (X \underset{˙}{\land} Y) = X))$

Proof

Step	Hyp	Ref	Expression
1		cvrval5.b	$⊢ B = {Base}_{K}$
2		cvrval5.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cvrval5.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cvrval5.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cvrval5.c	$⊢ C = ⋖_{K}$
6		cvrval5.a	$⊢ A = Atoms (K)$
7		simp1	$⊢ (K \in HL \land X \in B \land Y \in B) \to K \in HL$
8		hllat	$⊢ K \in HL \to K \in Lat$
9	1 4	latmcl	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y \in B$
10	8 9	syl3an1	$⊢ (K \in HL \land X \in B \land Y \in B) \to X \underset{˙}{\land} Y \in B$
11		simp2	$⊢ (K \in HL \land X \in B \land Y \in B) \to X \in B$
12	1 2 3 5 6	cvrval3	$⊢ (K \in HL \land X \underset{˙}{\land} Y \in B \land X \in B) \to ((X \underset{˙}{\land} Y) C X \leftrightarrow \exists p \in A (\neg p \underset{˙}{\leq} (X \underset{˙}{\land} Y) \land (X \underset{˙}{\land} Y) \underset{˙}{\lor} p = X))$
13	7 10 11 12	syl3anc	$⊢ (K \in HL \land X \in B \land Y \in B) \to ((X \underset{˙}{\land} Y) C X \leftrightarrow \exists p \in A (\neg p \underset{˙}{\leq} (X \underset{˙}{\land} Y) \land (X \underset{˙}{\land} Y) \underset{˙}{\lor} p = X))$
14	8	3ad2ant1	$⊢ (K \in HL \land X \in B \land Y \in B) \to K \in Lat$
15	14	ad2antrr	$⊢ (((K \in HL \land X \in B \land Y \in B) \land p \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\lor} p = X) \to K \in Lat$
16	10	ad2antrr	$⊢ (((K \in HL \land X \in B \land Y \in B) \land p \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\lor} p = X) \to X \underset{˙}{\land} Y \in B$
17	1 6	atbase	$⊢ p \in A \to p \in B$
18	17	ad2antlr	$⊢ (((K \in HL \land X \in B \land Y \in B) \land p \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\lor} p = X) \to p \in B$
19	1 2 3	latlej2	$⊢ (K \in Lat \land X \underset{˙}{\land} Y \in B \land p \in B) \to p \underset{˙}{\leq} ((X \underset{˙}{\land} Y) \underset{˙}{\lor} p)$
20	15 16 18 19	syl3anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land p \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\lor} p = X) \to p \underset{˙}{\leq} ((X \underset{˙}{\land} Y) \underset{˙}{\lor} p)$
21		simpr	$⊢ (((K \in HL \land X \in B \land Y \in B) \land p \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\lor} p = X) \to (X \underset{˙}{\land} Y) \underset{˙}{\lor} p = X$
22	20 21	breqtrd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land p \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\lor} p = X) \to p \underset{˙}{\leq} X$
23	22	biantrurd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land p \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\lor} p = X) \to (p \underset{˙}{\leq} Y \leftrightarrow (p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y))$
24		simpll2	$⊢ (((K \in HL \land X \in B \land Y \in B) \land p \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\lor} p = X) \to X \in B$
25		simpll3	$⊢ (((K \in HL \land X \in B \land Y \in B) \land p \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\lor} p = X) \to Y \in B$
26	1 2 4	latlem12	$⊢ (K \in Lat \land (p \in B \land X \in B \land Y \in B)) \to ((p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y) \leftrightarrow p \underset{˙}{\leq} (X \underset{˙}{\land} Y))$
27	15 18 24 25 26	syl13anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land p \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\lor} p = X) \to ((p \underset{˙}{\leq} X \land p \underset{˙}{\leq} Y) \leftrightarrow p \underset{˙}{\leq} (X \underset{˙}{\land} Y))$
28	23 27	bitr2d	$⊢ (((K \in HL \land X \in B \land Y \in B) \land p \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\lor} p = X) \to (p \underset{˙}{\leq} (X \underset{˙}{\land} Y) \leftrightarrow p \underset{˙}{\leq} Y)$
29	28	notbid	$⊢ (((K \in HL \land X \in B \land Y \in B) \land p \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\lor} p = X) \to (\neg p \underset{˙}{\leq} (X \underset{˙}{\land} Y) \leftrightarrow \neg p \underset{˙}{\leq} Y)$
30	29	ex	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in A) \to ((X \underset{˙}{\land} Y) \underset{˙}{\lor} p = X \to (\neg p \underset{˙}{\leq} (X \underset{˙}{\land} Y) \leftrightarrow \neg p \underset{˙}{\leq} Y))$
31	30	pm5.32rd	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in A) \to ((\neg p \underset{˙}{\leq} (X \underset{˙}{\land} Y) \land (X \underset{˙}{\land} Y) \underset{˙}{\lor} p = X) \leftrightarrow (\neg p \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\lor} p = X))$
32	14	adantr	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in A) \to K \in Lat$
33	10	adantr	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in A) \to X \underset{˙}{\land} Y \in B$
34	17	adantl	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in A) \to p \in B$
35	1 3	latjcom	$⊢ (K \in Lat \land X \underset{˙}{\land} Y \in B \land p \in B) \to (X \underset{˙}{\land} Y) \underset{˙}{\lor} p = p \underset{˙}{\lor} (X \underset{˙}{\land} Y)$
36	32 33 34 35	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in A) \to (X \underset{˙}{\land} Y) \underset{˙}{\lor} p = p \underset{˙}{\lor} (X \underset{˙}{\land} Y)$
37	36	eqeq1d	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in A) \to ((X \underset{˙}{\land} Y) \underset{˙}{\lor} p = X \leftrightarrow p \underset{˙}{\lor} (X \underset{˙}{\land} Y) = X)$
38	37	anbi2d	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in A) \to ((\neg p \underset{˙}{\leq} Y \land (X \underset{˙}{\land} Y) \underset{˙}{\lor} p = X) \leftrightarrow (\neg p \underset{˙}{\leq} Y \land p \underset{˙}{\lor} (X \underset{˙}{\land} Y) = X))$
39	31 38	bitrd	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in A) \to ((\neg p \underset{˙}{\leq} (X \underset{˙}{\land} Y) \land (X \underset{˙}{\land} Y) \underset{˙}{\lor} p = X) \leftrightarrow (\neg p \underset{˙}{\leq} Y \land p \underset{˙}{\lor} (X \underset{˙}{\land} Y) = X))$
40	39	rexbidva	$⊢ (K \in HL \land X \in B \land Y \in B) \to (\exists p \in A (\neg p \underset{˙}{\leq} (X \underset{˙}{\land} Y) \land (X \underset{˙}{\land} Y) \underset{˙}{\lor} p = X) \leftrightarrow \exists p \in A (\neg p \underset{˙}{\leq} Y \land p \underset{˙}{\lor} (X \underset{˙}{\land} Y) = X))$
41	13 40	bitrd	$⊢ (K \in HL \land X \in B \land Y \in B) \to ((X \underset{˙}{\land} Y) C X \leftrightarrow \exists p \in A (\neg p \underset{˙}{\leq} Y \land p \underset{˙}{\lor} (X \underset{˙}{\land} Y) = X))$

Metamath Proof Explorer

Theorem cvrval5

Proof