Metamath Proof Explorer

Theorem cfsetsnfsetf1

Description: The mapping of the class of singleton functions into the class of constant functions is an injection. (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 cfsetsnfsetf1 
|- ( ( A e. V /\ Y e. A ) -> H : G -1-1-> 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 1 2 3 cfsetsnfsetfv 
 |-  ( ( A e. V /\ m e. G ) -> ( H ` m ) = ( a e. A |-> ( m ` Y ) ) )
6 5 ad2ant2r 
 |-  ( ( ( A e. V /\ Y e. A ) /\ ( m e. G /\ n e. G ) ) -> ( H ` m ) = ( a e. A |-> ( m ` Y ) ) )
7 1 2 3 cfsetsnfsetfv 
 |-  ( ( A e. V /\ n e. G ) -> ( H ` n ) = ( a e. A |-> ( n ` Y ) ) )
8 7 ad2ant2rl 
 |-  ( ( ( A e. V /\ Y e. A ) /\ ( m e. G /\ n e. G ) ) -> ( H ` n ) = ( a e. A |-> ( n ` Y ) ) )
9 6 8 eqeq12d 
 |-  ( ( ( A e. V /\ Y e. A ) /\ ( m e. G /\ n e. G ) ) -> ( ( H ` m ) = ( H ` n ) <-> ( a e. A |-> ( m ` Y ) ) = ( a e. A |-> ( n ` Y ) ) ) )
10 fvexd 
 |-  ( ( ( ( A e. V /\ Y e. A ) /\ ( m e. G /\ n e. G ) ) /\ a e. A ) -> ( m ` Y ) e. _V )
11 10 ralrimiva 
 |-  ( ( ( A e. V /\ Y e. A ) /\ ( m e. G /\ n e. G ) ) -> A. a e. A ( m ` Y ) e. _V )
