Theorem fsetsnf

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

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

Proof

Step	Hyp	Ref	Expression
1		fsetsnf.a	⊢ 𝐴 = { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = { ⟨ 𝑆 , 𝑏 ⟩ } }
2		fsetsnf.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ { ⟨ 𝑆 , 𝑥 ⟩ } )
3		simpr	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
4		opeq2	⊢ ( 𝑏 = 𝑥 → ⟨ 𝑆 , 𝑏 ⟩ = ⟨ 𝑆 , 𝑥 ⟩ )
5	4	sneqd	⊢ ( 𝑏 = 𝑥 → { ⟨ 𝑆 , 𝑏 ⟩ } = { ⟨ 𝑆 , 𝑥 ⟩ } )
6	5	eqeq2d	⊢ ( 𝑏 = 𝑥 → ( { ⟨ 𝑆 , 𝑥 ⟩ } = { ⟨ 𝑆 , 𝑏 ⟩ } ↔ { ⟨ 𝑆 , 𝑥 ⟩ } = { ⟨ 𝑆 , 𝑥 ⟩ } ) )
7	6	adantl	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑏 = 𝑥 ) → ( { ⟨ 𝑆 , 𝑥 ⟩ } = { ⟨ 𝑆 , 𝑏 ⟩ } ↔ { ⟨ 𝑆 , 𝑥 ⟩ } = { ⟨ 𝑆 , 𝑥 ⟩ } ) )
8		eqidd	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) → { ⟨ 𝑆 , 𝑥 ⟩ } = { ⟨ 𝑆 , 𝑥 ⟩ } )
9	3 7 8	rspcedvd	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑏 ∈ 𝐵 { ⟨ 𝑆 , 𝑥 ⟩ } = { ⟨ 𝑆 , 𝑏 ⟩ } )
10		snex	⊢ { ⟨ 𝑆 , 𝑥 ⟩ } ∈ V
11		eqeq1	⊢ ( 𝑦 = { ⟨ 𝑆 , 𝑥 ⟩ } → ( 𝑦 = { ⟨ 𝑆 , 𝑏 ⟩ } ↔ { ⟨ 𝑆 , 𝑥 ⟩ } = { ⟨ 𝑆 , 𝑏 ⟩ } ) )
12	11	rexbidv	⊢ ( 𝑦 = { ⟨ 𝑆 , 𝑥 ⟩ } → ( ∃ 𝑏 ∈ 𝐵 𝑦 = { ⟨ 𝑆 , 𝑏 ⟩ } ↔ ∃ 𝑏 ∈ 𝐵 { ⟨ 𝑆 , 𝑥 ⟩ } = { ⟨ 𝑆 , 𝑏 ⟩ } ) )
13	10 12 1	elab2	⊢ ( { ⟨ 𝑆 , 𝑥 ⟩ } ∈ 𝐴 ↔ ∃ 𝑏 ∈ 𝐵 { ⟨ 𝑆 , 𝑥 ⟩ } = { ⟨ 𝑆 , 𝑏 ⟩ } )
14	9 13	sylibr	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) → { ⟨ 𝑆 , 𝑥 ⟩ } ∈ 𝐴 )
15	14 2	fmptd	⊢ ( 𝑆 ∈ 𝑉 → 𝐹 : 𝐵 ⟶ 𝐴 )