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={\mathrm{Base}}_K$$
	hlatmstc.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	hlatmstc.u	$$⊢U=\mathrm{lub}\left(K\right)$$
	hlatmstc.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	hlatmstcOLDN	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to U\left(\left\{y\in A|y\underset{\dot{}}{\le }X\right\}\right)=X$$

Proof

Step	Hyp	Ref	Expression
1		hlatmstc.b	$$⊢B={\mathrm{Base}}_K$$
2		hlatmstc.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		hlatmstc.u	$$⊢U=\mathrm{lub}\left(K\right)$$
4		hlatmstc.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		hlomcmat	$$⊢K\in \mathrm{HL}\to \left(K\in \mathrm{OML}\wedge K\in \mathrm{CLat}\wedge K\in \mathrm{AtLat}\right)$$
6	1 2 3 4	atlatmstc	$$⊢\left(\left(K\in \mathrm{OML}\wedge K\in \mathrm{CLat}\wedge K\in \mathrm{AtLat}\right)\wedge X\in B\right)\to U\left(\left\{y\in A|y\underset{\dot{}}{\le }X\right\}\right)=X$$
7	5 6	sylan	$$⊢\left(K\in \mathrm{HL}\wedge X\in B\right)\to U\left(\left\{y\in A|y\underset{\dot{}}{\le }X\right\}\right)=X$$