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 
|- F = { f | f : A --> B }
fsetfocdm.s 
|- S = ( g e. F |-> ( g ` X ) )
Assertion fsetfocdm 
|- ( ( A e. V /\ X e. A ) -> S : F -onto-> B )

Proof

Step Hyp Ref Expression
1 fsetfocdm.f 
 |-  F = { f | f : A --> B }
2 fsetfocdm.s 
 |-  S = ( g e. F |-> ( g ` X ) )
3 1 2 fsetfcdm 
 |-  ( X e. A -> S : F --> B )
4 3 adantl 
 |-  ( ( A e. V /\ X e. A ) -> S : F --> B )
5 simplr 
 |-  ( ( ( ( A e. V /\ X e. A ) /\ g e. B ) /\ x e. A ) -> g e. B )
6 5 fmpttd 
 |-  ( ( ( A e. V /\ X e. A ) /\ g e. B ) -> ( x e. A |-> g ) : A --> B )
7 simpll 
 |-  ( ( ( A e. V /\ X e. A ) /\ g e. B ) -> A e. V )
8 7 mptexd 
 |-  ( ( ( A e. V /\ X e. A ) /\ g e. B ) -> ( x e. A |-> g ) e. _V )
9 feq1 
 |-  ( f = ( x e. A |-> g ) -> ( f : A --> B <-> ( x e. A |-> g ) : A --> B ) )
10 9 1 elab2g 
 |-  ( ( x e. A |-> g ) e. _V -> ( ( x e. A |-> g ) e. F <-> ( x e. A |-> g ) : A --> B ) )
11 8 10 syl 
 |-  ( ( ( A e. V /\ X e. A ) /\ g e. B ) -> ( ( x e. A |-> g ) e. F <-> ( x e. A |-> g ) : A --> B ) )
12 6 11 mpbird 
 |-  ( ( ( A e. V /\ X e. A ) /\ g e. B ) -> ( x e. A |-> g ) e. F )
13 fveq1 
 |-  ( g = f -> ( g ` X ) = ( f ` X ) )
14 13 cbvmptv 
 |-  ( g e. F |-> ( g ` X ) ) = ( f e. F |-> ( f ` X ) )
15 2 14 eqtri 
 |-  S = ( f e. F |-> ( f ` X ) )
16 fveq1 
 |-  ( f = ( x e. A |-> g ) -> ( f ` X ) = ( ( x e. A |-> g ) ` X ) )
17 fvexd 
 |-  ( ( ( A e. V /\ X e. A ) /\ g e. B ) -> ( ( x e. A |-> g ) ` X ) e. _V )
18 15 16 12 17 fvmptd3 
 |-  ( ( ( A e. V /\ X e. A ) /\ g e. B ) -> ( S ` ( x e. A |-> g ) ) = ( ( x e. A |-> g ) ` X ) )
19 eqidd 
 |-  ( x = X -> g = g )
20 eqid 
 |-  ( x e. A |-> g ) = ( x e. A |-> g )
21 vex 
 |-  g e. _V
22 19 20 21 fvmpt 
 |-  ( X e. A -> ( ( x e. A |-> g ) ` X ) = g )
23 22 ad2antlr 
 |-  ( ( ( A e. V /\ X e. A ) /\ g e. B ) -> ( ( x e. A |-> g ) ` X ) = g )
24 18 23 eqtrd 
 |-  ( ( ( A e. V /\ X e. A ) /\ g e. B ) -> ( S ` ( x e. A |-> g ) ) = g )
25 fveq2 
 |-  ( h = ( x e. A |-> g ) -> ( S ` h ) = ( S ` ( x e. A |-> g ) ) )
26 25 eqcomd 
 |-  ( h = ( x e. A |-> g ) -> ( S ` ( x e. A |-> g ) ) = ( S ` h ) )
27 24 26 sylan9req 
 |-  ( ( ( ( A e. V /\ X e. A ) /\ g e. B ) /\ h = ( x e. A |-> g ) ) -> g = ( S ` h ) )
28 12 27 rspcedeq2vd 
 |-  ( ( ( A e. V /\ X e. A ) /\ g e. B ) -> E. h e. F g = ( S ` h ) )
29 28 ralrimiva 
 |-  ( ( A e. V /\ X e. A ) -> A. g e. B E. h e. F g = ( S ` h ) )
30 dffo3 
 |-  ( S : F -onto-> B <-> ( S : F --> B /\ A. g e. B E. h e. F g = ( S ` h ) ) )
31 4 29 30 sylanbrc 
 |-  ( ( A e. V /\ X e. A ) -> S : F -onto-> B )