Step | Hyp | Ref
| Expression |
1 | | mclsval.c |
. . 3
mCls   |
2 | | mclsval.1 |
. . . 4
 mFS |
3 | | elex 3212 |
. . . 4
 mFS   |
4 | | fveq2 6191 |
. . . . . . . 8
 mDV  mDV    |
5 | | mclsval.d |
. . . . . . . 8
mDV   |
6 | 4, 5 | syl6eqr 2674 |
. . . . . . 7
 mDV    |
7 | 6 | pweqd 4163 |
. . . . . 6
  mDV     |
8 | | fveq2 6191 |
. . . . . . . 8
 mEx  mEx    |
9 | | mclsval.e |
. . . . . . . 8
mEx   |
10 | 8, 9 | syl6eqr 2674 |
. . . . . . 7
 mEx    |
11 | 10 | pweqd 4163 |
. . . . . 6
  mEx     |
12 | | fveq2 6191 |
. . . . . . . . . . . . 13
 mVH  mVH    |
13 | | mclsval.h |
. . . . . . . . . . . . 13
mVH   |
14 | 12, 13 | syl6eqr 2674 |
. . . . . . . . . . . 12
 mVH    |
15 | 14 | rneqd 5353 |
. . . . . . . . . . 11
 mVH    |
16 | 15 | uneq2d 3767 |
. . . . . . . . . 10
  mVH       |
17 | 16 | sseq1d 3632 |
. . . . . . . . 9
   mVH  
     |
18 | | fveq2 6191 |
. . . . . . . . . . . . . 14
 mAx  mAx    |
19 | | mclsval.a |
. . . . . . . . . . . . . 14
mAx   |
20 | 18, 19 | syl6eqr 2674 |
. . . . . . . . . . . . 13
 mAx    |
21 | 20 | eleq2d 2687 |
. . . . . . . . . . . 12
     
mAx 
       |
22 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
 mSubst  mSubst    |
23 | | mclsval.s |
. . . . . . . . . . . . . . 15
mSubst   |
24 | 22, 23 | syl6eqr 2674 |
. . . . . . . . . . . . . 14
 mSubst    |
25 | 24 | rneqd 5353 |
. . . . . . . . . . . . 13
 mSubst    |
26 | 15 | uneq2d 3767 |
. . . . . . . . . . . . . . . . 17
  mVH       |
27 | 26 | imaeq2d 5466 |
. . . . . . . . . . . . . . . 16
     mVH            |
28 | 27 | sseq1d 3632 |
. . . . . . . . . . . . . . 15
      mVH   
         |
29 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
 mVars  mVars    |
30 | | mclsval.v |
. . . . . . . . . . . . . . . . . . . . 21
mVars   |
31 | 29, 30 | syl6eqr 2674 |
. . . . . . . . . . . . . . . . . . . 20
 mVars    |
32 | 14 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . 21
  mVH           |
33 | 32 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
     mVH                |
34 | 31, 33 | fveq12d 6197 |
. . . . . . . . . . . . . . . . . . 19
  mVars        mVH                     |
35 | 14 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . 21
  mVH           |
36 | 35 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
     mVH                |
37 | 31, 36 | fveq12d 6197 |
. . . . . . . . . . . . . . . . . . 19
  mVars        mVH                     |
38 | 34, 37 | xpeq12d 5140 |
. . . . . . . . . . . . . . . . . 18
   mVars        mVH        mVars        mVH                                    |
39 | 38 | sseq1d 3632 |
. . . . . . . . . . . . . . . . 17
    mVars        mVH        mVars        mVH                                     |
40 | 39 | imbi2d 330 |
. . . . . . . . . . . . . . . 16
       mVars        mVH        mVars        mVH        
                                 |
41 | 40 | 2albidv 1851 |
. . . . . . . . . . . . . . 15
           mVars        mVH        mVars        mVH        
      
                         
    |
42 | 28, 41 | anbi12d 747 |
. . . . . . . . . . . . . 14
       mVH   
         mVars        mVH        mVars        mVH         
      
                                      |
43 | 42 | imbi1d 331 |
. . . . . . . . . . . . 13
        mVH             mVars        mVH        mVars        mVH                                                                  |
44 | 25, 43 | raleqbidv 3152 |
. . . . . . . . . . . 12
  
mSubst         mVH   
         mVars        mVH        mVars        mVH               
                                                    |
45 | 21, 44 | imbi12d 334 |
. . . . . . . . . . 11
       mAx  
mSubst         mVH   
         mVars        mVH        mVars        mVH                                                                           |
