This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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→ 𝐵 )