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 ⊢ F = f | f : A ⟶ B
fsetfocdm.s ⊢ S = g ∈ F ⟼ g ⁡ X
Assertion fsetfocdm ⊢ A ∈ V ∧ X ∈ A → S : F ⟶ onto B

Proof

Step Hyp Ref Expression
1 fsetfocdm.f ⊢ F = f | f : A ⟶ B
2 fsetfocdm.s ⊢ S = g ∈ F ⟼ g ⁡ X
3 1 2 fsetfcdm ⊢ X ∈ A → S : F ⟶ B
4 3 adantl ⊢ A ∈ V ∧ X ∈ A → S : F ⟶ B
5 simplr ⊢ A ∈ V ∧ X ∈ A ∧ g ∈ B ∧ x ∈ A → g ∈ B
6 5 fmpttd ⊢ A ∈ V ∧ X ∈ A ∧ g ∈ B → x ∈ A ⟼ g : A ⟶ B
7 simpll ⊢ A ∈ V ∧ X ∈ A ∧ g ∈ B → A ∈ V
8 7 mptexd ⊢ A ∈ V ∧ X ∈ A ∧ g ∈ B → x ∈ A ⟼ g ∈ V
9 feq1 ⊢ f = x ∈ A ⟼ g → f : A ⟶ B ↔ x ∈ A ⟼ g : A ⟶ B
10 9 1 elab2g ⊢ x ∈ A ⟼ g ∈ V → x ∈ A ⟼ g ∈ F ↔ x ∈ A ⟼ g : A ⟶ B
11 8 10 syl ⊢ A ∈ V ∧ X ∈ A ∧ g ∈ B → x ∈ A ⟼ g ∈ F ↔ x ∈ A ⟼ g : A ⟶ B
12 6 11 mpbird ⊢ A ∈ V ∧ X ∈ A ∧ g ∈ B → x ∈ A ⟼ g ∈ F
13 fveq1 ⊢ g = f → g ⁡ X = f ⁡ X
14 13 cbvmptv ⊢ g ∈ F ⟼ g ⁡ X = f ∈ F ⟼ f ⁡ X
15 2 14 eqtri ⊢ S = f ∈ F ⟼ f ⁡ X
16 fveq1 ⊢ f = x ∈ A ⟼ g → f ⁡ X = x ∈ A ⟼ g ⁡ X
17 fvexd ⊢ A ∈ V ∧ X ∈ A ∧ g ∈ B → x ∈ A ⟼ g ⁡ X ∈ V
18 15 16 12 17 fvmptd3 ⊢ A ∈ V ∧ X ∈ A ∧ g ∈ B → S ⁡ x ∈ A ⟼ g = x ∈ A ⟼ g ⁡ X
19 eqidd ⊢ x = X → g = g
20 eqid ⊢ x ∈ A ⟼ g = x ∈ A ⟼ g
21 vex ⊢ g ∈ V
22 19 20 21 fvmpt ⊢ X ∈ A → x ∈ A ⟼ g ⁡ X = g
23 22 ad2antlr ⊢ A ∈ V ∧ X ∈ A ∧ g ∈ B → x ∈ A ⟼ g ⁡ X = g
24 18 23 eqtrd ⊢ A ∈ V ∧ X ∈ A ∧ g ∈ B → S ⁡ x ∈ A ⟼ g = g
25 fveq2 ⊢ h = x ∈ A ⟼ g → S ⁡ h = S ⁡ x ∈ A ⟼ g
26 25 eqcomd ⊢ h = x ∈ A ⟼ g → S ⁡ x ∈ A ⟼ g = S ⁡ h
27 24 26 sylan9req ⊢ A ∈ V ∧ X ∈ A ∧ g ∈ B ∧ h = x ∈ A ⟼ g → g = S ⁡ h
28 12 27 rspcedeqvd ⊢ A ∈ V ∧ X ∈ A ∧ g ∈ B → ∃ h ∈ F g = S ⁡ h
29 28 ralrimiva ⊢ A ∈ V ∧ X ∈ A → ∀ g ∈ B ∃ h ∈ F g = S ⁡ h
30 dffo3 ⊢ S : F ⟶ onto B ↔ S : F ⟶ B ∧ ∀ g ∈ B ∃ h ∈ F g = S ⁡ h
31 4 29 30 sylanbrc ⊢ A ∈ V ∧ X ∈ A → S : F ⟶ onto B