46 | 45 | albidv 1849 |
. . . . . . . . . 10
         mAx 
 mSubst         mVH             mVars        mVH        mVars        mVH       
 
     
                                                             |
47 | 46 | 2albidv 1851 |
. . . . . . . . 9
             mAx 
 mSubst         mVH             mVars        mVH        mVars        mVH       
 
     
          
                                                      |
48 | 17, 47 | anbi12d 747 |
. . . . . . . 8
    mVH  
           mAx 
 mSubst         mVH             mVars        mVH        mVars        mVH       
 
      
  
                                                                  |
49 | 48 | abbidv 2741 |
. . . . . . 7
    mVH             
mAx   mSubst         mVH             mVars        mVH        mVars        mVH       
 
                      
                                                       |
50 | 49 | inteqd 4480 |
. . . . . 6
     mVH             
mAx   mSubst         mVH             mVars        mVH        mVars        mVH       
 
                                                                               |
51 | 7, 11, 50 | mpt2eq123dv 6717 |
. . . . 5
   mDV    mEx      mVH  
           mAx 
 mSubst         mVH             mVars        mVH        mVars        mVH       
 
           
     
                                                                   |
52 | | df-mcls 31394 |
. . . . 5
mCls    mDV    mEx      mVH  
           mAx 
 mSubst         mVH             mVars        mVH        mVars        mVH       
 
           |
53 | | fvex 6201 |
. . . . . . . 8
mDV   |
54 | 5, 53 | eqeltri 2697 |
. . . . . . 7
 |
55 | 54 | pwex 4848 |
. . . . . 6
  |
56 | | fvex 6201 |
. . . . . . . 8
mEx   |
57 | 9, 56 | eqeltri 2697 |
. . . . . . 7
 |
58 | 57 | pwex 4848 |
. . . . . 6
  |
59 | 55, 58 | mpt2ex 7247 |
. . . . 5
  
     
                                                                  |
60 | 51, 52, 59 | fvmpt 6282 |
. . . 4
 mCls    
                
                                                        |
61 | 2, 3, 60 | 3syl 18 |
. . 3
 mCls                                                                              |
62 | 1, 61 | syl5eq 2668 |
. 2
   
     
                                                                   |
63 | | simprr 796 |
. . . . . . 7
 

 
  |
64 | 63 | uneq1d 3766 |
. . . . . 6
 

        |
65 | 64 | sseq1d 3632 |
. . . . 5
 

      
   |
66 | | simprl 794 |
. . . . . . . . . . . . . 14
 

    |
67 | 66 | sseq2d 3633 |
. . . . . . . . . . . . 13
 

                            
                         
   |
68 | 67 | imbi2d 330 |
. . . . . . . . . . . 12
 

     
                         
                                  |
69 | 68 | 2albidv 1851 |
. . . . . . . . . . 11
 

         
                         
                                      |
70 | 69 | anbi2d 740 |
. . . . . . . . . 10
 

                                            
      
                                      |
71 | 70 | imbi1d 331 |
. . . . . . . . 9
 

          
                                               
                                           |
72 | 71 | ralbidv 2986 |
. . . . . . . 8
 

                                                                                                          |
73 | 72 | imbi2d 330 |
. . . . . . 7
 

                                                          
                                                           |
74 | 73 | albidv 1849 |
. . . . . 6
 

         
                                                         
                                                      |
75 | 74 | 2albidv 1851 |
. . . . 5
 

             
                                                                                                                    |
76 | 65, 75 | anbi12d 747 |
. . . 4
 

                                                                    
 
                                                                   |
77 | 76 | abbidv 2741 |
. . 3
 

     
                                                                                                                                      |
78 | 77 | inteqd 4480 |
. 2
 

      
                                                                                                                                       |
79 | | mclsval.2 |
. . 3

  |
80 | 54 | elpw2 4828 |
. . 3
 
  |
81 | 79, 80 | sylibr 224 |
. 2
    |
82 | | mclsval.3 |
. . 3

  |
83 | 57 | elpw2 4828 |
. . 3
 
  |
84 | 82, 83 | sylibr 224 |
. 2
    |
85 | 5, 9, 1, 2, 79, 82, 13, 19, 23, 30 | mclsssvlem 31459 |
. . 3
                                                                        |
86 | 57 | ssex 4802 |
. . 3
     
                                                                                                                                       |
87 | 85, 86 | syl 17 |
. 2
                                                                        |
88 | 62, 78, 81, 84, 87 | ovmpt2d 6788 |
1
                                                                            |