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