Metamath Proof Explorer

Theorem msubff1

Description: When restricted to complete mappings, the substitution-producing function is one-to-one. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses msubff1.v 
|- V = ( mVR ` T )
msubff1.r 
|- R = ( mREx ` T )
msubff1.s 
|- S = ( mSubst ` T )
msubff1.e 
|- E = ( mEx ` T )
Assertion msubff1 
|- ( T e. mFS -> ( S |` ( R ^m V ) ) : ( R ^m V ) -1-1-> ( E ^m E ) )

Proof

Step Hyp Ref Expression
1 msubff1.v 
 |-  V = ( mVR ` T )
2 msubff1.r 
 |-  R = ( mREx ` T )
3 msubff1.s 
 |-  S = ( mSubst ` T )
4 msubff1.e 
 |-  E = ( mEx ` T )
5 1 2 3 4 msubff 
 |-  ( T e. mFS -> S : ( R ^pm V ) --> ( E ^m E ) )
6 mapsspm 
 |-  ( R ^m V ) C_ ( R ^pm V )
7 6 a1i 
 |-  ( T e. mFS -> ( R ^m V ) C_ ( R ^pm V ) )
8 5 7 fssresd 
 |-  ( T e. mFS -> ( S |` ( R ^m V ) ) : ( R ^m V ) --> ( E ^m E ) )
9 eqid 
 |-  ( mRSubst ` T ) = ( mRSubst ` T )
10 1 2 9 mrsubff 
 |-  ( T e. mFS -> ( mRSubst ` T ) : ( R ^pm V ) --> ( R ^m R ) )
11 10 ad2antrr 
 |-  ( ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ ( v e. V /\ ( S ` f ) = ( S ` g ) ) ) -> ( mRSubst ` T ) : ( R ^pm V ) --> ( R ^m R ) )
12 simplrl 
 |-  ( ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ ( v e. V /\ ( S ` f ) = ( S ` g ) ) ) -> f e. ( R ^m V ) )
13 6 12 sseldi 
 |-  ( ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ ( v e. V /\ ( S ` f ) = ( S ` g ) ) ) -> f e. ( R ^pm V ) )
14 11 13 ffvelrnd 
 |-  ( ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ ( v e. V /\ ( S ` f ) = ( S ` g ) ) ) -> ( ( mRSubst ` T ) ` f ) e. ( R ^m R ) )
