Metamath Proof Explorer

Theorem msubco

Description: The composition of two substitutions is a substitution. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypothesis msubco.s 
|- S = ( mSubst ` T )
Assertion msubco 
|- ( ( F e. ran S /\ G e. ran S ) -> ( F o. G ) e. ran S )

Proof

Step Hyp Ref Expression
1 msubco.s 
 |-  S = ( mSubst ` T )
2 eqid 
 |-  ( mEx ` T ) = ( mEx ` T )
3 eqid 
 |-  ( mRSubst ` T ) = ( mRSubst ` T )
4 2 3 1 elmsubrn 
 |-  ran S = ran ( f e. ran ( mRSubst ` T ) |-> ( x e. ( mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) )
5 4 eleq2i 
 |-  ( F e. ran S <-> F e. ran ( f e. ran ( mRSubst ` T ) |-> ( x e. ( mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) ) )
6 eqid 
 |-  ( f e. ran ( mRSubst ` T ) |-> ( x e. ( mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) ) = ( f e. ran ( mRSubst ` T ) |-> ( x e. ( mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) )
7 fvex 
 |-  ( mEx ` T ) e. _V
8 7 mptex 
 |-  ( x e. ( mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) e. _V
9 6 8 elrnmpti 
 |-  ( F e. ran ( f e. ran ( mRSubst ` T ) |-> ( x e. ( mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) ) <-> E. f e. ran ( mRSubst ` T ) F = ( x e. ( mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) )
10 5 9 bitri 
 |-  ( F e. ran S <-> E. f e. ran ( mRSubst ` T ) F = ( x e. ( mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) )
11 2 3 1 elmsubrn 
 |-  ran S = ran ( g e. ran ( mRSubst ` T ) |-> ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) )
12 11 eleq2i 
 |-  ( G e. ran S <-> G e. ran ( g e. ran ( mRSubst ` T ) |-> ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) ) )
13 eqid 
 |-  ( g e. ran ( mRSubst ` T ) |-> ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) ) = ( g e. ran ( mRSubst ` T ) |-> ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) )
14 7 mptex 
 |-  ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) e. _V
15 13 14 elrnmpti 
 |-  ( G e. ran ( g e. ran ( mRSubst ` T ) |-> ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) ) <-> E. g e. ran ( mRSubst ` T ) G = ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) )
16 12 15 bitri 
 |-  ( G e. ran S <-> E. g e. ran ( mRSubst ` T ) G = ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) )
17 reeanv 
 |-  ( E. f e. ran ( mRSubst ` T ) E. g e. ran ( mRSubst ` T ) ( F = ( x e. ( mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) /\ G = ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) ) <-> ( E. f e. ran ( mRSubst ` T ) F = ( x e. ( mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) /\ E. g e. ran ( mRSubst ` T ) G = ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) ) )
18 simpr 
 |-  ( ( ( f e. ran ( mRSubst ` T ) /\ g e. ran ( mRSubst ` T ) ) /\ y e. ( mEx ` T ) ) -> y e. ( mEx ` T ) )
19 eqid 
 |-  ( mTC ` T ) = ( mTC ` T )
20 eqid 
 |-  ( mREx ` T ) = ( mREx ` T )
21 19 2 20 mexval 
 |-  ( mEx ` T ) = ( ( mTC ` T ) X. ( mREx ` T ) )
22 18 21 eleqtrdi 
 |-  ( ( ( f e. ran ( mRSubst ` T ) /\ g e. ran ( mRSubst ` T ) ) /\ y e. ( mEx ` T ) ) -> y e. ( ( mTC ` T ) X. ( mREx ` T ) ) )
23 xp1st 
 |-  ( y e. ( ( mTC ` T ) X. ( mREx ` T ) ) -> ( 1st ` y ) e. ( mTC ` T ) )
24 22 23 syl 
 |-  ( ( ( f e. ran ( mRSubst ` T ) /\ g e. ran ( mRSubst ` T ) ) /\ y e. ( mEx ` T ) ) -> ( 1st ` y ) e. ( mTC ` T ) )
25 3 20 mrsubf 
 |-  ( g e. ran ( mRSubst ` T ) -> g : ( mREx ` T ) --> ( mREx ` T ) )
26 25 ad2antlr 
 |-  ( ( ( f e. ran ( mRSubst ` T ) /\ g e. ran ( mRSubst ` T ) ) /\ y e. ( mEx ` T ) ) -> g : ( mREx ` T ) --> ( mREx ` T ) )
