Theorem paddasslem3

Description: Lemma for paddass . Restate projective space axiom ps-2 . (Contributed by NM, 8-Jan-2012)

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

Proof

Step	Hyp	Ref	Expression
1		paddasslem.l	⊢ ≤ = ( le ‘ 𝐾 )
2		paddasslem.j	⊢ ∨ = ( join ‘ 𝐾 )
3		paddasslem.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4	1 2 3	ps-2	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ( ( ¬ 𝑥 ≤ ( 𝑟 ∨ 𝑦 ) ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑧 ≤ ( 𝑟 ∨ 𝑦 ) ) ) ) → ∃ 𝑠 ∈ 𝐴 ( 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) )
5	4	ex	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( ( ¬ 𝑥 ≤ ( 𝑟 ∨ 𝑦 ) ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ∧ 𝑧 ≤ ( 𝑟 ∨ 𝑦 ) ) ) → ∃ 𝑠 ∈ 𝐴 ( 𝑠 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) )