15 elmapi 
 |-  ( ( ( mRSubst ` T ) ` f ) e. ( R ^m R ) -> ( ( mRSubst ` T ) ` f ) : R --> R )
16 ffn 
 |-  ( ( ( mRSubst ` T ) ` f ) : R --> R -> ( ( mRSubst ` T ) ` f ) Fn R )
17 14 15 16 3syl 
 |-  ( ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ ( v e. V /\ ( S ` f ) = ( S ` g ) ) ) -> ( ( mRSubst ` T ) ` f ) Fn R )
18 simplrr 
 |-  ( ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ ( v e. V /\ ( S ` f ) = ( S ` g ) ) ) -> g e. ( R ^m V ) )
19 6 18 sseldi 
 |-  ( ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ ( v e. V /\ ( S ` f ) = ( S ` g ) ) ) -> g e. ( R ^pm V ) )
20 11 19 ffvelrnd 
 |-  ( ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ ( v e. V /\ ( S ` f ) = ( S ` g ) ) ) -> ( ( mRSubst ` T ) ` g ) e. ( R ^m R ) )
21 elmapi 
 |-  ( ( ( mRSubst ` T ) ` g ) e. ( R ^m R ) -> ( ( mRSubst ` T ) ` g ) : R --> R )
22 ffn 
 |-  ( ( ( mRSubst ` T ) ` g ) : R --> R -> ( ( mRSubst ` T ) ` g ) Fn R )
23 20 21 22 3syl 
 |-  ( ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ ( v e. V /\ ( S ` f ) = ( S ` g ) ) ) -> ( ( mRSubst ` T ) ` g ) Fn R )
24 simplrr 
 |-  ( ( ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ ( v e. V /\ ( S ` f ) = ( S ` g ) ) ) /\ r e. R ) -> ( S ` f ) = ( S ` g ) )
25 24 fveq1d 
 |-  ( ( ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ ( v e. V /\ ( S ` f ) = ( S ` g ) ) ) /\ r e. R ) -> ( ( S ` f ) ` <. ( ( mType ` T ) ` v ) , r >. ) = ( ( S ` g ) ` <. ( ( mType ` T ) ` v ) , r >. ) )
26 12 adantr 
 |-  ( ( ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ ( v e. V /\ ( S ` f ) = ( S ` g ) ) ) /\ r e. R ) -> f e. ( R ^m V ) )
27 elmapi 
 |-  ( f e. ( R ^m V ) -> f : V --> R )
28 26 27 syl 
 |-  ( ( ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ ( v e. V /\ ( S ` f ) = ( S ` g ) ) ) /\ r e. R ) -> f : V --> R )
29 ssidd 
 |-  ( ( ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ ( v e. V /\ ( S ` f ) = ( S ` g ) ) ) /\ r e. R ) -> V C_ V )
30 eqid 
 |-  ( mTC ` T ) = ( mTC ` T )
31 eqid 
 |-  ( mType ` T ) = ( mType ` T )
32 1 30 31 mtyf2 
 |-  ( T e. mFS -> ( mType ` T ) : V --> ( mTC ` T ) )
33 32 ad3antrrr 
 |-  ( ( ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ ( v e. V /\ ( S ` f ) = ( S ` g ) ) ) /\ r e. R ) -> ( mType ` T ) : V --> ( mTC ` T ) )
34 simplrl 
 |-  ( ( ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ ( v e. V /\ ( S ` f ) = ( S ` g ) ) ) /\ r e. R ) -> v e. V )
35 33 34 ffvelrnd 
 |-  ( ( ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ ( v e. V /\ ( S ` f ) = ( S ` g ) ) ) /\ r e. R ) -> ( ( mType ` T ) ` v ) e. ( mTC ` T ) )
36 opelxpi 
 |-  ( ( ( ( mType ` T ) ` v ) e. ( mTC ` T ) /\ r e. R ) -> <. ( ( mType ` T ) ` v ) , r >. e. ( ( mTC ` T ) X. R ) )
37 35 36 sylancom 
 |-  ( ( ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ ( v e. V /\ ( S ` f ) = ( S ` g ) ) ) /\ r e. R ) -> <. ( ( mType ` T ) ` v ) , r >. e. ( ( mTC ` T ) X. R ) )
38 30 4 2 mexval 
 |-  E = ( ( mTC ` T ) X. R )
39 37 38 eleqtrrdi 
 |-  ( ( ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ ( v e. V /\ ( S ` f ) = ( S ` g ) ) ) /\ r e. R ) -> <. ( ( mType ` T ) ` v ) , r >. e. E )
40 1 2 3 4 9 msubval 
 |-  ( ( f : V --> R /\ V C_ V /\ <. ( ( mType ` T ) ` v ) , r >. e. E ) -> ( ( S ` f ) ` <. ( ( mType ` T ) ` v ) , r >. ) = <. ( 1st ` <. ( ( mType ` T ) ` v ) , r >. ) , ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` <. ( ( mType ` T ) ` v ) , r >. ) ) >. )
41 28 29 39 40 syl3anc 
 |-  ( ( ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ ( v e. V /\ ( S ` f ) = ( S ` g ) ) ) /\ r e. R ) -> ( ( S ` f ) ` <. ( ( mType ` T ) ` v ) , r >. ) = <. ( 1st ` <. ( ( mType ` T ) ` v ) , r >. ) , ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` <. ( ( mType ` T ) ` v ) , r >. ) ) >. )
42 18 adantr 
 |-  ( ( ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ ( v e. V /\ ( S ` f ) = ( S ` g ) ) ) /\ r e. R ) -> g e. ( R ^m V ) )
43 elmapi 
 |-  ( g e. ( R ^m V ) -> g : V --> R )
44 42 43 syl 
 |-  ( ( ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ ( v e. V /\ ( S ` f ) = ( S ` g ) ) ) /\ r e. R ) -> g : V --> R )
45 1 2 3 4 9 msubval 
 |-  ( ( g : V --> R /\ V C_ V /\ <. ( ( mType ` T ) ` v ) , r >. e. E ) -> ( ( S ` g ) ` <. ( ( mType ` T ) ` v ) , r >. ) = <. ( 1st ` <. ( ( mType ` T ) ` v ) , r >. ) , ( ( ( mRSubst ` T ) ` g ) ` ( 2nd ` <. ( ( mType ` T ) ` v ) , r >. ) ) >. )
46 44 29 39 45 syl3anc 
 |-  ( ( ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ ( v e. V /\ ( S ` f ) = ( S ` g ) ) ) /\ r e. R ) -> ( ( S ` g ) ` <. ( ( mType ` T ) ` v ) , r >. ) = <. ( 1st ` <. ( ( mType ` T ) ` v ) , r >. ) , ( ( ( mRSubst ` T ) ` g ) ` ( 2nd ` <. ( ( mType ` T ) ` v ) , r >. ) ) >. )
47 25 41 46 3eqtr3d 
 |-  ( ( ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ ( v e. V /\ ( S ` f ) = ( S ` g ) ) ) /\ r e. R ) -> <. ( 1st ` <. ( ( mType ` T ) ` v ) , r >. ) , ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` <. ( ( mType ` T ) ` v ) , r >. ) ) >. = <. ( 1st ` <. ( ( mType ` T ) ` v ) , r >. ) , ( ( ( mRSubst ` T ) ` g ) ` ( 2nd ` <. ( ( mType ` T ) ` v ) , r >. ) ) >. )
