Theorem hlrelat1

Description: An atomistic lattice with 0 is relatively atomic. Part of Lemma 7.2 of MaedaMaeda p. 30. ( chpssati , with /\ swapped, analog.) (Contributed by NM, 4-Dec-2011)

	Ref	Expression
Hypotheses	hlrelat1.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	hlrelat1.l	⊢ ≤ = ( le ‘ 𝐾 )
	hlrelat1.s	⊢ < = ( lt ‘ 𝐾 )
	hlrelat1.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	hlrelat1	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < 𝑌 → ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		hlrelat1.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		hlrelat1.l	⊢ ≤ = ( le ‘ 𝐾 )
3		hlrelat1.s	⊢ < = ( lt ‘ 𝐾 )
4		hlrelat1.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		hlomcmat	⊢ ( 𝐾 ∈ HL → ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) )
6	1 2 3 4	atlrelat1	⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < 𝑌 → ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ) )
7	5 6	syl3an1	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < 𝑌 → ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌 ) ) )