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 sselid
 |-  ( ( ( 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 sselid
 |-  ( ( ( 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 ) )