Step | Hyp | Ref
| Expression |
1 | | mclsppslem.10 |
. . . 4
   |
2 | | mclspps.l |
. . . . 5
mSubst   |
3 | | mclspps.e |
. . . . 5
mEx   |
4 | 2, 3 | msubf 30242 |
. . . 4
       |
5 | 1, 4 | syl 17 |
. . 3
       |
6 | | mclspps.1 |
. . . . . . . 8
 mFS |
7 | | eqid 2471 |
. . . . . . . . 9
mAx  mAx   |
8 | | eqid 2471 |
. . . . . . . . 9
mStat  mStat   |
9 | 7, 8 | maxsta 30264 |
. . . . . . . 8
 mFS mAx 
mStat    |
10 | 6, 9 | syl 17 |
. . . . . . 7
 mAx  mStat    |
11 | | eqid 2471 |
. . . . . . . 8
mPreSt  mPreSt   |
12 | 11, 8 | mstapst 30257 |
. . . . . . 7
mStat  mPreSt   |
13 | 10, 12 | syl6ss 3430 |
. . . . . 6
 mAx  mPreSt    |
14 | | mclsppslem.9 |
. . . . . 6
    
mAx    |
15 | 13, 14 | sseldd 3419 |
. . . . 5
    
mPreSt    |
16 | | mclspps.d |
. . . . . 6
mDV   |
17 | 16, 3, 11 | elmpst 30246 |
. . . . 5
    
mPreSt 
 


     |
18 | 15, 17 | sylib 201 |
. . . 4
     

   |
19 | 18 | simp3d 1044 |
. . 3
   |
20 | 5, 19 | ffvelrnd 6038 |
. 2
       |
21 | | fvco3 5957 |
. . . 4
     
                 |
22 | 5, 19, 21 | syl2anc 673 |
. . 3
                 |
23 | | mclspps.c |
. . . 4
mCls   |
24 | | mclspps.2 |
. . . 4

  |
25 | | mclspps.3 |
. . . 4

  |
26 | | mclspps.v |
. . . 4
mVR   |
27 | | mclspps.h |
. . . 4
mVH   |
28 | | mclspps.w |
. . . 4
mVars   |
29 | | mclspps.5 |
. . . . 5
   |
30 | 2 | msubco 30241 |
. . . . 5
 

    |
31 | 29, 1, 30 | syl2anc 673 |
. . . 4
     |
32 | 2, 3 | msubf 30242 |
. . . . . . . . 9
       |
33 | 29, 32 | syl 17 |
. . . . . . . 8
       |
34 | | fco 5751 |
. . . . . . . 8
                   |
35 | 33, 5, 34 | syl2anc 673 |
. . . . . . 7
         |
36 | | ffn 5739 |
. . . . . . 7
           |
37 | 35, 36 | syl 17 |
. . . . . 6
     |
38 | 37 | adantr 472 |
. . . . 5
 
 
   |
39 | | mclsppslem.11 |
. . . . . . . . 9
                  |
40 | | ffun 5742 |
. . . . . . . . . . 11
       |
41 | 5, 40 | syl 17 |
. . . . . . . . . 10
   |
42 | 17 | simp2bi 1046 |
. . . . . . . . . . . . . 14
    
mPreSt  
   |
43 | 15, 42 | syl 17 |
. . . . . . . . . . . . 13
 
   |
44 | 43 | simpld 466 |
. . . . . . . . . . . 12

  |
45 | 26, 3, 27 | mvhf 30268 |
. . . . . . . . . . . . 13
 mFS       |
46 | | frn 5747 |
. . . . . . . . . . . . 13
    
  |
47 | 6, 45, 46 | 3syl 18 |
. . . . . . . . . . . 12
   |
48 | 44, 47 | unssd 3601 |
. . . . . . . . . . 11
  
  |
49 | | fdm 5745 |
. . . . . . . . . . . 12
    
  |
50 | 5, 49 | syl 17 |
. . . . . . . . . . 11
   |
51 | 48, 50 | sseqtr4d 3455 |
. . . . . . . . . 10
  
  |
52 | | funimass3 6013 |
. . . . . . . . . 10
   
                
                   |
53 | 41, 51, 52 | syl2anc 673 |
. . . . . . . . 9
                  
                 |
54 | 39, 53 | mpbid 215 |
. . . . . . . 8
  
                |
55 | | cnvco 5025 |
. . . . . . . . . 10
        |
56 | 55 | imaeq1i 5171 |
. . . . . . . . 9
                        |
57 | | imaco 5347 |
. . . . . . . . 9
  
                        |
58 | 56, 57 | eqtri 2493 |
. . . . . . . 8
                          |
59 | 54, 58 | syl6sseqr 3465 |
. . . . . . 7
  
  
          |
60 | 59 | unssad 3602 |
. . . . . 6

  
          |
61 | 60 | sselda 3418 |
. . . . 5
 
              |
