Metamath Proof Explorer

Theorem cfsetsnfsetfo

Description: The mapping of the class of singleton functions into the class of constant functions is a surjection. (Contributed by AV, 14-Sep-2024)

Ref Expression
Hypotheses cfsetsnfsetfv.f 
|- F = { f | ( f : A --> B /\ E. b e. B A. z e. A ( f ` z ) = b ) }
cfsetsnfsetfv.g 
|- G = { x | x : { Y } --> B }
cfsetsnfsetfv.h 
|- H = ( g e. G |-> ( a e. A |-> ( g ` Y ) ) )
Assertion cfsetsnfsetfo 
|- ( ( A e. V /\ Y e. A ) -> H : G -onto-> F )

Proof

Step Hyp Ref Expression
1 cfsetsnfsetfv.f 
 |-  F = { f | ( f : A --> B /\ E. b e. B A. z e. A ( f ` z ) = b ) }
2 cfsetsnfsetfv.g 
 |-  G = { x | x : { Y } --> B }
3 cfsetsnfsetfv.h 
 |-  H = ( g e. G |-> ( a e. A |-> ( g ` Y ) ) )
4 1 2 3 cfsetsnfsetf 
 |-  ( ( A e. V /\ Y e. A ) -> H : G --> F )
5 vex 
 |-  m e. _V
6 feq1 
 |-  ( f = m -> ( f : A --> B <-> m : A --> B ) )
7 fveq1 
 |-  ( f = m -> ( f ` z ) = ( m ` z ) )
8 7 adantr 
 |-  ( ( f = m /\ z e. A ) -> ( f ` z ) = ( m ` z ) )
9 8 eqeq1d 
 |-  ( ( f = m /\ z e. A ) -> ( ( f ` z ) = b <-> ( m ` z ) = b ) )
10 9 ralbidva 
 |-  ( f = m -> ( A. z e. A ( f ` z ) = b <-> A. z e. A ( m ` z ) = b ) )
11 10 rexbidv 
 |-  ( f = m -> ( E. b e. B A. z e. A ( f ` z ) = b <-> E. b e. B A. z e. A ( m ` z ) = b ) )
12 6 11 anbi12d 
 |-  ( f = m -> ( ( f : A --> B /\ E. b e. B A. z e. A ( f ` z ) = b ) <-> ( m : A --> B /\ E. b e. B A. z e. A ( m ` z ) = b ) ) )
13 5 12 1 elab2 
 |-  ( m e. F <-> ( m : A --> B /\ E. b e. B A. z e. A ( m ` z ) = b ) )
14 simpllr 
 |-  ( ( ( ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) /\ b e. B ) /\ A. z e. A ( m ` z ) = b ) /\ y e. { Y } ) -> b e. B )
15 eqid 
 |-  ( y e. { Y } |-> b ) = ( y e. { Y } |-> b )
16 14 15 fmptd 
 |-  ( ( ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) /\ b e. B ) /\ A. z e. A ( m ` z ) = b ) -> ( y e. { Y } |-> b ) : { Y } --> B )
17 snex 
 |-  { Y } e. _V
18 17 mptex 
 |-  ( y e. { Y } |-> b ) e. _V
19 feq1 
 |-  ( x = ( y e. { Y } |-> b ) -> ( x : { Y } --> B <-> ( y e. { Y } |-> b ) : { Y } --> B ) )
20 18 19 2 elab2 
 |-  ( ( y e. { Y } |-> b ) e. G <-> ( y e. { Y } |-> b ) : { Y } --> B )
21 16 20 sylibr 
 |-  ( ( ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) /\ b e. B ) /\ A. z e. A ( m ` z ) = b ) -> ( y e. { Y } |-> b ) e. G )
22 fveq1 
 |-  ( n = ( y e. { Y } |-> b ) -> ( n ` Y ) = ( ( y e. { Y } |-> b ) ` Y ) )
23 22 mpteq2dv 
 |-  ( n = ( y e. { Y } |-> b ) -> ( a e. A |-> ( n ` Y ) ) = ( a e. A |-> ( ( y e. { Y } |-> b ) ` Y ) ) )
24 23 eqeq2d 
 |-  ( n = ( y e. { Y } |-> b ) -> ( m = ( a e. A |-> ( n ` Y ) ) <-> m = ( a e. A |-> ( ( y e. { Y } |-> b ) ` Y ) ) ) )
