Theorem fsetsnfo

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

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

Proof

Step	Hyp	Ref	Expression
1		fsetsnf.a	⊢ 𝐴 = { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = { ⟨ 𝑆 , 𝑏 ⟩ } }
2		fsetsnf.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ { ⟨ 𝑆 , 𝑥 ⟩ } )
3	1 2	fsetsnf	⊢ ( 𝑆 ∈ 𝑉 → 𝐹 : 𝐵 ⟶ 𝐴 )
4		vex	⊢ 𝑚 ∈ V
5		eqeq1	⊢ ( 𝑦 = 𝑚 → ( 𝑦 = { ⟨ 𝑆 , 𝑏 ⟩ } ↔ 𝑚 = { ⟨ 𝑆 , 𝑏 ⟩ } ) )
6	5	rexbidv	⊢ ( 𝑦 = 𝑚 → ( ∃ 𝑏 ∈ 𝐵 𝑦 = { ⟨ 𝑆 , 𝑏 ⟩ } ↔ ∃ 𝑏 ∈ 𝐵 𝑚 = { ⟨ 𝑆 , 𝑏 ⟩ } ) )
7	4 6 1	elab2	⊢ ( 𝑚 ∈ 𝐴 ↔ ∃ 𝑏 ∈ 𝐵 𝑚 = { ⟨ 𝑆 , 𝑏 ⟩ } )
8		opeq2	⊢ ( 𝑏 = 𝑛 → ⟨ 𝑆 , 𝑏 ⟩ = ⟨ 𝑆 , 𝑛 ⟩ )
9	8	sneqd	⊢ ( 𝑏 = 𝑛 → { ⟨ 𝑆 , 𝑏 ⟩ } = { ⟨ 𝑆 , 𝑛 ⟩ } )
10	9	eqeq2d	⊢ ( 𝑏 = 𝑛 → ( 𝑚 = { ⟨ 𝑆 , 𝑏 ⟩ } ↔ 𝑚 = { ⟨ 𝑆 , 𝑛 ⟩ } ) )
11	10	cbvrexvw	⊢ ( ∃ 𝑏 ∈ 𝐵 𝑚 = { ⟨ 𝑆 , 𝑏 ⟩ } ↔ ∃ 𝑛 ∈ 𝐵 𝑚 = { ⟨ 𝑆 , 𝑛 ⟩ } )
12		simpr	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑛 ∈ 𝐵 ) ∧ 𝑚 = { ⟨ 𝑆 , 𝑛 ⟩ } ) → 𝑚 = { ⟨ 𝑆 , 𝑛 ⟩ } )
13	2	a1i	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑛 ∈ 𝐵 ) → 𝐹 = ( 𝑥 ∈ 𝐵 ↦ { ⟨ 𝑆 , 𝑥 ⟩ } ) )
14		opeq2	⊢ ( 𝑥 = 𝑛 → ⟨ 𝑆 , 𝑥 ⟩ = ⟨ 𝑆 , 𝑛 ⟩ )
15	14	sneqd	⊢ ( 𝑥 = 𝑛 → { ⟨ 𝑆 , 𝑥 ⟩ } = { ⟨ 𝑆 , 𝑛 ⟩ } )
16	15	adantl	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑛 ∈ 𝐵 ) ∧ 𝑥 = 𝑛 ) → { ⟨ 𝑆 , 𝑥 ⟩ } = { ⟨ 𝑆 , 𝑛 ⟩ } )
17		simpr	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑛 ∈ 𝐵 ) → 𝑛 ∈ 𝐵 )
18		snex	⊢ { ⟨ 𝑆 , 𝑛 ⟩ } ∈ V
19	18	a1i	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑛 ∈ 𝐵 ) → { ⟨ 𝑆 , 𝑛 ⟩ } ∈ V )
20	13 16 17 19	fvmptd	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑛 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑛 ) = { ⟨ 𝑆 , 𝑛 ⟩ } )
21	20	eqcomd	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑛 ∈ 𝐵 ) → { ⟨ 𝑆 , 𝑛 ⟩ } = ( 𝐹 ‘ 𝑛 ) )
22	21	adantr	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑛 ∈ 𝐵 ) ∧ 𝑚 = { ⟨ 𝑆 , 𝑛 ⟩ } ) → { ⟨ 𝑆 , 𝑛 ⟩ } = ( 𝐹 ‘ 𝑛 ) )
23	12 22	eqtrd	⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑛 ∈ 𝐵 ) ∧ 𝑚 = { ⟨ 𝑆 , 𝑛 ⟩ } ) → 𝑚 = ( 𝐹 ‘ 𝑛 ) )
24	23	ex	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑛 ∈ 𝐵 ) → ( 𝑚 = { ⟨ 𝑆 , 𝑛 ⟩ } → 𝑚 = ( 𝐹 ‘ 𝑛 ) ) )
25	24	reximdva	⊢ ( 𝑆 ∈ 𝑉 → ( ∃ 𝑛 ∈ 𝐵 𝑚 = { ⟨ 𝑆 , 𝑛 ⟩ } → ∃ 𝑛 ∈ 𝐵 𝑚 = ( 𝐹 ‘ 𝑛 ) ) )
26	11 25	syl5bi	⊢ ( 𝑆 ∈ 𝑉 → ( ∃ 𝑏 ∈ 𝐵 𝑚 = { ⟨ 𝑆 , 𝑏 ⟩ } → ∃ 𝑛 ∈ 𝐵 𝑚 = ( 𝐹 ‘ 𝑛 ) ) )
27	7 26	syl5bi	⊢ ( 𝑆 ∈ 𝑉 → ( 𝑚 ∈ 𝐴 → ∃ 𝑛 ∈ 𝐵 𝑚 = ( 𝐹 ‘ 𝑛 ) ) )
28	27	imp	⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑚 ∈ 𝐴 ) → ∃ 𝑛 ∈ 𝐵 𝑚 = ( 𝐹 ‘ 𝑛 ) )
29	28	ralrimiva	⊢ ( 𝑆 ∈ 𝑉 → ∀ 𝑚 ∈ 𝐴 ∃ 𝑛 ∈ 𝐵 𝑚 = ( 𝐹 ‘ 𝑛 ) )
30		dffo3	⊢ ( 𝐹 : 𝐵 –onto→ 𝐴 ↔ ( 𝐹 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑚 ∈ 𝐴 ∃ 𝑛 ∈ 𝐵 𝑚 = ( 𝐹 ‘ 𝑛 ) ) )
31	3 29 30	sylanbrc	⊢ ( 𝑆 ∈ 𝑉 → 𝐹 : 𝐵 –onto→ 𝐴 )