62 | | elpreima 6017 |
. . . . . 6
                              |
63 | 62 | simplbda 636 |
. . . . 5
   
  
        
 
          |
64 | 38, 61, 63 | syl2anc 673 |
. . . 4
 
             |
65 | 37 | adantr 472 |
. . . . 5
 
 
   |
66 | 59 | unssbd 3603 |
. . . . . . 7
              |
67 | 66 | adantr 472 |
. . . . . 6
 
              |
68 | | ffn 5739 |
. . . . . . . 8
    
  |
69 | 6, 45, 68 | 3syl 18 |
. . . . . . 7
   |
70 | | fnfvelrn 6034 |
. . . . . . 7
 
       |
71 | 69, 70 | sylan 479 |
. . . . . 6
 
       |
72 | 67, 71 | sseldd 3419 |
. . . . 5
 
                  |
73 | | elpreima 6017 |
. . . . . 6
                                          |
74 | 73 | simplbda 636 |
. . . . 5
                                    |
75 | 65, 72, 74 | syl2anc 673 |
. . . 4
 
                 |
76 | 5 | adantr 472 |
. . . . . . . . . . . . 13
 
         |
77 | 6, 45 | syl 17 |
. . . . . . . . . . . . . . 15
       |
78 | 77 | adantr 472 |
. . . . . . . . . . . . . 14
 
         |
79 | 18 | simp1d 1042 |
. . . . . . . . . . . . . . . . . . . 20
  
   |
80 | 79 | simpld 466 |
. . . . . . . . . . . . . . . . . . 19

  |
81 | 26, 16 | mdvval 30214 |
. . . . . . . . . . . . . . . . . . . 20
    |
82 | | difss 3549 |
. . . . . . . . . . . . . . . . . . . 20
   
  |
83 | 81, 82 | eqsstri 3448 |
. . . . . . . . . . . . . . . . . . 19

  |
84 | 80, 83 | syl6ss 3430 |
. . . . . . . . . . . . . . . . . 18

    |
85 | 84 | ssbrd 4437 |
. . . . . . . . . . . . . . . . 17
           |
86 | 85 | imp 436 |
. . . . . . . . . . . . . . . 16
 
         |
87 | | brxp 4870 |
. . . . . . . . . . . . . . . 16
    

   |
88 | 86, 87 | sylib 201 |
. . . . . . . . . . . . . . 15
 
   
   |
89 | 88 | simpld 466 |
. . . . . . . . . . . . . 14
 
     |
90 | 78, 89 | ffvelrnd 6038 |
. . . . . . . . . . . . 13
 
         |
91 | | fvco3 5957 |
. . . . . . . . . . . . 13
                                   |
92 | 76, 90, 91 | syl2anc 673 |
. . . . . . . . . . . 12
 
                           |
93 | 92 | fveq2d 5883 |
. . . . . . . . . . 11
 
       
                           |
94 | 6 | adantr 472 |
. . . . . . . . . . . 12
 
   mFS |
95 | 29 | adantr 472 |
. . . . . . . . . . . 12
 
     |
96 | 76, 90 | ffvelrnd 6038 |
. . . . . . . . . . . 12
 
             |
97 | 2, 3, 28, 27 | msubvrs 30270 |
. . . . . . . . . . . 12
  mFS                                                      |
98 | 94, 95, 96, 97 | syl3anc 1292 |
. . . . . . . . . . 11
 
                                               |
99 | 93, 98 | eqtrd 2505 |
. . . . . . . . . 10
 
       
                                     |
100 | 99 | eleq2d 2534 |
. . . . . . . . 9
 
                 
                             |
101 | | eliun 4274 |
. . . . . . . . 9
                           
                           |
102 | 100, 101 | syl6bb 269 |
. . . . . . . 8
 
                 
                             |
103 | 88 | simprd 470 |
. . . . . . . . . . . . . 14
 
     |
104 | 78, 103 | ffvelrnd 6038 |
. . . . . . . . . . . . 13
 
         |
105 | | fvco3 5957 |
. . . . . . . . . . . . 13
                                   |
106 | 76, 104, 105 | syl2anc 673 |
. . . . . . . . . . . 12
 
                           |
107 | 106 | fveq2d 5883 |
. . . . . . . . . . 11
 
       
                           |
108 | 76, 104 | ffvelrnd 6038 |
. . . . . . . . . . . 12
 
             |
109 | 2, 3, 28, 27 | msubvrs 30270 |
. . . . . . . . . . . 12
  mFS                                                      |
110 | 94, 95, 108, 109 | syl3anc 1292 |
. . . . . . . . . . 11
 
                                               |
111 | 107, 110 | eqtrd 2505 |
. . . . . . . . . 10
 
       
                                     |
112 | 111 | eleq2d 2534 |
. . . . . . . . 9
 
                 
                             |
113 | | eliun 4274 |
. . . . . . . . 9
                           
                           |
