Theorem cfsetssfset

Description: The class of constant functions is a subclass of the class of functions. (Contributed by AV, 13-Sep-2024)

	Ref	Expression
Hypothesis	cfsetsnfsetfv.f	$$⊢F=\left\{f|\left(f:A⟶B\wedge \exists b\in B\forall z\in Af\left(z\right)=b\right)\right\}$$
Assertion	cfsetssfset	$$⊢F\subseteq \left\{f|f:A⟶B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		cfsetsnfsetfv.f	$$⊢F=\left\{f|\left(f:A⟶B\wedge \exists b\in B\forall z\in Af\left(z\right)=b\right)\right\}$$
2		ss2ab	$$⊢\left\{f|\left(f:A⟶B\wedge \exists b\in B\forall z\in Af\left(z\right)=b\right)\right\}\subseteq \left\{f|f:A⟶B\right\}\leftrightarrow \forall f\left(\left(f:A⟶B\wedge \exists b\in B\forall z\in Af\left(z\right)=b\right)\to f:A⟶B\right)$$
3		simpl	$$⊢\left(f:A⟶B\wedge \exists b\in B\forall z\in Af\left(z\right)=b\right)\to f:A⟶B$$
4	2 3	mpgbir	$$⊢\left\{f|\left(f:A⟶B\wedge \exists b\in B\forall z\in Af\left(z\right)=b\right)\right\}\subseteq \left\{f|f:A⟶B\right\}$$
5	1 4	eqsstri	$$⊢F\subseteq \left\{f|f:A⟶B\right\}$$