27 xp2nd 
 |-  ( y e. ( ( mTC ` T ) X. ( mREx ` T ) ) -> ( 2nd ` y ) e. ( mREx ` T ) )
28 22 27 syl 
 |-  ( ( ( f e. ran ( mRSubst ` T ) /\ g e. ran ( mRSubst ` T ) ) /\ y e. ( mEx ` T ) ) -> ( 2nd ` y ) e. ( mREx ` T ) )
29 26 28 ffvelcdmd 
 |-  ( ( ( f e. ran ( mRSubst ` T ) /\ g e. ran ( mRSubst ` T ) ) /\ y e. ( mEx ` T ) ) -> ( g ` ( 2nd ` y ) ) e. ( mREx ` T ) )
30 opelxpi 
 |-  ( ( ( 1st ` y ) e. ( mTC ` T ) /\ ( g ` ( 2nd ` y ) ) e. ( mREx ` T ) ) -> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. e. ( ( mTC ` T ) X. ( mREx ` T ) ) )
31 24 29 30 syl2anc 
 |-  ( ( ( f e. ran ( mRSubst ` T ) /\ g e. ran ( mRSubst ` T ) ) /\ y e. ( mEx ` T ) ) -> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. e. ( ( mTC ` T ) X. ( mREx ` T ) ) )
32 31 21 eleqtrrdi 
 |-  ( ( ( f e. ran ( mRSubst ` T ) /\ g e. ran ( mRSubst ` T ) ) /\ y e. ( mEx ` T ) ) -> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. e. ( mEx ` T ) )
33 eqidd 
 |-  ( ( f e. ran ( mRSubst ` T ) /\ g e. ran ( mRSubst ` T ) ) -> ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) = ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) )
34 eqidd 
 |-  ( ( f e. ran ( mRSubst ` T ) /\ g e. ran ( mRSubst ` T ) ) -> ( x e. ( mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) = ( x e. ( mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) )
35 fvex 
 |-  ( 1st ` y ) e. _V
36 fvex 
 |-  ( g ` ( 2nd ` y ) ) e. _V
37 35 36 op1std 
 |-  ( x = <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. -> ( 1st ` x ) = ( 1st ` y ) )
38 35 36 op2ndd 
 |-  ( x = <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. -> ( 2nd ` x ) = ( g ` ( 2nd ` y ) ) )
39 38 fveq2d 
 |-  ( x = <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. -> ( f ` ( 2nd ` x ) ) = ( f ` ( g ` ( 2nd ` y ) ) ) )
40 37 39 opeq12d 
 |-  ( x = <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. -> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. = <. ( 1st ` y ) , ( f ` ( g ` ( 2nd ` y ) ) ) >. )
41 32 33 34 40 fmptco 
 |-  ( ( f e. ran ( mRSubst ` T ) /\ g e. ran ( mRSubst ` T ) ) -> ( ( x e. ( mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) o. ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) ) = ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( f ` ( g ` ( 2nd ` y ) ) ) >. ) )
42 fvco3 
 |-  ( ( g : ( mREx ` T ) --> ( mREx ` T ) /\ ( 2nd ` y ) e. ( mREx ` T ) ) -> ( ( f o. g ) ` ( 2nd ` y ) ) = ( f ` ( g ` ( 2nd ` y ) ) ) )
43 26 28 42 syl2anc 
 |-  ( ( ( f e. ran ( mRSubst ` T ) /\ g e. ran ( mRSubst ` T ) ) /\ y e. ( mEx ` T ) ) -> ( ( f o. g ) ` ( 2nd ` y ) ) = ( f ` ( g ` ( 2nd ` y ) ) ) )
44 43 opeq2d 
 |-  ( ( ( f e. ran ( mRSubst ` T ) /\ g e. ran ( mRSubst ` T ) ) /\ y e. ( mEx ` T ) ) -> <. ( 1st ` y ) , ( ( f o. g ) ` ( 2nd ` y ) ) >. = <. ( 1st ` y ) , ( f ` ( g ` ( 2nd ` y ) ) ) >. )
45 44 mpteq2dva 
 |-  ( ( f e. ran ( mRSubst ` T ) /\ g e. ran ( mRSubst ` T ) ) -> ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( ( f o. g ) ` ( 2nd ` y ) ) >. ) = ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( f ` ( g ` ( 2nd ` y ) ) ) >. ) )
46 41 45 eqtr4d 
 |-  ( ( f e. ran ( mRSubst ` T ) /\ g e. ran ( mRSubst ` T ) ) -> ( ( x e. ( mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) o. ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) ) = ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( ( f o. g ) ` ( 2nd ` y ) ) >. ) )
47 3 mrsubco 
 |-  ( ( f e. ran ( mRSubst ` T ) /\ g e. ran ( mRSubst ` T ) ) -> ( f o. g ) e. ran ( mRSubst ` T ) )
48 7 mptex 
 |-  ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( ( f o. g ) ` ( 2nd ` y ) ) >. ) e. _V
