Metamath Proof Explorer


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 rspcedeq2vd ( ( ( 𝐴𝑉𝑋𝐴 ) ∧ 𝑔𝐵 ) → ∃ 𝐹 𝑔 = ( 𝑆 ) )
29 28 ralrimiva ( ( 𝐴𝑉𝑋𝐴 ) → ∀ 𝑔𝐵𝐹 𝑔 = ( 𝑆 ) )
30 dffo3 ( 𝑆 : 𝐹onto𝐵 ↔ ( 𝑆 : 𝐹𝐵 ∧ ∀ 𝑔𝐵𝐹 𝑔 = ( 𝑆 ) ) )
31 4 29 30 sylanbrc ( ( 𝐴𝑉𝑋𝐴 ) → 𝑆 : 𝐹onto𝐵 )