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	⊢ 𝐹 = { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) }
Assertion	cfsetssfset	⊢ 𝐹 ⊆ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 }

Proof

Step	Hyp	Ref	Expression
1		cfsetsnfsetfv.f	⊢ 𝐹 = { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) }
2		ss2ab	⊢ ( { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) } ⊆ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ↔ ∀ 𝑓 ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) → 𝑓 : 𝐴 ⟶ 𝐵 ) )
3		simpl	⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) → 𝑓 : 𝐴 ⟶ 𝐵 )
4	2 3	mpgbir	⊢ { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) } ⊆ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 }
5	1 4	eqsstri	⊢ 𝐹 ⊆ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 }