Step | Hyp | Ref
| Expression |
1 | | msubff1.v |
. . . 4
mVR   |
2 | | msubff1.r |
. . . 4
mREx   |
3 | | msubff1.s |
. . . 4
mSubst   |
4 | | msubff1.e |
. . . 4
mEx   |
5 | 1, 2, 3, 4 | msubff 30168 |
. . 3
 mFS   
   
   |
6 | | mapsspm 7505 |
. . . 4
  
  |
7 | 6 | a1i 11 |
. . 3
 mFS       |
8 | 5, 7 | fssresd 5750 |
. 2
 mFS  
            |
9 | | eqid 2451 |
. . . . . . . . . . . . 13
mRSubst  mRSubst   |
10 | 1, 2, 9 | mrsubff 30150 |
. . . . . . . . . . . 12
 mFS mRSubst            |
11 | 10 | ad2antrr 732 |
. . . . . . . . . . 11
   mFS                   mRSubst            |
12 | | simplrl 770 |
. . . . . . . . . . . 12
   mFS                       |
13 | 6, 12 | sseldi 3430 |
. . . . . . . . . . 11
   mFS                   
   |
14 | 11, 13 | ffvelrnd 6023 |
. . . . . . . . . 10
   mFS                    mRSubst         |
15 | | elmapi 7493 |
. . . . . . . . . 10
  mRSubst        mRSubst           |
16 | | ffn 5728 |
. . . . . . . . . 10
  mRSubst          mRSubst       |
17 | 14, 15, 16 | 3syl 18 |
. . . . . . . . 9
   mFS                    mRSubst       |
18 | | simplrr 771 |
. . . . . . . . . . . 12
   mFS                       |
19 | 6, 18 | sseldi 3430 |
. . . . . . . . . . 11
   mFS                   
   |
20 | 11, 19 | ffvelrnd 6023 |
. . . . . . . . . 10
   mFS                    mRSubst         |
21 | | elmapi 7493 |
. . . . . . . . . 10
  mRSubst        mRSubst           |
22 | | ffn 5728 |
. . . . . . . . . 10
  mRSubst          mRSubst       |
23 | 20, 21, 22 | 3syl 18 |
. . . . . . . . 9
   mFS                    mRSubst       |
24 | | simplrr 771 |
. . . . . . . . . . . . 13
    mFS                   
          |
25 | 24 | fveq1d 5867 |
. . . . . . . . . . . 12
    mFS                   
         mType                 mType          |
26 | 12 | adantr 467 |
. . . . . . . . . . . . . 14
    mFS                   

   |
27 | | elmapi 7493 |
. . . . . . . . . . . . . 14
         |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . 13
    mFS                   
      |
29 | | ssid 3451 |
. . . . . . . . . . . . . 14
 |
30 | 29 | a1i 11 |
. . . . . . . . . . . . 13
    mFS                   
  |
31 | | eqid 2451 |
. . . . . . . . . . . . . . . . . 18
mTC  mTC   |
32 | | eqid 2451 |
. . . . . . . . . . . . . . . . . 18
mType  mType   |
33 | 1, 31, 32 | mtyf2 30189 |
. . . . . . . . . . . . . . . . 17
 mFS mType      mTC    |
34 | 33 | ad3antrrr 736 |
. . . . . . . . . . . . . . . 16
    mFS                   
mType      mTC    |
35 | | simplrl 770 |
. . . . . . . . . . . . . . . 16
    mFS                   
  |
36 | 34, 35 | ffvelrnd 6023 |
. . . . . . . . . . . . . . 15
    mFS                   
 mType     mTC    |
37 | | opelxpi 4866 |
. . . . . . . . . . . . . . 15
   mType     mTC 

  mType        mTC     |
38 | 36, 37 | sylancom 673 |
. . . . . . . . . . . . . 14
    mFS                   
  mType        mTC     |
39 | 31, 4, 2 | mexval 30140 |
. . . . . . . . . . . . . 14
 mTC    |
40 | 38, 39 | syl6eleqr 2540 |
. . . . . . . . . . . . 13
    mFS                   
  mType         |
41 | 1, 2, 3, 4, 9 | msubval 30163 |
. . . . . . . . . . . . 13
        mType                 mType       
      mType           mRSubst            mType            |
42 | 28, 30, 40, 41 | syl3anc 1268 |
. . . . . . . . . . . 12
    mFS                   
         mType              mType           mRSubst            mType            |
43 | 18 | adantr 467 |
. . . . . . . . . . . . . 14
    mFS                   

   |
44 | | elmapi 7493 |
. . . . . . . . . . . . . 14
         |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . 13
    mFS                   
      |
