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