Theorem clatp1cl

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

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

Proof

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