atcvrj2

Description: Condition for an atom to be covered by the join of two others. (Contributed by NM, 7-Feb-2012)

	Ref	Expression
Hypotheses	atcvrj1x.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	atcvrj1x.j	$⊢ \underset{˙}{\lor} = join (K)$
	atcvrj1x.c	$⊢ C = ⋖_{K}$
	atcvrj1x.a	$⊢ A = Atoms (K)$
Assertion	atcvrj2	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to P C (Q \underset{˙}{\lor} R)$

Step	Hyp	Ref	Expression
1		atcvrj1x.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		atcvrj1x.j	$⊢ \underset{˙}{\lor} = join (K)$
3		atcvrj1x.c	$⊢ C = ⋖_{K}$
4		atcvrj1x.a	$⊢ A = Atoms (K)$
5	1 2 3 4	atcvrj2b	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to ((Q \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \leftrightarrow P C (Q \underset{˙}{\lor} R))$
6	5	biimp3a	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to P C (Q \underset{˙}{\lor} R)$

Metamath Proof Explorer