Theorem hlatle

Description: The ordering of two Hilbert lattice elements is determined by the atoms under them. ( chrelat3 analog.) (Contributed by NM, 4-Nov-2011)

	Ref	Expression
Hypotheses	hlatle.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	hlatle.l	⊢ ≤ = ( le ‘ 𝐾 )
	hlatle.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	hlatle	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 ↔ ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		hlatle.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		hlatle.l	⊢ ≤ = ( le ‘ 𝐾 )
3		hlatle.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		hlomcmat	⊢ ( 𝐾 ∈ HL → ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) )
5	1 2 3	atlatle	⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 ↔ ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌 ) ) )
6	4 5	syl3an1	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 ↔ ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌 ) ) )