Theorem fsetsnf1o

Description: The mapping of an element of a class to a singleton function is a bijection. (Contributed by AV, 13-Sep-2024)

	Ref	Expression
Hypotheses	fsetsnf.a	⊢ 𝐴 = { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = { ⟨ 𝑆 , 𝑏 ⟩ } }
	fsetsnf.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ { ⟨ 𝑆 , 𝑥 ⟩ } )
Assertion	fsetsnf1o	⊢ ( 𝑆 ∈ 𝑉 → 𝐹 : 𝐵 –1-1-onto→ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		fsetsnf.a	⊢ 𝐴 = { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = { ⟨ 𝑆 , 𝑏 ⟩ } }
2		fsetsnf.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ { ⟨ 𝑆 , 𝑥 ⟩ } )
3	1 2	fsetsnf1	⊢ ( 𝑆 ∈ 𝑉 → 𝐹 : 𝐵 –1-1→ 𝐴 )
4	1 2	fsetsnfo	⊢ ( 𝑆 ∈ 𝑉 → 𝐹 : 𝐵 –onto→ 𝐴 )
5		df-f1o	⊢ ( 𝐹 : 𝐵 –1-1-onto→ 𝐴 ↔ ( 𝐹 : 𝐵 –1-1→ 𝐴 ∧ 𝐹 : 𝐵 –onto→ 𝐴 ) )
6	3 4 5	sylanbrc	⊢ ( 𝑆 ∈ 𝑉 → 𝐹 : 𝐵 –1-1-onto→ 𝐴 )