atcvr2

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

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

Step	Hyp	Ref	Expression
1		atcvr1.j	$⊢ \underset{˙}{\lor} = join (K)$
2		atcvr1.c	$⊢ C = ⋖_{K}$
3		atcvr1.a	$⊢ A = Atoms (K)$
4		hlomcmcv	$⊢ K \in HL \to (K \in OML \land K \in CLat \land K \in CvLat)$
5	1 2 3	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))$
6	4 5	syl3an1	$⊢ (K \in HL \land P \in A \land Q \in A) \to (P \neq Q \leftrightarrow P C (Q \underset{˙}{\lor} P))$

Metamath Proof Explorer