Theorem 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	⊢ ≤ = ( le ‘ 𝐾 )
	atcvrj1x.j	⊢ ∨ = ( join ‘ 𝐾 )
	atcvrj1x.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
	atcvrj1x.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	atcvrj2	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		atcvrj1x.l	⊢ ≤ = ( le ‘ 𝐾 )
2		atcvrj1x.j	⊢ ∨ = ( join ‘ 𝐾 )
3		atcvrj1x.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
4		atcvrj1x.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5	1 2 3 4	atcvrj2b	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( ( 𝑄 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ↔ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) )
6	5	biimp3a	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) )