Theorem paddasslem1

Description: Lemma for paddass . (Contributed by NM, 8-Jan-2012)

	Ref	Expression
Hypotheses	paddasslem.l	⊢ ≤ = ( le ‘ 𝐾 )
	paddasslem.j	⊢ ∨ = ( join ‘ 𝐾 )
	paddasslem.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	paddasslem1	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑦 ) ∧ ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) → ¬ 𝑥 ≤ ( 𝑟 ∨ 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		paddasslem.l	⊢ ≤ = ( le ‘ 𝐾 )
2		paddasslem.j	⊢ ∨ = ( join ‘ 𝐾 )
3		paddasslem.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4	1 2 3	hlatexch2	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑥 ≤ ( 𝑟 ∨ 𝑦 ) → 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) )
5	4	con3dimp	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑦 ) ∧ ¬ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) → ¬ 𝑥 ≤ ( 𝑟 ∨ 𝑦 ) )