Theorem atlex

Description: Every nonzero element of an atomic lattice is greater than or equal to an atom. ( hatomic analog.) (Contributed by NM, 21-Oct-2011)

	Ref	Expression
Hypotheses	atlex.b	$$⊢B={\mathrm{Base}}_K$$
	atlex.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	atlex.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
	atlex.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	atlex	$$⊢\left(K\in \mathrm{AtLat}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\to \exists y\in Ay\underset{\dot{}}{\le }X$$

Proof

Step	Hyp	Ref	Expression
1		atlex.b	$$⊢B={\mathrm{Base}}_K$$
2		atlex.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		atlex.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
4		atlex.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		eqid	$$⊢\mathrm{glb}\left(K\right)=\mathrm{glb}\left(K\right)$$
6	1 5 2 3 4	isatl	$$⊢K\in \mathrm{AtLat}\leftrightarrow \left(K\in \mathrm{Lat}\wedge B\in \mathrm{dom}\mathrm{glb}\left(K\right)\wedge \forall x\in B\left(x\ne \underset{\dot{}}{0}\to \exists y\in Ay\underset{\dot{}}{\le }x\right)\right)$$
7	6	simp3bi	$$⊢K\in \mathrm{AtLat}\to \forall x\in B\left(x\ne \underset{\dot{}}{0}\to \exists y\in Ay\underset{\dot{}}{\le }x\right)$$
8		neeq1	$$⊢x=X\to \left(x\ne \underset{\dot{}}{0}\leftrightarrow X\ne \underset{\dot{}}{0}\right)$$
9		breq2	$$⊢x=X\to \left(y\underset{\dot{}}{\le }x\leftrightarrow y\underset{\dot{}}{\le }X\right)$$
10	9	rexbidv	$$⊢x=X\to \left(\exists y\in Ay\underset{\dot{}}{\le }x\leftrightarrow \exists y\in Ay\underset{\dot{}}{\le }X\right)$$
11	8 10	imbi12d	$$⊢x=X\to \left(\left(x\ne \underset{\dot{}}{0}\to \exists y\in Ay\underset{\dot{}}{\le }x\right)\leftrightarrow \left(X\ne \underset{\dot{}}{0}\to \exists y\in Ay\underset{\dot{}}{\le }X\right)\right)$$
12	11	rspccv	$$⊢\forall x\in B\left(x\ne \underset{\dot{}}{0}\to \exists y\in Ay\underset{\dot{}}{\le }x\right)\to \left(X\in B\to \left(X\ne \underset{\dot{}}{0}\to \exists y\in Ay\underset{\dot{}}{\le }X\right)\right)$$
13	7 12	syl	$$⊢K\in \mathrm{AtLat}\to \left(X\in B\to \left(X\ne \underset{\dot{}}{0}\to \exists y\in Ay\underset{\dot{}}{\le }X\right)\right)$$
14	13	3imp	$$⊢\left(K\in \mathrm{AtLat}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\to \exists y\in Ay\underset{\dot{}}{\le }X$$