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	|- B = ( Base ` K )
	hlatmstc.l	|- .<_ = ( le ` K )
	hlatmstc.u	|- U = ( lub ` K )
	hlatmstc.a	|- A = ( Atoms ` K )
Assertion	hlatmstcOLDN	|- ( ( K e. HL /\ X e. B ) -> ( U ` { y e. A | y .<_ X } ) = X )

Proof

Step	Hyp	Ref	Expression
1		hlatmstc.b	|- B = ( Base ` K )
2		hlatmstc.l	|- .<_ = ( le ` K )
3		hlatmstc.u	|- U = ( lub ` K )
4		hlatmstc.a	|- A = ( Atoms ` K )
5		hlomcmat	|- ( K e. HL -> ( K e. OML /\ K e. CLat /\ K e. AtLat ) )
6	1 2 3 4	atlatmstc	|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) -> ( U ` { y e. A | y .<_ X } ) = X )
7	5 6	sylan	|- ( ( K e. HL /\ X e. B ) -> ( U ` { y e. A | y .<_ X } ) = X )