Theorem fsetfocdm

Description: The class of functions with a given domain that is a set and a given codomain is mapped, through evaluation at a point of the domain, onto the codomain. (Contributed by AV, 15-Sep-2024)

	Ref	Expression
Hypotheses	fsetfocdm.f	⊢ 𝐹 = { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 }
	fsetfocdm.s	⊢ 𝑆 = ( 𝑔 ∈ 𝐹 ↦ ( 𝑔 ‘ 𝑋 ) )
Assertion	fsetfocdm	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → 𝑆 : 𝐹 –onto→ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fsetfocdm.f	⊢ 𝐹 = { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 }
2		fsetfocdm.s	⊢ 𝑆 = ( 𝑔 ∈ 𝐹 ↦ ( 𝑔 ‘ 𝑋 ) )
3	1 2	fsetfcdm	⊢ ( 𝑋 ∈ 𝐴 → 𝑆 : 𝐹 ⟶ 𝐵 )
4	3	adantl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → 𝑆 : 𝐹 ⟶ 𝐵 )
5		simplr	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑔 ∈ 𝐵 )
6		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑔 )
7	5 6	fmptd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) : 𝐴 ⟶ 𝐵 )
8		simpll	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → 𝐴 ∈ 𝑉 )
9	8	mptexd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ∈ V )
10		feq1	⊢ ( 𝑓 = ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) → ( 𝑓 : 𝐴 ⟶ 𝐵 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) : 𝐴 ⟶ 𝐵 ) )
11	10 1	elab2g	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ∈ V → ( ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ∈ 𝐹 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) : 𝐴 ⟶ 𝐵 ) )
12	9 11	syl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ∈ 𝐹 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) : 𝐴 ⟶ 𝐵 ) )
13	7 12	mpbird	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ∈ 𝐹 )
14		fveq2	⊢ ( ℎ = ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) → ( 𝑆 ‘ ℎ ) = ( 𝑆 ‘ ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ) )
15	14	eqeq2d	⊢ ( ℎ = ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) → ( 𝑔 = ( 𝑆 ‘ ℎ ) ↔ 𝑔 = ( 𝑆 ‘ ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ) ) )
16	15	adantl	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ) → ( 𝑔 = ( 𝑆 ‘ ℎ ) ↔ 𝑔 = ( 𝑆 ‘ ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ) ) )
17		fveq1	⊢ ( 𝑔 = 𝑓 → ( 𝑔 ‘ 𝑋 ) = ( 𝑓 ‘ 𝑋 ) )
18	17	cbvmptv	⊢ ( 𝑔 ∈ 𝐹 ↦ ( 𝑔 ‘ 𝑋 ) ) = ( 𝑓 ∈ 𝐹 ↦ ( 𝑓 ‘ 𝑋 ) )
19	2 18	eqtri	⊢ 𝑆 = ( 𝑓 ∈ 𝐹 ↦ ( 𝑓 ‘ 𝑋 ) )
20	19	a1i	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → 𝑆 = ( 𝑓 ∈ 𝐹 ↦ ( 𝑓 ‘ 𝑋 ) ) )
21		fveq1	⊢ ( 𝑓 = ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) → ( 𝑓 ‘ 𝑋 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ‘ 𝑋 ) )
22	21	adantl	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) ∧ 𝑓 = ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ) → ( 𝑓 ‘ 𝑋 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ‘ 𝑋 ) )
23		fvexd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ‘ 𝑋 ) ∈ V )
24	20 22 13 23	fvmptd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝑆 ‘ ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ‘ 𝑋 ) )
25		eqidd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) )
26		eqidd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑥 = 𝑋 ) → 𝑔 = 𝑔 )
27		simpr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ 𝐴 )
28		vex	⊢ 𝑔 ∈ V
29	28	a1i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → 𝑔 ∈ V )
30	25 26 27 29	fvmptd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ‘ 𝑋 ) = 𝑔 )
31	30	adantr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ‘ 𝑋 ) = 𝑔 )
32	24 31	eqtr2d	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → 𝑔 = ( 𝑆 ‘ ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ) )
33	13 16 32	rspcedvd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ∃ ℎ ∈ 𝐹 𝑔 = ( 𝑆 ‘ ℎ ) )
34	33	ralrimiva	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑔 ∈ 𝐵 ∃ ℎ ∈ 𝐹 𝑔 = ( 𝑆 ‘ ℎ ) )
35		dffo3	⊢ ( 𝑆 : 𝐹 –onto→ 𝐵 ↔ ( 𝑆 : 𝐹 ⟶ 𝐵 ∧ ∀ 𝑔 ∈ 𝐵 ∃ ℎ ∈ 𝐹 𝑔 = ( 𝑆 ‘ ℎ ) ) )
36	4 34 35	sylanbrc	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → 𝑆 : 𝐹 –onto→ 𝐵 )