Step | Hyp | Ref
| Expression |
1 | | mclsval.d |
. . 3
mDV   |
2 | | mclsval.e |
. . 3
mEx   |
3 | | mclsval.c |
. . 3
mCls   |
4 | | mclsval.1 |
. . 3
 mFS |
5 | | mclsval.2 |
. . 3

  |
6 | | mclsval.3 |
. . 3

  |
7 | | mclsax.h |
. . 3
mVH   |
8 | | mclsax.a |
. . 3
mAx   |
9 | | mclsax.l |
. . 3
mSubst   |
10 | | mclsax.w |
. . 3
mVars   |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | mclsval 30273 |
. 2
                                                                            |
12 | | mclsind.4 |
. . . . . . 7

  |
13 | 6, 12 | ssind 3647 |
. . . . . 6

    |
14 | | mclsax.v |
. . . . . . . . . . 11
mVR   |
15 | 14, 2, 7 | mvhf 30268 |
. . . . . . . . . 10
 mFS       |
16 | 4, 15 | syl 17 |
. . . . . . . . 9
       |
17 | | ffn 5739 |
. . . . . . . . 9
    
  |
18 | 16, 17 | syl 17 |
. . . . . . . 8
   |
19 | 16 | ffvelrnda 6037 |
. . . . . . . . . 10
 
       |
20 | | mclsind.5 |
. . . . . . . . . 10
 
       |
21 | 19, 20 | elind 3609 |
. . . . . . . . 9
 
         |
22 | 21 | ralrimiva 2809 |
. . . . . . . 8
          |
23 | | ffnfv 6064 |
. . . . . . . 8
      


         |
24 | 18, 22, 23 | sylanbrc 677 |
. . . . . . 7
         |
25 | | frn 5747 |
. . . . . . 7
      
    |
26 | 24, 25 | syl 17 |
. . . . . 6
     |
27 | 13, 26 | unssd 3601 |
. . . . 5
  
    |
28 | | id 22 |
. . . . . . . . . . . 12
      
       
    |
29 | | inss2 3644 |
. . . . . . . . . . . 12
   |
30 | 28, 29 | syl6ss 3430 |
. . . . . . . . . . 11
      
       
  |
31 | 4 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
 
          
 
mFS |
32 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . . . 21
mREx  mREx   |
33 | 14, 32, 9, 2 | msubff 30240 |
. . . . . . . . . . . . . . . . . . . 20
 mFS    mREx         |
34 | | frn 5747 |
. . . . . . . . . . . . . . . . . . . 20
    mREx           |
35 | 31, 33, 34 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
 
          
 

   |
36 | | simpr2 1037 |
. . . . . . . . . . . . . . . . . . 19
 
          
 
  |
37 | 35, 36 | sseldd 3419 |
. . . . . . . . . . . . . . . . . 18
 
          
 

   |
38 | | elmapi 7511 |
. . . . . . . . . . . . . . . . . 18
         |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . . . . . 17
 
          
 
      |
40 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . . . . 22
mStat  mStat   |
41 | 8, 40 | maxsta 30264 |
. . . . . . . . . . . . . . . . . . . . 21
 mFS mStat    |
42 | 31, 41 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
 
          
 
mStat    |
43 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . . . 21
mPreSt  mPreSt   |
44 | 43, 40 | mstapst 30257 |
. . . . . . . . . . . . . . . . . . . 20
mStat  mPreSt   |
45 | 42, 44 | syl6ss 3430 |
. . . . . . . . . . . . . . . . . . 19
 
          
 
mPreSt    |
46 | | simpr1 1036 |
. . . . . . . . . . . . . . . . . . 19
 
          
 
      |
47 | 45, 46 | sseldd 3419 |
. . . . . . . . . . . . . . . . . 18
 
          
 
    mPreSt    |
48 | 1, 2, 43 | elmpst 30246 |
. . . . . . . . . . . . . . . . . . 19
    
mPreSt 
 


     |
49 | 48 | simp3bi 1047 |
. . . . . . . . . . . . . . . . . 18
    
mPreSt    |
50 | 47, 49 | syl 17 |
. . . . . . . . . . . . . . . . 17
 
          
 
  |
51 | 39, 50 | ffvelrnd 6038 |
. . . . . . . . . . . . . . . 16
 
          
 
      |
52 | 51 | 3adant3 1050 |
. . . . . . . . . . . . . . 15
 
          
                                          |
53 | | mclsind.6 |
. . . . . . . . . . . . . . 15
 
          
                                          |
54 | 52, 53 | elind 3609 |
. . . . . . . . . . . . . 14
 
          
                                            |
55 | 54 | 3exp 1230 |
. . . . . . . . . . . . 13
            
        
                         
           |
56 | 55 | 3expd 1250 |
. . . . . . . . . . . 12
                                                             |
57 | 56 | imp31 439 |
. . . . . . . . . . 11
       
                                                     |
58 | 30, 57 | syl5 32 |
. . . . . . . . . 10
       
         
                                             |
59 | 58 | impd 438 |
. . . . . . . . 9
       
        
                                              |
60 | 59 | ralrimiva 2809 |
. . . . . . . 8
 
                                                             |
61 | 60 | ex 441 |
. . . . . . 7
                        
                         
 
          |
62 | 61 | alrimiv 1781 |
. . . . . 6
       
                  
                         
 
          |
63 | 62 | alrimivv 1782 |
. . . . 5
                                                                     |
64 | | fvex 5889 |
. . . . . . . 8
mEx   |
65 | 2, 64 | eqeltri 2545 |
. . . . . . 7
 |
66 | 65 | inex1 4537 |
. . . . . 6
   |
67 | | sseq2 3440 |
. . . . . . 7
  
 

  
    |
68 | | sseq2 3440 |
. . . . . . . . . . . . 13
  
      
           |
69 | 68 | anbi1d 719 |
. . . . . . . . . . . 12
  
                                                                                          |
70 | | eleq2 2538 |
. . . . . . . . . . . 12
  
    
         |
71 | 69, 70 | imbi12d 327 |
. . . . . . . . . . 11
  
                                                        
                                               |
72 | 71 | ralbidv 2829 |
. . . . . . . . . 10
  
 
                                                                   
                         
 
          |
73 | 72 | imbi2d 323 |
. . . . . . . . 9
  
     
                                                                                                                  |
74 | 73 | albidv 1775 |
. . . . . . . 8
  
                                                          
                         
                         
 
           |
75 | 74 | 2albidv 1777 |
. . . . . . 7
  
                                                                                                                                    |
76 | 67, 75 | anbi12d 725 |
. . . . . 6
  
   
                                                              
 
             
                  
                         
 
            |
77 | 66, 76 | elab 3173 |
. . . . 5
                                                                                                                                                 |
78 | 27, 63, 77 | sylanbrc 677 |
. . . 4
                                                                         |
79 | | intss1 4241 |
. . . 4
                                                                                                                                                |
80 | 78, 79 | syl 17 |
. . 3
                                                                          |
81 | 80, 29 | syl6ss 3430 |
. 2
                                                                        |
82 | 11, 81 | eqsstrd 3452 |
1
    
  |