48 fvex 
 |-  ( 1st ` <. ( ( mType ` T ) ` v ) , r >. ) e. _V
49 fvex 
 |-  ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` <. ( ( mType ` T ) ` v ) , r >. ) ) e. _V
50 48 49 opth 
 |-  ( <. ( 1st ` <. ( ( mType ` T ) ` v ) , r >. ) , ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` <. ( ( mType ` T ) ` v ) , r >. ) ) >. = <. ( 1st ` <. ( ( mType ` T ) ` v ) , r >. ) , ( ( ( mRSubst ` T ) ` g ) ` ( 2nd ` <. ( ( mType ` T ) ` v ) , r >. ) ) >. <-> ( ( 1st ` <. ( ( mType ` T ) ` v ) , r >. ) = ( 1st ` <. ( ( mType ` T ) ` v ) , r >. ) /\ ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` <. ( ( mType ` T ) ` v ) , r >. ) ) = ( ( ( mRSubst ` T ) ` g ) ` ( 2nd ` <. ( ( mType ` T ) ` v ) , r >. ) ) ) )
51 50 simprbi 
 |-  ( <. ( 1st ` <. ( ( mType ` T ) ` v ) , r >. ) , ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` <. ( ( mType ` T ) ` v ) , r >. ) ) >. = <. ( 1st ` <. ( ( mType ` T ) ` v ) , r >. ) , ( ( ( mRSubst ` T ) ` g ) ` ( 2nd ` <. ( ( mType ` T ) ` v ) , r >. ) ) >. -> ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` <. ( ( mType ` T ) ` v ) , r >. ) ) = ( ( ( mRSubst ` T ) ` g ) ` ( 2nd ` <. ( ( mType ` T ) ` v ) , r >. ) ) )
52 47 51 syl 
 |-  ( ( ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ ( v e. V /\ ( S ` f ) = ( S ` g ) ) ) /\ r e. R ) -> ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` <. ( ( mType ` T ) ` v ) , r >. ) ) = ( ( ( mRSubst ` T ) ` g ) ` ( 2nd ` <. ( ( mType ` T ) ` v ) , r >. ) ) )
53 fvex 
 |-  ( ( mType ` T ) ` v ) e. _V
54 vex 
 |-  r e. _V
55 53 54 op2nd 
 |-  ( 2nd ` <. ( ( mType ` T ) ` v ) , r >. ) = r
56 55 fveq2i 
 |-  ( ( ( mRSubst ` T ) ` f ) ` ( 2nd ` <. ( ( mType ` T ) ` v ) , r >. ) ) = ( ( ( mRSubst ` T ) ` f ) ` r )
57 55 fveq2i 
 |-  ( ( ( mRSubst ` T ) ` g ) ` ( 2nd ` <. ( ( mType ` T ) ` v ) , r >. ) ) = ( ( ( mRSubst ` T ) ` g ) ` r )
58 52 56 57 3eqtr3g 
 |-  ( ( ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ ( v e. V /\ ( S ` f ) = ( S ` g ) ) ) /\ r e. R ) -> ( ( ( mRSubst ` T ) ` f ) ` r ) = ( ( ( mRSubst ` T ) ` g ) ` r ) )
