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

Proof

Step	Hyp	Ref	Expression
1		clatp0cl.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		clatp0cl.0	⊢ 0 = ( 0. ‘ 𝑊 )
3		eqid	⊢ ( glb ‘ 𝑊 ) = ( glb ‘ 𝑊 )
4	1 3 2	p0val	⊢ ( 𝑊 ∈ CLat → 0 = ( ( glb ‘ 𝑊 ) ‘ 𝐵 ) )
5		ssid	⊢ 𝐵 ⊆ 𝐵
6	1 3	clatglbcl	⊢ ( ( 𝑊 ∈ CLat ∧ 𝐵 ⊆ 𝐵 ) → ( ( glb ‘ 𝑊 ) ‘ 𝐵 ) ∈ 𝐵 )
7	5 6	mpan2	⊢ ( 𝑊 ∈ CLat → ( ( glb ‘ 𝑊 ) ‘ 𝐵 ) ∈ 𝐵 )
8	4 7	eqeltrd	⊢ ( 𝑊 ∈ CLat → 0 ∈ 𝐵 )