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