12 mpteqb 
 |-  ( A. a e. A ( m ` Y ) e. _V -> ( ( a e. A |-> ( m ` Y ) ) = ( a e. A |-> ( n ` Y ) ) <-> A. a e. A ( m ` Y ) = ( n ` Y ) ) )
13 11 12 syl 
 |-  ( ( ( A e. V /\ Y e. A ) /\ ( m e. G /\ n e. G ) ) -> ( ( a e. A |-> ( m ` Y ) ) = ( a e. A |-> ( n ` Y ) ) <-> A. a e. A ( m ` Y ) = ( n ` Y ) ) )
14 simplr 
 |-  ( ( ( A e. V /\ Y e. A ) /\ ( m e. G /\ n e. G ) ) -> Y e. A )
15 idd 
 |-  ( ( ( ( A e. V /\ Y e. A ) /\ ( m e. G /\ n e. G ) ) /\ a = Y ) -> ( ( m ` Y ) = ( n ` Y ) -> ( m ` Y ) = ( n ` Y ) ) )
16 14 15 rspcimdv 
 |-  ( ( ( A e. V /\ Y e. A ) /\ ( m e. G /\ n e. G ) ) -> ( A. a e. A ( m ` Y ) = ( n ` Y ) -> ( m ` Y ) = ( n ` Y ) ) )
17 vex 
 |-  m e. _V
18 feq1 
 |-  ( x = m -> ( x : { Y } --> B <-> m : { Y } --> B ) )
19 17 18 2 elab2 
 |-  ( m e. G <-> m : { Y } --> B )
20 vex 
 |-  n e. _V
21 feq1 
 |-  ( x = n -> ( x : { Y } --> B <-> n : { Y } --> B ) )
22 20 21 2 elab2 
 |-  ( n e. G <-> n : { Y } --> B )
23 19 22 anbi12i 
 |-  ( ( m e. G /\ n e. G ) <-> ( m : { Y } --> B /\ n : { Y } --> B ) )
24 simp3 
 |-  ( ( ( A e. V /\ Y e. A ) /\ ( m : { Y } --> B /\ n : { Y } --> B ) /\ ( m ` Y ) = ( n ` Y ) ) -> ( m ` Y ) = ( n ` Y ) )
25 simp1r 
 |-  ( ( ( A e. V /\ Y e. A ) /\ ( m : { Y } --> B /\ n : { Y } --> B ) /\ ( m ` Y ) = ( n ` Y ) ) -> Y e. A )
26 fveq2 
 |-  ( y = Y -> ( m ` y ) = ( m ` Y ) )
27 fveq2 
 |-  ( y = Y -> ( n ` y ) = ( n ` Y ) )
28 26 27 eqeq12d 
 |-  ( y = Y -> ( ( m ` y ) = ( n ` y ) <-> ( m ` Y ) = ( n ` Y ) ) )
29 28 ralsng 
 |-  ( Y e. A -> ( A. y e. { Y } ( m ` y ) = ( n ` y ) <-> ( m ` Y ) = ( n ` Y ) ) )
30 25 29 syl 
 |-  ( ( ( A e. V /\ Y e. A ) /\ ( m : { Y } --> B /\ n : { Y } --> B ) /\ ( m ` Y ) = ( n ` Y ) ) -> ( A. y e. { Y } ( m ` y ) = ( n ` y ) <-> ( m ` Y ) = ( n ` Y ) ) )
31 24 30 mpbird 
 |-  ( ( ( A e. V /\ Y e. A ) /\ ( m : { Y } --> B /\ n : { Y } --> B ) /\ ( m ` Y ) = ( n ` Y ) ) -> A. y e. { Y } ( m ` y ) = ( n ` y ) )
32 ffn 
 |-  ( m : { Y } --> B -> m Fn { Y } )
33 ffn 
 |-  ( n : { Y } --> B -> n Fn { Y } )
34 32 33 anim12i 
 |-  ( ( m : { Y } --> B /\ n : { Y } --> B ) -> ( m Fn { Y } /\ n Fn { Y } ) )
35 34 3ad2ant2 
 |-  ( ( ( A e. V /\ Y e. A ) /\ ( m : { Y } --> B /\ n : { Y } --> B ) /\ ( m ` Y ) = ( n ` Y ) ) -> ( m Fn { Y } /\ n Fn { Y } ) )
36 eqfnfv 
 |-  ( ( m Fn { Y } /\ n Fn { Y } ) -> ( m = n <-> A. y e. { Y } ( m ` y ) = ( n ` y ) ) )
37 35 36 syl 
 |-  ( ( ( A e. V /\ Y e. A ) /\ ( m : { Y } --> B /\ n : { Y } --> B ) /\ ( m ` Y ) = ( n ` Y ) ) -> ( m = n <-> A. y e. { Y } ( m ` y ) = ( n ` y ) ) )
38 31 37 mpbird 
 |-  ( ( ( A e. V /\ Y e. A ) /\ ( m : { Y } --> B /\ n : { Y } --> B ) /\ ( m ` Y ) = ( n ` Y ) ) -> m = n )
39 38 3exp 
 |-  ( ( A e. V /\ Y e. A ) -> ( ( m : { Y } --> B /\ n : { Y } --> B ) -> ( ( m ` Y ) = ( n ` Y ) -> m = n ) ) )
40 23 39 syl5bi 
 |-  ( ( A e. V /\ Y e. A ) -> ( ( m e. G /\ n e. G ) -> ( ( m ` Y ) = ( n ` Y ) -> m = n ) ) )
41 40 imp 
 |-  ( ( ( A e. V /\ Y e. A ) /\ ( m e. G /\ n e. G ) ) -> ( ( m ` Y ) = ( n ` Y ) -> m = n ) )
42 16 41 syld 
 |-  ( ( ( A e. V /\ Y e. A ) /\ ( m e. G /\ n e. G ) ) -> ( A. a e. A ( m ` Y ) = ( n ` Y ) -> m = n ) )
43 13 42 sylbid 
 |-  ( ( ( A e. V /\ Y e. A ) /\ ( m e. G /\ n e. G ) ) -> ( ( a e. A |-> ( m ` Y ) ) = ( a e. A |-> ( n ` Y ) ) -> m = n ) )
44 9 43 sylbid 
 |-  ( ( ( A e. V /\ Y e. A ) /\ ( m e. G /\ n e. G ) ) -> ( ( H ` m ) = ( H ` n ) -> m = n ) )
45 44 ralrimivva 
 |-  ( ( A e. V /\ Y e. A ) -> A. m e. G A. n e. G ( ( H ` m ) = ( H ` n ) -> m = n ) )
46 dff13 
 |-  ( H : G -1-1-> F <-> ( H : G --> F /\ A. m e. G A. n e. G ( ( H ` m ) = ( H ` n ) -> m = n ) ) )
47 4 45 46 sylanbrc 
 |-  ( ( A e. V /\ Y e. A ) -> H : G -1-1-> F )