Theorem cfsetsnfsetf1o

Description: The mapping of the class of singleton functions into the class of constant functions is a bijection. (Contributed by AV, 14-Sep-2024)

	Ref	Expression
Hypotheses	cfsetsnfsetfv.f	⊢ 𝐹 = { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) }
	cfsetsnfsetfv.g	⊢ 𝐺 = { 𝑥 ∣ 𝑥 : { 𝑌 } ⟶ 𝐵 }
	cfsetsnfsetfv.h	⊢ 𝐻 = ( 𝑔 ∈ 𝐺 ↦ ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) )
Assertion	cfsetsnfsetf1o	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → 𝐻 : 𝐺 –1-1-onto→ 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		cfsetsnfsetfv.f	⊢ 𝐹 = { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) }
2		cfsetsnfsetfv.g	⊢ 𝐺 = { 𝑥 ∣ 𝑥 : { 𝑌 } ⟶ 𝐵 }
3		cfsetsnfsetfv.h	⊢ 𝐻 = ( 𝑔 ∈ 𝐺 ↦ ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) )
4	1 2 3	cfsetsnfsetf1	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → 𝐻 : 𝐺 –1-1→ 𝐹 )
5	1 2 3	cfsetsnfsetfo	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → 𝐻 : 𝐺 –onto→ 𝐹 )
6		df-f1o	⊢ ( 𝐻 : 𝐺 –1-1-onto→ 𝐹 ↔ ( 𝐻 : 𝐺 –1-1→ 𝐹 ∧ 𝐻 : 𝐺 –onto→ 𝐹 ) )
7	4 5 6	sylanbrc	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → 𝐻 : 𝐺 –1-1-onto→ 𝐹 )