Step | Hyp | Ref
| Expression |
1 | | eqid 2461 |
. . . . 5
mEx  mEx   |
2 | | eqid 2461 |
. . . . 5
mRSubst  mRSubst   |
3 | | msubco.s |
. . . . 5
mSubst   |
4 | 1, 2, 3 | elmsubrn 30214 |
. . . 4
 mRSubst   mEx                    |
5 | 4 | eleq2i 2531 |
. . 3

 mRSubst   mEx                     |
6 | | eqid 2461 |
. . . 4
 mRSubst   mEx                    mRSubst   mEx                    |
7 | | fvex 5897 |
. . . . 5
mEx   |
8 | 7 | mptex 6160 |
. . . 4
 mEx                   |
9 | 6, 8 | elrnmpti 5103 |
. . 3
  mRSubst   mEx                    mRSubst    mEx                    |
10 | 5, 9 | bitri 257 |
. 2

 mRSubst    mEx                    |
11 | 1, 2, 3 | elmsubrn 30214 |
. . . 4
 mRSubst   mEx                    |
12 | 11 | eleq2i 2531 |
. . 3

 mRSubst   mEx                     |
13 | | eqid 2461 |
. . . 4
 mRSubst   mEx                    mRSubst   mEx                    |
14 | 7 | mptex 6160 |
. . . 4
 mEx                   |
15 | 13, 14 | elrnmpti 5103 |
. . 3
  mRSubst   mEx                    mRSubst    mEx                    |
16 | 12, 15 | bitri 257 |
. 2

 mRSubst    mEx                    |
17 | | reeanv 2969 |
. . 3
  mRSubst    mRSubst     mEx                 
 mEx                  
 
mRSubst    mEx                 
 mRSubst    mEx                     |
18 | | simpr 467 |
. . . . . . . . . . . 12
   mRSubst 
mRSubst   mEx  
mEx    |
19 | | eqid 2461 |
. . . . . . . . . . . . 13
mTC  mTC   |
20 | | eqid 2461 |
. . . . . . . . . . . . 13
mREx  mREx   |
21 | 19, 1, 20 | mexval 30188 |
. . . . . . . . . . . 12
mEx   mTC  mREx    |
22 | 18, 21 | syl6eleq 2549 |
. . . . . . . . . . 11
   mRSubst 
mRSubst   mEx  
 mTC  mREx     |
23 | | xp1st 6849 |
. . . . . . . . . . 11
  mTC  mREx       mTC    |
24 | 22, 23 | syl 17 |
. . . . . . . . . 10
   mRSubst 
mRSubst   mEx  
    mTC    |
25 | 2, 20 | mrsubf 30203 |
. . . . . . . . . . . 12
 mRSubst 
  mREx    mREx    |
26 | 25 | ad2antlr 738 |
. . . . . . . . . . 11
   mRSubst 
mRSubst   mEx  
  mREx    mREx    |
27 | | xp2nd 6850 |
. . . . . . . . . . . 12
  mTC  mREx       mREx    |
28 | 22, 27 | syl 17 |
. . . . . . . . . . 11
   mRSubst 
mRSubst   mEx  
    mREx    |
29 | 26, 28 | ffvelrnd 6045 |
. . . . . . . . . 10
   mRSubst 
mRSubst   mEx  
        mREx    |
30 | | opelxpi 4884 |
. . . . . . . . . 10
      mTC          mREx  
                mTC  mREx     |
31 | 24, 29, 30 | syl2anc 671 |
. . . . . . . . 9
   mRSubst 
mRSubst   mEx  
                mTC  mREx     |
32 | 31, 21 | syl6eleqr 2550 |
. . . . . . . 8
   mRSubst 
mRSubst   mEx  
               mEx    |
33 | | eqidd 2462 |
. . . . . . . 8
  mRSubst  mRSubst    mEx                 
 mEx                    |
34 | | eqidd 2462 |
. . . . . . . 8
  mRSubst  mRSubst    mEx                 
 mEx                    |
35 | | fvex 5897 |
. . . . . . . . . 10
     |
36 | | fvex 5897 |
. . . . . . . . . 10
         |
37 | 35, 36 | op1std 6829 |
. . . . . . . . 9
                          |
38 | 35, 36 | op2ndd 6830 |
. . . . . . . . . 10
                              |
39 | 38 | fveq2d 5891 |
. . . . . . . . 9
                                      |
40 | 37, 39 | opeq12d 4187 |
. . . . . . . 8
                              
                     |
41 | 32, 33, 34, 40 | fmptco 6079 |
. . . . . . 7
  mRSubst  mRSubst     mEx                   mEx                    mEx                        |
42 | | fvco3 5964 |
. . . . . . . . . 10
    mREx    mREx      mREx  
                        |
43 | 26, 28, 42 | syl2anc 671 |
. . . . . . . . 9
   mRSubst 
mRSubst   mEx  
                        |
44 | 43 | opeq2d 4186 |
. . . . . . . 8
   mRSubst 
mRSubst   mEx  
                                      |
45 | 44 | mpteq2dva 4502 |
. . . . . . 7
  mRSubst  mRSubst    mEx                   
 mEx                        |
46 | 41, 45 | eqtr4d 2498 |
. . . . . 6
  mRSubst  mRSubst     mEx                   mEx                    mEx                      |
47 | 2 | mrsubco 30207 |
. . . . . . . 8
  mRSubst  mRSubst     mRSubst    |
48 | 7 | mptex 6160 |
. . . . . . . 8
 mEx                     |
49 | | eqid 2461 |
. . . . . . . . 9
 mRSubst   mEx                    mRSubst   mEx                    |
50 | | fveq1 5886 |
. . . . . . . . . . 11
                       |
51 | 50 | opeq2d 4186 |
. . . . . . . . . 10
                 
                   |
52 | 51 | mpteq2dv 4503 |
. . . . . . . . 9
    mEx                 
 mEx                      |
53 | 49, 52 | elrnmpt1s 5100 |
. . . . . . . 8
    mRSubst   mEx                   
  mEx                     mRSubst   mEx                     |
54 | 47, 48, 53 | sylancl 673 |
. . . . . . 7
  mRSubst  mRSubst    mEx                   

mRSubst   mEx                     |
55 | 1, 2, 3 | elmsubrn 30214 |
. . . . . . 7
 mRSubst   mEx                    |
56 | 54, 55 | syl6eleqr 2550 |
. . . . . 6
  mRSubst  mRSubst    mEx                   
  |
57 | 46, 56 | eqeltrd 2539 |
. . . . 5
  mRSubst  mRSubst     mEx                   mEx                     |
58 | | coeq1 5010 |
. . . . . . 7
  mEx                      mEx                 
   |
59 | | coeq2 5011 |
. . . . . . 7
  mEx                    mEx                     mEx                   mEx                     |
60 | 58, 59 | sylan9eq 2515 |
. . . . . 6
   mEx                 
 mEx                   
   mEx                   mEx                     |
61 | 60 | eleq1d 2523 |
. . . . 5
   mEx                 
 mEx                        mEx                   mEx                      |
62 | 57, 61 | syl5ibrcom 230 |
. . . 4
  mRSubst  mRSubst      mEx                 
 mEx                  
     |
63 | 62 | rexlimivv 2895 |
. . 3
  mRSubst    mRSubst     mEx                 
 mEx                   
   |
64 | 17, 63 | sylbir 218 |
. 2
   mRSubst    mEx                   mRSubst    mEx                  
    |
65 | 10, 16, 64 | syl2anb 486 |
1
 

    |