25 24 adantl 
 |-  ( ( ( ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) /\ b e. B ) /\ A. z e. A ( m ` z ) = b ) /\ n = ( y e. { Y } |-> b ) ) -> ( m = ( a e. A |-> ( n ` Y ) ) <-> m = ( a e. A |-> ( ( y e. { Y } |-> b ) ` Y ) ) ) )
26 simpr 
 |-  ( ( ( ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) /\ b e. B ) /\ z e. A ) /\ ( m ` z ) = b ) -> ( m ` z ) = b )
27 eqidd 
 |-  ( ( ( ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) /\ b e. B ) /\ z e. A ) /\ ( m ` z ) = b ) -> ( a e. A |-> ( ( y e. { Y } |-> b ) ` Y ) ) = ( a e. A |-> ( ( y e. { Y } |-> b ) ` Y ) ) )
28 eqidd 
 |-  ( ( ( ( ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) /\ b e. B ) /\ z e. A ) /\ ( m ` z ) = b ) /\ a = z ) -> ( y e. { Y } |-> b ) = ( y e. { Y } |-> b ) )
29 eqidd 
 |-  ( ( ( ( ( ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) /\ b e. B ) /\ z e. A ) /\ ( m ` z ) = b ) /\ a = z ) /\ y = Y ) -> b = b )
30 snidg 
 |-  ( Y e. A -> Y e. { Y } )
31 30 ad6antlr 
 |-  ( ( ( ( ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) /\ b e. B ) /\ z e. A ) /\ ( m ` z ) = b ) /\ a = z ) -> Y e. { Y } )
32 simpllr 
 |-  ( ( ( ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) /\ b e. B ) /\ z e. A ) /\ ( m ` z ) = b ) -> b e. B )
33 32 adantr 
 |-  ( ( ( ( ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) /\ b e. B ) /\ z e. A ) /\ ( m ` z ) = b ) /\ a = z ) -> b e. B )
34 28 29 31 33 fvmptd 
 |-  ( ( ( ( ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) /\ b e. B ) /\ z e. A ) /\ ( m ` z ) = b ) /\ a = z ) -> ( ( y e. { Y } |-> b ) ` Y ) = b )
35 simpr 
 |-  ( ( ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) /\ b e. B ) /\ z e. A ) -> z e. A )
36 35 adantr 
 |-  ( ( ( ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) /\ b e. B ) /\ z e. A ) /\ ( m ` z ) = b ) -> z e. A )
37 27 34 36 32 fvmptd 
 |-  ( ( ( ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) /\ b e. B ) /\ z e. A ) /\ ( m ` z ) = b ) -> ( ( a e. A |-> ( ( y e. { Y } |-> b ) ` Y ) ) ` z ) = b )
38 26 37 eqtr4d 
 |-  ( ( ( ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) /\ b e. B ) /\ z e. A ) /\ ( m ` z ) = b ) -> ( m ` z ) = ( ( a e. A |-> ( ( y e. { Y } |-> b ) ` Y ) ) ` z ) )
39 38 ex 
 |-  ( ( ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) /\ b e. B ) /\ z e. A ) -> ( ( m ` z ) = b -> ( m ` z ) = ( ( a e. A |-> ( ( y e. { Y } |-> b ) ` Y ) ) ` z ) ) )
40 39 ralimdva 
 |-  ( ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) /\ b e. B ) -> ( A. z e. A ( m ` z ) = b -> A. z e. A ( m ` z ) = ( ( a e. A |-> ( ( y e. { Y } |-> b ) ` Y ) ) ` z ) ) )
41 40 imp 
 |-  ( ( ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) /\ b e. B ) /\ A. z e. A ( m ` z ) = b ) -> A. z e. A ( m ` z ) = ( ( a e. A |-> ( ( y e. { Y } |-> b ) ` Y ) ) ` z ) )
42 ffn 
 |-  ( m : A --> B -> m Fn A )
43 42 adantl 
 |-  ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) -> m Fn A )
44 nfv 
 |-  F/ a ( ( A e. V /\ Y e. A ) /\ m : A --> B )
45 fvexd 
 |-  ( ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) /\ a e. A ) -> ( ( y e. { Y } |-> b ) ` Y ) e. _V )
46 eqid 
 |-  ( a e. A |-> ( ( y e. { Y } |-> b ) ` Y ) ) = ( a e. A |-> ( ( y e. { Y } |-> b ) ` Y ) )
