Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . 5
mEx mEx |
2 | | eqid 2622 |
. . . . 5
mRSubst mRSubst |
3 | | msubco.s |
. . . . 5
mSubst |
4 | 1, 2, 3 | elmsubrn 31425 |
. . . 4
mRSubst mEx |
5 | 4 | eleq2i 2693 |
. . 3
mRSubst mEx |
6 | | eqid 2622 |
. . . 4
mRSubst mEx mRSubst mEx |
7 | | fvex 6201 |
. . . . 5
mEx |
8 | 7 | mptex 6486 |
. . . 4
mEx |
9 | 6, 8 | elrnmpti 5376 |
. . 3
mRSubst mEx mRSubst mEx |
10 | 5, 9 | bitri 264 |
. 2
mRSubst mEx |
11 | 1, 2, 3 | elmsubrn 31425 |
. . . 4
mRSubst mEx |
12 | 11 | eleq2i 2693 |
. . 3
mRSubst mEx |
13 | | eqid 2622 |
. . . 4
mRSubst mEx mRSubst mEx |
14 | 7 | mptex 6486 |
. . . 4
mEx |
15 | 13, 14 | elrnmpti 5376 |
. . 3
mRSubst mEx mRSubst mEx |
16 | 12, 15 | bitri 264 |
. 2
mRSubst mEx |
17 | | reeanv 3107 |
. . 3
mRSubst mRSubst mEx
mEx
mRSubst mEx
mRSubst mEx |
18 | | simpr 477 |
. . . . . . . . . . . 12
mRSubst
mRSubst mEx
mEx |
19 | | eqid 2622 |
. . . . . . . . . . . . 13
mTC mTC |
20 | | eqid 2622 |
. . . . . . . . . . . . 13
mREx mREx |
21 | 19, 1, 20 | mexval 31399 |
. . . . . . . . . . . 12
mEx mTC mREx |
22 | 18, 21 | syl6eleq 2711 |
. . . . . . . . . . 11
mRSubst
mRSubst mEx
mTC mREx |
23 | | xp1st 7198 |
. . . . . . . . . . 11
mTC mREx mTC |
24 | 22, 23 | syl 17 |
. . . . . . . . . 10
mRSubst
mRSubst mEx
mTC |
25 | 2, 20 | mrsubf 31414 |
. . . . . . . . . . . 12
mRSubst
mRExmREx |
26 | 25 | ad2antlr 763 |
. . . . . . . . . . 11
mRSubst
mRSubst mEx
mRExmREx |
27 | | xp2nd 7199 |
. . . . . . . . . . . 12
mTC mREx mREx |
28 | 22, 27 | syl 17 |
. . . . . . . . . . 11
mRSubst
mRSubst mEx
mREx |
29 | 26, 28 | ffvelrnd 6360 |
. . . . . . . . . 10
mRSubst
mRSubst mEx
mREx |
30 | | opelxpi 5148 |
. . . . . . . . . 10
mTC mREx
mTC mREx |
31 | 24, 29, 30 | syl2anc 693 |
. . . . . . . . 9
mRSubst
mRSubst mEx
mTC mREx |
32 | 31, 21 | syl6eleqr 2712 |
. . . . . . . 8
mRSubst
mRSubst mEx
mEx |
33 | | eqidd 2623 |
. . . . . . . 8
mRSubst mRSubst mEx
mEx |
34 | | eqidd 2623 |
. . . . . . . 8
mRSubst mRSubst mEx
mEx |
35 | | fvex 6201 |
. . . . . . . . . 10
|
36 | | fvex 6201 |
. . . . . . . . . 10
|
37 | 35, 36 | op1std 7178 |
. . . . . . . . 9
|
38 | 35, 36 | op2ndd 7179 |
. . . . . . . . . 10
|
39 | 38 | fveq2d 6195 |
. . . . . . . . 9
|
40 | 37, 39 | opeq12d 4410 |
. . . . . . . 8
|
41 | 32, 33, 34, 40 | fmptco 6396 |
. . . . . . 7
mRSubst mRSubst mEx mEx mEx |
42 | | fvco3 6275 |
. . . . . . . . . 10
mRExmREx mREx
|
43 | 26, 28, 42 | syl2anc 693 |
. . . . . . . . 9
mRSubst
mRSubst mEx
|
44 | 43 | opeq2d 4409 |
. . . . . . . 8
mRSubst
mRSubst mEx
|
45 | 44 | mpteq2dva 4744 |
. . . . . . 7
mRSubst mRSubst mEx
mEx |
46 | 41, 45 | eqtr4d 2659 |
. . . . . 6
mRSubst mRSubst mEx mEx mEx |
47 | 2 | mrsubco 31418 |
. . . . . . . 8
mRSubst mRSubst mRSubst |
48 | 7 | mptex 6486 |
. . . . . . . 8
mEx |
49 | | eqid 2622 |
. . . . . . . . 9
mRSubst mEx mRSubst mEx |
50 | | fveq1 6190 |
. . . . . . . . . . 11
|
51 | 50 | opeq2d 4409 |
. . . . . . . . . 10
|
52 | 51 | mpteq2dv 4745 |
. . . . . . . . 9
mEx
mEx |
53 | 49, 52 | elrnmpt1s 5373 |
. . . . . . . 8
mRSubst mEx
mEx mRSubst mEx |
54 | 47, 48, 53 | sylancl 694 |
. . . . . . 7
mRSubst mRSubst mEx
mRSubst mEx |
55 | 1, 2, 3 | elmsubrn 31425 |
. . . . . . 7
mRSubst mEx |
56 | 54, 55 | syl6eleqr 2712 |
. . . . . 6
mRSubst mRSubst mEx
|
57 | 46, 56 | eqeltrd 2701 |
. . . . 5
mRSubst mRSubst mEx mEx |
58 | | coeq1 5279 |
. . . . . . 7
mEx mEx
|
59 | | coeq2 5280 |
. . . . . . 7
mEx mEx mEx mEx |
60 | 58, 59 | sylan9eq 2676 |
. . . . . 6
mEx
mEx
mEx mEx |
61 | 60 | eleq1d 2686 |
. . . . 5
mEx
mEx mEx mEx |
62 | 57, 61 | syl5ibrcom 237 |
. . . 4
mRSubst mRSubst mEx
mEx
|
63 | 62 | rexlimivv 3036 |
. . 3
mRSubst mRSubst mEx
mEx
|
64 | 17, 63 | sylbir 225 |
. 2
mRSubst mEx mRSubst mEx
|
65 | 10, 16, 64 | syl2anb 496 |
1
|