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	⊢ 𝐵 = ( Base ‘ 𝑊 )
	clatp1cl.1	⊢ 1 = ( 1. ‘ 𝑊 )
Assertion	clatp1cl	⊢ ( 𝑊 ∈ CLat → 1 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		clatp1cl.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		clatp1cl.1	⊢ 1 = ( 1. ‘ 𝑊 )
3		eqid	⊢ ( lub ‘ 𝑊 ) = ( lub ‘ 𝑊 )
4	1 3 2	p1val	⊢ ( 𝑊 ∈ CLat → 1 = ( ( lub ‘ 𝑊 ) ‘ 𝐵 ) )
5		ssid	⊢ 𝐵 ⊆ 𝐵
6	1 3	clatlubcl	⊢ ( ( 𝑊 ∈ CLat ∧ 𝐵 ⊆ 𝐵 ) → ( ( lub ‘ 𝑊 ) ‘ 𝐵 ) ∈ 𝐵 )
7	5 6	mpan2	⊢ ( 𝑊 ∈ CLat → ( ( lub ‘ 𝑊 ) ‘ 𝐵 ) ∈ 𝐵 )
8	4 7	eqeltrd	⊢ ( 𝑊 ∈ CLat → 1 ∈ 𝐵 )