46 | 1, 2, 3, 4, 9 | msubval 30163 |
. . . . . . . . . . . . 13
        mType                 mType       
      mType           mRSubst            mType            |
47 | 45, 30, 40, 46 | syl3anc 1268 |
. . . . . . . . . . . 12
    mFS                   
         mType              mType           mRSubst            mType            |
48 | 25, 42, 47 | 3eqtr3d 2493 |
. . . . . . . . . . 11
    mFS                   
      mType           mRSubst            mType                mType           mRSubst            mType            |
49 | | fvex 5875 |
. . . . . . . . . . . . 13
     mType         |
50 | | fvex 5875 |
. . . . . . . . . . . . 13
  mRSubst            mType          |
51 | 49, 50 | opth 4676 |
. . . . . . . . . . . 12
       mType           mRSubst            mType                mType           mRSubst            mType         
      mType             mType       
  mRSubst            mType           mRSubst            mType            |
52 | 51 | simprbi 466 |
. . . . . . . . . . 11
       mType           mRSubst            mType                mType           mRSubst            mType            mRSubst            mType           mRSubst            mType           |
53 | 48, 52 | syl 17 |
. . . . . . . . . 10
    mFS                   
  mRSubst            mType           mRSubst            mType           |
54 | | fvex 5875 |
. . . . . . . . . . . 12
 mType      |
55 | | vex 3048 |
. . . . . . . . . . . 12
 |
56 | 54, 55 | op2nd 6802 |
. . . . . . . . . . 11
     mType         |
57 | 56 | fveq2i 5868 |
. . . . . . . . . 10
  mRSubst            mType           mRSubst         |
58 | 56 | fveq2i 5868 |
. . . . . . . . . 10
  mRSubst            mType           mRSubst         |
59 | 53, 57, 58 | 3eqtr3g 2508 |
. . . . . . . . 9
    mFS                   
  mRSubst          mRSubst          |
60 | 17, 23, 59 | eqfnfvd 5979 |
. . . . . . . 8
   mFS                    mRSubst      mRSubst       |
61 | 1, 2, 9 | mrsubff1 30152 |
. . . . . . . . . . 11
 mFS  mRSubst               |
62 | | f1fveq 6163 |
. . . . . . . . . . 11
   mRSubst               
       mRSubst          mRSubst           |
63 | 61, 62 | sylan 474 |
. . . . . . . . . 10
  mFS   
       mRSubst          mRSubst           |
64 | | fvres 5879 |
. . . . . . . . . . . 12
     mRSubst         mRSubst       |
65 | | fvres 5879 |
. . . . . . . . . . . 12
     mRSubst         mRSubst       |
66 | 64, 65 | eqeqan12d 2467 |
. . . . . . . . . . 11
   
      mRSubst          mRSubst       
 mRSubst      mRSubst        |
67 | 66 | adantl 468 |
. . . . . . . . . 10
  mFS   
       mRSubst          mRSubst         mRSubst      mRSubst        |
68 | 63, 67 | bitr3d 259 |
. . . . . . . . 9
  mFS   
      mRSubst      mRSubst        |
69 | 68 | adantr 467 |
. . . . . . . 8
   mFS                     mRSubst      mRSubst        |
70 | 60, 69 | mpbird 236 |
. . . . . . 7
   mFS                     |
71 | 70 | fveq1d 5867 |
. . . . . 6
   mFS                             |
72 | 71 | expr 620 |
. . . . 5
   mFS                             |
73 | 72 | ralrimdva 2806 |
. . . 4
  mFS   
            

           |
74 | | fvres 5879 |
. . . . . 6
                 |
75 | | fvres 5879 |
. . . . . 6
                 |
76 | 74, 75 | eqeqan12d 2467 |
. . . . 5
   
             
     
           |
77 | 76 | adantl 468 |
. . . 4
  mFS   
      
             
           |
78 | | ffn 5728 |
. . . . . . 7
       |
79 | | ffn 5728 |
. . . . . . 7
       |
80 | | eqfnfv 5976 |
. . . . . . 7
 
  
           |
81 | 78, 79, 80 | syl2an 480 |
. . . . . 6
                        |
82 | 27, 44, 81 | syl2an 480 |
. . . . 5
   
    
           |
83 | 82 | adantl 468 |
. . . 4
  mFS   
                 |
84 | 73, 77, 83 | 3imtr4d 272 |
. . 3
  mFS   
      
                 |
85 | 84 | ralrimivva 2809 |
. 2
 mFS                   
         |
86 | | dff13 6159 |
. 2
 
          
             
         
                  |
87 | 8, 85, 86 | sylanbrc 670 |
1
 mFS  
            |