Theorem hlatmstcOLDN

Description: An atomic, complete, orthomodular lattice is atomistic i.e. every element is the join of the atoms under it. See remark before Proposition 1 in Kalmbach p. 140; also remark in BeltramettiCassinelli p. 98. ( hatomistici analog.) (Contributed by NM, 21-Oct-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hlatmstc.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	hlatmstc.l	⊢ ≤ = ( le ‘ 𝐾 )
	hlatmstc.u	⊢ 𝑈 = ( lub ‘ 𝐾 )
	hlatmstc.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	hlatmstcOLDN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑈 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		hlatmstc.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		hlatmstc.l	⊢ ≤ = ( le ‘ 𝐾 )
3		hlatmstc.u	⊢ 𝑈 = ( lub ‘ 𝐾 )
4		hlatmstc.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		hlomcmat	⊢ ( 𝐾 ∈ HL → ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) )
6	1 2 3 4	atlatmstc	⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝑈 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) = 𝑋 )
7	5 6	sylan	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑈 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) = 𝑋 )