49 eqid 
 |-  ( h e. ran ( mRSubst ` T ) |-> ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( h ` ( 2nd ` y ) ) >. ) ) = ( h e. ran ( mRSubst ` T ) |-> ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( h ` ( 2nd ` y ) ) >. ) )
50 fveq1 
 |-  ( h = ( f o. g ) -> ( h ` ( 2nd ` y ) ) = ( ( f o. g ) ` ( 2nd ` y ) ) )
51 50 opeq2d 
 |-  ( h = ( f o. g ) -> <. ( 1st ` y ) , ( h ` ( 2nd ` y ) ) >. = <. ( 1st ` y ) , ( ( f o. g ) ` ( 2nd ` y ) ) >. )
52 51 mpteq2dv 
 |-  ( h = ( f o. g ) -> ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( h ` ( 2nd ` y ) ) >. ) = ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( ( f o. g ) ` ( 2nd ` y ) ) >. ) )
53 49 52 elrnmpt1s 
 |-  ( ( ( f o. g ) e. ran ( mRSubst ` T ) /\ ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( ( f o. g ) ` ( 2nd ` y ) ) >. ) e. _V ) -> ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( ( f o. g ) ` ( 2nd ` y ) ) >. ) e. ran ( h e. ran ( mRSubst ` T ) |-> ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( h ` ( 2nd ` y ) ) >. ) ) )
54 47 48 53 sylancl 
 |-  ( ( f e. ran ( mRSubst ` T ) /\ g e. ran ( mRSubst ` T ) ) -> ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( ( f o. g ) ` ( 2nd ` y ) ) >. ) e. ran ( h e. ran ( mRSubst ` T ) |-> ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( h ` ( 2nd ` y ) ) >. ) ) )
55 2 3 1 elmsubrn 
 |-  ran S = ran ( h e. ran ( mRSubst ` T ) |-> ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( h ` ( 2nd ` y ) ) >. ) )
56 54 55 eleqtrrdi 
 |-  ( ( f e. ran ( mRSubst ` T ) /\ g e. ran ( mRSubst ` T ) ) -> ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( ( f o. g ) ` ( 2nd ` y ) ) >. ) e. ran S )
57 46 56 eqeltrd 
 |-  ( ( f e. ran ( mRSubst ` T ) /\ g e. ran ( mRSubst ` T ) ) -> ( ( x e. ( mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) o. ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) ) e. ran S )
58 coeq1 
 |-  ( F = ( x e. ( mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) -> ( F o. G ) = ( ( x e. ( mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) o. G ) )
59 coeq2 
 |-  ( G = ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) -> ( ( x e. ( mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) o. G ) = ( ( x e. ( mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) o. ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) ) )
60 58 59 sylan9eq 
 |-  ( ( F = ( x e. ( mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) /\ G = ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) ) -> ( F o. G ) = ( ( x e. ( mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) o. ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) ) )
61 60 eleq1d 
 |-  ( ( F = ( x e. ( mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) /\ G = ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) ) -> ( ( F o. G ) e. ran S <-> ( ( x e. ( mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) o. ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) ) e. ran S ) )
62 57 61 syl5ibrcom 
 |-  ( ( f e. ran ( mRSubst ` T ) /\ g e. ran ( mRSubst ` T ) ) -> ( ( F = ( x e. ( mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) /\ G = ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) ) -> ( F o. G ) e. ran S ) )
63 62 rexlimivv 
 |-  ( E. f e. ran ( mRSubst ` T ) E. g e. ran ( mRSubst ` T ) ( F = ( x e. ( mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) /\ G = ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) ) -> ( F o. G ) e. ran S )
64 17 63 sylbir 
 |-  ( ( E. f e. ran ( mRSubst ` T ) F = ( x e. ( mEx ` T ) |-> <. ( 1st ` x ) , ( f ` ( 2nd ` x ) ) >. ) /\ E. g e. ran ( mRSubst ` T ) G = ( y e. ( mEx ` T ) |-> <. ( 1st ` y ) , ( g ` ( 2nd ` y ) ) >. ) ) -> ( F o. G ) e. ran S )
65 10 16 64 syl2anb 
 |-  ( ( F e. ran S /\ G e. ran S ) -> ( F o. G ) e. ran S )