59 17 23 58 eqfnfvd 
 |-  ( ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ ( v e. V /\ ( S ` f ) = ( S ` g ) ) ) -> ( ( mRSubst ` T ) ` f ) = ( ( mRSubst ` T ) ` g ) )
60 1 2 9 mrsubff1 
 |-  ( T e. mFS -> ( ( mRSubst ` T ) |` ( R ^m V ) ) : ( R ^m V ) -1-1-> ( R ^m R ) )
61 f1fveq 
 |-  ( ( ( ( mRSubst ` T ) |` ( R ^m V ) ) : ( R ^m V ) -1-1-> ( R ^m R ) /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) -> ( ( ( ( mRSubst ` T ) |` ( R ^m V ) ) ` f ) = ( ( ( mRSubst ` T ) |` ( R ^m V ) ) ` g ) <-> f = g ) )
62 60 61 sylan 
 |-  ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) -> ( ( ( ( mRSubst ` T ) |` ( R ^m V ) ) ` f ) = ( ( ( mRSubst ` T ) |` ( R ^m V ) ) ` g ) <-> f = g ) )
63 fvres 
 |-  ( f e. ( R ^m V ) -> ( ( ( mRSubst ` T ) |` ( R ^m V ) ) ` f ) = ( ( mRSubst ` T ) ` f ) )
64 fvres 
 |-  ( g e. ( R ^m V ) -> ( ( ( mRSubst ` T ) |` ( R ^m V ) ) ` g ) = ( ( mRSubst ` T ) ` g ) )
65 63 64 eqeqan12d 
 |-  ( ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) -> ( ( ( ( mRSubst ` T ) |` ( R ^m V ) ) ` f ) = ( ( ( mRSubst ` T ) |` ( R ^m V ) ) ` g ) <-> ( ( mRSubst ` T ) ` f ) = ( ( mRSubst ` T ) ` g ) ) )
66 65 adantl 
 |-  ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) -> ( ( ( ( mRSubst ` T ) |` ( R ^m V ) ) ` f ) = ( ( ( mRSubst ` T ) |` ( R ^m V ) ) ` g ) <-> ( ( mRSubst ` T ) ` f ) = ( ( mRSubst ` T ) ` g ) ) )
67 62 66 bitr3d 
 |-  ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) -> ( f = g <-> ( ( mRSubst ` T ) ` f ) = ( ( mRSubst ` T ) ` g ) ) )
68 67 adantr 
 |-  ( ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ ( v e. V /\ ( S ` f ) = ( S ` g ) ) ) -> ( f = g <-> ( ( mRSubst ` T ) ` f ) = ( ( mRSubst ` T ) ` g ) ) )
69 59 68 mpbird 
 |-  ( ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ ( v e. V /\ ( S ` f ) = ( S ` g ) ) ) -> f = g )
70 69 fveq1d 
 |-  ( ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ ( v e. V /\ ( S ` f ) = ( S ` g ) ) ) -> ( f ` v ) = ( g ` v ) )
71 70 expr 
 |-  ( ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) /\ v e. V ) -> ( ( S ` f ) = ( S ` g ) -> ( f ` v ) = ( g ` v ) ) )
72 71 ralrimdva 
 |-  ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) -> ( ( S ` f ) = ( S ` g ) -> A. v e. V ( f ` v ) = ( g ` v ) ) )
73 fvres 
 |-  ( f e. ( R ^m V ) -> ( ( S |` ( R ^m V ) ) ` f ) = ( S ` f ) )
74 fvres 
 |-  ( g e. ( R ^m V ) -> ( ( S |` ( R ^m V ) ) ` g ) = ( S ` g ) )
75 73 74 eqeqan12d 
 |-  ( ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) -> ( ( ( S |` ( R ^m V ) ) ` f ) = ( ( S |` ( R ^m V ) ) ` g ) <-> ( S ` f ) = ( S ` g ) ) )
76 75 adantl 
 |-  ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) -> ( ( ( S |` ( R ^m V ) ) ` f ) = ( ( S |` ( R ^m V ) ) ` g ) <-> ( S ` f ) = ( S ` g ) ) )
77 ffn 
 |-  ( f : V --> R -> f Fn V )
78 ffn 
 |-  ( g : V --> R -> g Fn V )
79 eqfnfv 
 |-  ( ( f Fn V /\ g Fn V ) -> ( f = g <-> A. v e. V ( f ` v ) = ( g ` v ) ) )
80 77 78 79 syl2an 
 |-  ( ( f : V --> R /\ g : V --> R ) -> ( f = g <-> A. v e. V ( f ` v ) = ( g ` v ) ) )
81 27 43 80 syl2an 
 |-  ( ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) -> ( f = g <-> A. v e. V ( f ` v ) = ( g ` v ) ) )
82 81 adantl 
 |-  ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) -> ( f = g <-> A. v e. V ( f ` v ) = ( g ` v ) ) )
83 72 76 82 3imtr4d 
 |-  ( ( T e. mFS /\ ( f e. ( R ^m V ) /\ g e. ( R ^m V ) ) ) -> ( ( ( S |` ( R ^m V ) ) ` f ) = ( ( S |` ( R ^m V ) ) ` g ) -> f = g ) )
84 83 ralrimivva 
 |-  ( T e. mFS -> A. f e. ( R ^m V ) A. g e. ( R ^m V ) ( ( ( S |` ( R ^m V ) ) ` f ) = ( ( S |` ( R ^m V ) ) ` g ) -> f = g ) )
85 dff13 
 |-  ( ( S |` ( R ^m V ) ) : ( R ^m V ) -1-1-> ( E ^m E ) <-> ( ( S |` ( R ^m V ) ) : ( R ^m V ) --> ( E ^m E ) /\ A. f e. ( R ^m V ) A. g e. ( R ^m V ) ( ( ( S |` ( R ^m V ) ) ` f ) = ( ( S |` ( R ^m V ) ) ` g ) -> f = g ) ) )
86 8 84 85 sylanbrc 
 |-  ( T e. mFS -> ( S |` ( R ^m V ) ) : ( R ^m V ) -1-1-> ( E ^m E ) )