114 | 112, 113 | syl6bb 269 |
. . . . . . . 8
 
                 
                             |
115 | 102, 114 | anbi12d 725 |
. . . . . . 7
 
                                                             
                             |
116 | | reeanv 2944 |
. . . . . . . 8
                                                                                  
                            |
117 | | simpll 768 |
. . . . . . . . . 10
      
           
                |
118 | | brxp 4870 |
. . . . . . . . . . . 12
                                                         |
119 | | mclsppslem.12 |
. . . . . . . . . . . . . . 15
                                     |
120 | | vex 3034 |
. . . . . . . . . . . . . . . 16
 |
121 | | vex 3034 |
. . . . . . . . . . . . . . . 16
 |
122 | | breq12 4400 |
. . . . . . . . . . . . . . . . . 18
 
         |
123 | | simpl 464 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
124 | 123 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . . 22
 
           |
125 | 124 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . 21
 
                   |
126 | 125 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . 20
 
                           |
127 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
128 | 127 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . . 22
 
           |
129 | 128 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . 21
 
                   |
130 | 129 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . 20
 
                           |
131 | 126, 130 | xpeq12d 4864 |
. . . . . . . . . . . . . . . . . . 19
 
                                                       |
132 | 131 | sseq1d 3445 |
. . . . . . . . . . . . . . . . . 18
 
                           
                         
   |
133 | 122, 132 | imbi12d 327 |
. . . . . . . . . . . . . . . . 17
 
    
                         
                                  |
134 | 133 | spc2gv 3123 |
. . . . . . . . . . . . . . . 16
 
        
                         
                                  |
135 | 120, 121,
134 | mp2an 686 |
. . . . . . . . . . . . . . 15
                                                                   |
136 | 119, 135 | syl 17 |
. . . . . . . . . . . . . 14
                                 |
137 | 136 | imp 436 |
. . . . . . . . . . . . 13
 
                               |
138 | 137 | ssbrd 4437 |
. . . . . . . . . . . 12
 
                               
     |
139 | 118, 138 | syl5bir 226 |
. . . . . . . . . . 11
 
                             
     |
140 | 139 | imp 436 |
. . . . . . . . . 10
      
           
                  |
141 | | vex 3034 |
. . . . . . . . . . . . 13
 |
142 | | vex 3034 |
. . . . . . . . . . . . 13
 |
143 | | breq12 4400 |
. . . . . . . . . . . . . . . 16
 
         |
144 | | simpl 464 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
145 | 144 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . 19
 
           |
146 | 145 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . 18
 
                   |
147 | 146 | fveq2d 5883 |
. . . . . . . . . . . . . . . . 17
 
                           |
148 | 147 | eleq2d 2534 |
. . . . . . . . . . . . . . . 16
 
                             |
149 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
150 | 149 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . 19
 
           |
151 | 150 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . 18
 
                   |
152 | 151 | fveq2d 5883 |
. . . . . . . . . . . . . . . . 17
 
                           |
153 | 152 | eleq2d 2534 |
. . . . . . . . . . . . . . . 16
 
                             |
154 | 143, 148,
153 | 3anbi123d 1365 |
. . . . . . . . . . . . . . 15
 
                                                             |
155 | 154 | anbi2d 718 |
. . . . . . . . . . . . . 14
 
                               
                                 |
156 | 155 | imbi1d 324 |
. . . . . . . . . . . . 13
 
                                   
                                     |
157 | | mclspps.8 |
. . . . . . . . . . . . 13
 
                                 |
158 | 141, 142,
156, 157 | vtocl2 3088 |
. . . . . . . . . . . 12
 
                                 |
159 | 158 | 3exp2 1251 |
. . . . . . . . . . 11
                                     |
160 | 159 | imp4b 601 |
. . . . . . . . . 10
 
                             
     |
161 | 117, 140,
160 | syl2anc 673 |
. . . . . . . . 9
      
           
                                        
     |
162 | 161 | rexlimdvva 2878 |
. . . . . . . 8
 
    
                                                    
     |
163 | 116, 162 | syl5bir 226 |
. . . . . . 7
 
                               
                         
     |
164 | 115, 163 | sylbid 223 |
. . . . . 6
 
                                 
     |
165 | 164 | exp4b 618 |
. . . . 5
                                         |
166 | 165 | 3imp2 1248 |
. . . 4
 
                                     |
167 | 16, 3, 23, 6, 24, 25, 7, 2, 26, 27, 28, 14, 31, 64, 75, 166 | mclsax 30279 |
. . 3
             |
168 | 22, 167 | eqeltrrd 2550 |
. 2
               |
169 | | ffn 5739 |
. . . 4
    
  |
170 | 33, 169 | syl 17 |
. . 3
   |
171 | | elpreima 6017 |
. . 3
                                    |
172 | 170, 171 | syl 17 |
. 2
                                    |
173 | 20, 168, 172 | mpbir2and 936 |
1
                |