cvlatcvr2

Description: An atom is covered by its join with a different atom. (Contributed by NM, 5-Nov-2012)

	Ref	Expression
Hypotheses	cvlatcvr1.j	$⊢ \underset{˙}{\lor} = join (K)$
	cvlatcvr1.c	$⊢ C = ⋖_{K}$
	cvlatcvr1.a	$⊢ A = Atoms (K)$
Assertion	cvlatcvr2	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land P \in A \land Q \in A) \to (P \neq Q \leftrightarrow P C (Q \underset{˙}{\lor} P))$

Step	Hyp	Ref	Expression
1		cvlatcvr1.j	$⊢ \underset{˙}{\lor} = join (K)$
2		cvlatcvr1.c	$⊢ C = ⋖_{K}$
3		cvlatcvr1.a	$⊢ A = Atoms (K)$
4	1 2 3	cvlatcvr1	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land P \in A \land Q \in A) \to (P \neq Q \leftrightarrow P C (P \underset{˙}{\lor} Q))$
5		simp13	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land P \in A \land Q \in A) \to K \in CvLat$
6		cvllat	$⊢ K \in CvLat \to K \in Lat$
7	5 6	syl	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land P \in A \land Q \in A) \to K \in Lat$
8		eqid	$⊢ {Base}_{K} = {Base}_{K}$
9	8 3	atbase	$⊢ P \in A \to P \in {Base}_{K}$
10	9	3ad2ant2	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land P \in A \land Q \in A) \to P \in {Base}_{K}$
11	8 3	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
12	11	3ad2ant3	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land P \in A \land Q \in A) \to Q \in {Base}_{K}$
13	8 1	latjcom	$⊢ (K \in Lat \land P \in {Base}_{K} \land Q \in {Base}_{K}) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
14	7 10 12 13	syl3anc	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
15	14	breq2d	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land P \in A \land Q \in A) \to (P C (P \underset{˙}{\lor} Q) \leftrightarrow P C (Q \underset{˙}{\lor} P))$
16	4 15	bitrd	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land P \in A \land Q \in A) \to (P \neq Q \leftrightarrow P C (Q \underset{˙}{\lor} P))$

Metamath Proof Explorer