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	5	fmpttd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) : 𝐴 ⟶ 𝐵 )
7		simpll	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → 𝐴 ∈ 𝑉 )
8	7	mptexd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ∈ V )
9		feq1	⊢ ( 𝑓 = ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) → ( 𝑓 : 𝐴 ⟶ 𝐵 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) : 𝐴 ⟶ 𝐵 ) )
10	9 1	elab2g	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ∈ V → ( ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ∈ 𝐹 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) : 𝐴 ⟶ 𝐵 ) )
11	8 10	syl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ∈ 𝐹 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) : 𝐴 ⟶ 𝐵 ) )
12	6 11	mpbird	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ∈ 𝐹 )
13		fveq1	⊢ ( 𝑔 = 𝑓 → ( 𝑔 ‘ 𝑋 ) = ( 𝑓 ‘ 𝑋 ) )
14	13	cbvmptv	⊢ ( 𝑔 ∈ 𝐹 ↦ ( 𝑔 ‘ 𝑋 ) ) = ( 𝑓 ∈ 𝐹 ↦ ( 𝑓 ‘ 𝑋 ) )
15	2 14	eqtri	⊢ 𝑆 = ( 𝑓 ∈ 𝐹 ↦ ( 𝑓 ‘ 𝑋 ) )
16		fveq1	⊢ ( 𝑓 = ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) → ( 𝑓 ‘ 𝑋 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ‘ 𝑋 ) )
17		fvexd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ‘ 𝑋 ) ∈ V )
18	15 16 12 17	fvmptd3	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝑆 ‘ ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ‘ 𝑋 ) )
19		eqidd	⊢ ( 𝑥 = 𝑋 → 𝑔 = 𝑔 )
20		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑔 )
21		vex	⊢ 𝑔 ∈ V
22	19 20 21	fvmpt	⊢ ( 𝑋 ∈ 𝐴 → ( ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ‘ 𝑋 ) = 𝑔 )
23	22	ad2antlr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ‘ 𝑋 ) = 𝑔 )
24	18 23	eqtrd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝑆 ‘ ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ) = 𝑔 )
25		fveq2	⊢ ( ℎ = ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) → ( 𝑆 ‘ ℎ ) = ( 𝑆 ‘ ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ) )
26	25	eqcomd	⊢ ( ℎ = ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) → ( 𝑆 ‘ ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ) = ( 𝑆 ‘ ℎ ) )
27	24 26	sylan9req	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 ∈ 𝐴 ↦ 𝑔 ) ) → 𝑔 = ( 𝑆 ‘ ℎ ) )
28	12 27	rspcedeqvd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ∃ ℎ ∈ 𝐹 𝑔 = ( 𝑆 ‘ ℎ ) )
29	28	ralrimiva	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑔 ∈ 𝐵 ∃ ℎ ∈ 𝐹 𝑔 = ( 𝑆 ‘ ℎ ) )
30		dffo3	⊢ ( 𝑆 : 𝐹 –onto→ 𝐵 ↔ ( 𝑆 : 𝐹 ⟶ 𝐵 ∧ ∀ 𝑔 ∈ 𝐵 ∃ ℎ ∈ 𝐹 𝑔 = ( 𝑆 ‘ ℎ ) ) )
31	4 29 30	sylanbrc	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴 ) → 𝑆 : 𝐹 –onto→ 𝐵 )