Theorem clatp0cl

Description: The poset zero of a complete lattice belongs to its base. (Contributed by Thierry Arnoux, 17-Feb-2018)

	Ref	Expression
Hypotheses	clatp0cl.b	$$⊢B={\mathrm{Base}}_W$$
	clatp0cl.0	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(W\right)$$
Assertion	clatp0cl	$$⊢W\in \mathrm{CLat}\to \underset{\dot{}}{0}\in B$$

Proof

Step	Hyp	Ref	Expression
1		clatp0cl.b	$$⊢B={\mathrm{Base}}_W$$
2		clatp0cl.0	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(W\right)$$
3		eqid	$$⊢\mathrm{glb}\left(W\right)=\mathrm{glb}\left(W\right)$$
4	1 3 2	p0val	$$⊢W\in \mathrm{CLat}\to \underset{\dot{}}{0}=\mathrm{glb}\left(W\right)\left(B\right)$$
5		ssid	$$⊢B\subseteq B$$
6	1 3	clatglbcl	$$⊢\left(W\in \mathrm{CLat}\wedge B\subseteq B\right)\to \mathrm{glb}\left(W\right)\left(B\right)\in B$$
7	5 6	mpan2	$$⊢W\in \mathrm{CLat}\to \mathrm{glb}\left(W\right)\left(B\right)\in B$$
8	4 7	eqeltrd	$$⊢W\in \mathrm{CLat}\to \underset{\dot{}}{0}\in B$$