47 44 45 46 fnmptd 
 |-  ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) -> ( a e. A |-> ( ( y e. { Y } |-> b ) ` Y ) ) Fn A )
48 43 47 jca 
 |-  ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) -> ( m Fn A /\ ( a e. A |-> ( ( y e. { Y } |-> b ) ` Y ) ) Fn A ) )
49 48 adantr 
 |-  ( ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) /\ b e. B ) -> ( m Fn A /\ ( a e. A |-> ( ( y e. { Y } |-> b ) ` Y ) ) Fn A ) )
50 49 adantr 
 |-  ( ( ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) /\ b e. B ) /\ A. z e. A ( m ` z ) = b ) -> ( m Fn A /\ ( a e. A |-> ( ( y e. { Y } |-> b ) ` Y ) ) Fn A ) )
51 eqfnfv 
 |-  ( ( m Fn A /\ ( a e. A |-> ( ( y e. { Y } |-> b ) ` Y ) ) Fn A ) -> ( m = ( a e. A |-> ( ( y e. { Y } |-> b ) ` Y ) ) <-> A. z e. A ( m ` z ) = ( ( a e. A |-> ( ( y e. { Y } |-> b ) ` Y ) ) ` z ) ) )
52 50 51 syl 
 |-  ( ( ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) /\ b e. B ) /\ A. z e. A ( m ` z ) = b ) -> ( m = ( a e. A |-> ( ( y e. { Y } |-> b ) ` Y ) ) <-> A. z e. A ( m ` z ) = ( ( a e. A |-> ( ( y e. { Y } |-> b ) ` Y ) ) ` z ) ) )
53 41 52 mpbird 
 |-  ( ( ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) /\ b e. B ) /\ A. z e. A ( m ` z ) = b ) -> m = ( a e. A |-> ( ( y e. { Y } |-> b ) ` Y ) ) )
54 21 25 53 rspcedvd 
 |-  ( ( ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) /\ b e. B ) /\ A. z e. A ( m ` z ) = b ) -> E. n e. G m = ( a e. A |-> ( n ` Y ) ) )
55 simp-4l 
 |-  ( ( ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) /\ b e. B ) /\ A. z e. A ( m ` z ) = b ) -> A e. V )
56 1 2 3 cfsetsnfsetfv 
 |-  ( ( A e. V /\ n e. G ) -> ( H ` n ) = ( a e. A |-> ( n ` Y ) ) )
57 55 56 sylan 
 |-  ( ( ( ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) /\ b e. B ) /\ A. z e. A ( m ` z ) = b ) /\ n e. G ) -> ( H ` n ) = ( a e. A |-> ( n ` Y ) ) )
58 57 eqeq2d 
 |-  ( ( ( ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) /\ b e. B ) /\ A. z e. A ( m ` z ) = b ) /\ n e. G ) -> ( m = ( H ` n ) <-> m = ( a e. A |-> ( n ` Y ) ) ) )
59 58 rexbidva 
 |-  ( ( ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) /\ b e. B ) /\ A. z e. A ( m ` z ) = b ) -> ( E. n e. G m = ( H ` n ) <-> E. n e. G m = ( a e. A |-> ( n ` Y ) ) ) )
60 54 59 mpbird 
 |-  ( ( ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) /\ b e. B ) /\ A. z e. A ( m ` z ) = b ) -> E. n e. G m = ( H ` n ) )
61 60 ex 
 |-  ( ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) /\ b e. B ) -> ( A. z e. A ( m ` z ) = b -> E. n e. G m = ( H ` n ) ) )
62 61 rexlimdva 
 |-  ( ( ( A e. V /\ Y e. A ) /\ m : A --> B ) -> ( E. b e. B A. z e. A ( m ` z ) = b -> E. n e. G m = ( H ` n ) ) )
63 62 expimpd 
 |-  ( ( A e. V /\ Y e. A ) -> ( ( m : A --> B /\ E. b e. B A. z e. A ( m ` z ) = b ) -> E. n e. G m = ( H ` n ) ) )
64 13 63 syl5bi 
 |-  ( ( A e. V /\ Y e. A ) -> ( m e. F -> E. n e. G m = ( H ` n ) ) )
65 64 ralrimiv 
 |-  ( ( A e. V /\ Y e. A ) -> A. m e. F E. n e. G m = ( H ` n ) )
66 dffo3 
 |-  ( H : G -onto-> F <-> ( H : G --> F /\ A. m e. F E. n e. G m = ( H ` n ) ) )
67 4 65 66 sylanbrc 
 |-  ( ( A e. V /\ Y e. A ) -> H : G -onto-> F )