Step | Hyp | Ref
| Expression |
1 | | cnvimass 5187 |
. . . . . . . . 9
        |
2 | 1 | a1i 11 |
. . . . . . . 8
 
          |
3 | | wessf1ornlem.f |
. . . . . . . . . 10
   |
4 | | fndm 5673 |
. . . . . . . . . 10
   |
5 | 3, 4 | syl 17 |
. . . . . . . . 9
   |
6 | 5 | adantr 467 |
. . . . . . . 8
 
   |
7 | 2, 6 | sseqtrd 3467 |
. . . . . . 7
 
          |
8 | | wessf1ornlem.r |
. . . . . . . . . 10
   |
9 | 8 | adantr 467 |
. . . . . . . . 9
 
   |
10 | 1, 5 | syl5sseq 3479 |
. . . . . . . . . . 11
          |
11 | | wessf1ornlem.a |
. . . . . . . . . . 11
   |
12 | | ssexg 4548 |
. . . . . . . . . . 11
                   |
13 | 10, 11, 12 | syl2anc 666 |
. . . . . . . . . 10
          |
14 | 13 | adantr 467 |
. . . . . . . . 9
 
          |
15 | | inisegn0 5199 |
. . . . . . . . . . 11

         |
16 | 15 | biimpi 198 |
. . . . . . . . . 10
          |
17 | 16 | adantl 468 |
. . . . . . . . 9
 
          |
18 | | wereu 4829 |
. . . . . . . . 9
                          
                    |
19 | 9, 14, 7, 17, 18 | syl13anc 1269 |
. . . . . . . 8
 
 
                    |
20 | | riotacl 6264 |
. . . . . . . 8
                                                  |
21 | 19, 20 | syl 17 |
. . . . . . 7
 
                               |
22 | 7, 21 | sseldd 3432 |
. . . . . 6
 
                        |
23 | 22 | ralrimiva 2801 |
. . . . 5
                          |
24 | | wessf1ornlem.g |
. . . . . . 7
                        |
25 | | sneq 3977 |
. . . . . . . . . . 11
       |
26 | 25 | imaeq2d 5167 |
. . . . . . . . . 10
                 |
27 | 26 | raleqdv 2992 |
. . . . . . . . . 10
  
        
             |
28 | 26, 27 | riotaeqbidv 6253 |
. . . . . . . . 9
                                             |
29 | | breq1 4404 |
. . . . . . . . . . . . . . 15
   
     |
30 | 29 | notbid 296 |
. . . . . . . . . . . . . 14
   
     |
31 | 30 | cbvralv 3018 |
. . . . . . . . . . . . 13
 
                     |
32 | 31 | a1i 11 |
. . . . . . . . . . . 12
  
        
             |
33 | | breq2 4405 |
. . . . . . . . . . . . . 14
   
     |
34 | 33 | notbid 296 |
. . . . . . . . . . . . 13
   
     |
35 | 34 | ralbidv 2826 |
. . . . . . . . . . . 12
  
        
             |
36 | 32, 35 | bitrd 257 |
. . . . . . . . . . 11
  
        
             |
37 | 36 | cbvriotav 6261 |
. . . . . . . . . 10
                                           |
38 | 37 | a1i 11 |
. . . . . . . . 9
                                             |
39 | 28, 38 | eqtrd 2484 |
. . . . . . . 8
                                             |
40 | 39 | cbvmptv 4494 |
. . . . . . 7
  
                                            |
41 | 24, 40 | eqtri 2472 |
. . . . . 6
                        |
42 | 41 | rnmptss 6050 |
. . . . 5
 
  
                  
  |
43 | 23, 42 | syl 17 |
. . . 4
   |
44 | 11, 43 | ssexd 4549 |
. . . . 5
   |
45 | | elpwg 3958 |
. . . . 5
      |
46 | 44, 45 | syl 17 |
. . . 4
  
   |
47 | 43, 46 | mpbird 236 |
. . 3
    |
48 | | dffn3 5734 |
. . . . . . . . . 10

      |
49 | 48 | biimpi 198 |
. . . . . . . . 9
    
  |
50 | 3, 49 | syl 17 |
. . . . . . . 8
       |
51 | 50, 43 | fssresd 5748 |
. . . . . . 7
         |
52 | | simpl 459 |
. . . . . . . . 9
 
     |
53 | | simprl 763 |
. . . . . . . . 9
 
     |
54 | | simprr 765 |
. . . . . . . . 9
 
     |
55 | | simpl 459 |
. . . . . . . . . . 11
           
     
   |
56 | | fvres 5877 |
. . . . . . . . . . . . . . 15
             |
57 | 56 | eqcomd 2456 |
. . . . . . . . . . . . . 14
      
      |
58 | 57 | ad2antrr 731 |
. . . . . . . . . . . . 13
     
                       |
59 | | simpr 463 |
. . . . . . . . . . . . 13
     
                         |
60 | | fvres 5877 |
. . . . . . . . . . . . . 14
             |
61 | 60 | ad2antlr 732 |
. . . . . . . . . . . . 13
     
                       |
62 | 58, 59, 61 | 3eqtrd 2488 |
. . . . . . . . . . . 12
     
                     |
63 | 62 | 3adantl1 1163 |
. . . . . . . . . . 11
           
               |
64 | | simpl1 1010 |
. . . . . . . . . . . . . 14
               |
65 | | simpl3 1012 |
. . . . . . . . . . . . . 14
               |
66 | | vex 3047 |
. . . . . . . . . . . . . . . . . . 19
 |
67 | 41 | elrnmpt 5080 |
. . . . . . . . . . . . . . . . . . 19
  
                        |
68 | 66, 67 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18

                        |
69 | 68 | biimpi 198 |
. . . . . . . . . . . . . . . . 17
 
                       |
70 | 69 | adantr 467 |
. . . . . . . . . . . . . . . 16
                                   |
71 | 70 | 3ad2antl2 1170 |
. . . . . . . . . . . . . . 15
             
                       |
72 | 71, 68 | sylibr 216 |
. . . . . . . . . . . . . 14
            
  |
73 | | id 22 |
. . . . . . . . . . . . . . . 16
                   |
74 | 73 | eqcomd 2456 |
. . . . . . . . . . . . . . 15
                   |
75 | 74 | adantl 468 |
. . . . . . . . . . . . . 14
                       |
76 | | eleq1 2516 |
. . . . . . . . . . . . . . . . . 18
     |
77 | 76 | 3anbi3d 1344 |
. . . . . . . . . . . . . . . . 17
  


    |
78 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . 18
           |
79 | 78 | eqeq2d 2460 |
. . . . . . . . . . . . . . . . 17
         
           |
80 | 77, 79 | anbi12d 716 |
. . . . . . . . . . . . . . . 16
   
           
             |
81 | | breq1 4404 |
. . . . . . . . . . . . . . . . 17
   
     |
82 | 81 | notbid 296 |
. . . . . . . . . . . . . . . 16
   
     |
83 | 80, 82 | imbi12d 322 |
. . . . . . . . . . . . . . 15
    
            
  
                |
84 | | eleq1 2516 |
. . . . . . . . . . . . . . . . . . 19
     |
85 | 84 | 3anbi2d 1343 |
. . . . . . . . . . . . . . . . . 18
  


    |
86 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . 19
           |
87 | 86 | eqeq1d 2452 |
. . . . . . . . . . . . . . . . . 18
         
           |
88 | 85, 87 | anbi12d 716 |
. . . . . . . . . . . . . . . . 17
   
           
             |
89 | | breq2 4405 |
. . . . . . . . . . . . . . . . . 18
   
     |
90 | 89 | notbid 296 |
. . . . . . . . . . . . . . . . 17
   
     |
91 | 88, 90 | imbi12d 322 |
. . . . . . . . . . . . . . . 16
    
            
  
                |
92 | | eleq1 2516 |
. . . . . . . . . . . . . . . . . . . 20
     |
93 | 92 | 3anbi3d 1344 |
. . . . . . . . . . . . . . . . . . 19
  


    |
94 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . 20
           |
95 | 94 | eqeq2d 2460 |
. . . . . . . . . . . . . . . . . . 19
         
           |
96 | 93, 95 | anbi12d 716 |
. . . . . . . . . . . . . . . . . 18
   
           
             |
97 | | breq1 4404 |
. . . . . . . . . . . . . . . . . . 19
   
     |
98 | 97 | notbid 296 |
. . . . . . . . . . . . . . . . . 18
   
     |
99 | 96, 98 | imbi12d 322 |
. . . . . . . . . . . . . . . . 17
    
            
  
                |
100 | | eleq1 2516 |
. . . . . . . . . . . . . . . . . . . . 21
     |
101 | 100 | 3anbi2d 1343 |
. . . . . . . . . . . . . . . . . . . 20
  


    |
102 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . . 21
           |
103 | 102 | eqeq1d 2452 |
. . . . . . . . . . . . . . . . . . . 20
         
           |
104 | 101, 103 | anbi12d 716 |
. . . . . . . . . . . . . . . . . . 19
   
           
             |
105 | | breq2 4405 |
. . . . . . . . . . . . . . . . . . . 20
   
     |
106 | 105 | notbid 296 |
. . . . . . . . . . . . . . . . . . 19
   
     |
107 | 104, 106 | imbi12d 322 |
. . . . . . . . . . . . . . . . . 18
    
            
  
                |
108 | | nfv 1760 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
109 | | nfcv 2591 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
110 | | nfmpt1 4491 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                          |
111 | 41, 110 | nfcxfr 2589 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
112 | 111 | nfrn 5076 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
113 | 109, 112 | nfel 2603 |
. . . . . . . . . . . . . . . . . . . . . 22

 |
114 | 112 | nfcri 2585 |
. . . . . . . . . . . . . . . . . . . . . 22

 |
115 | 108, 113,
114 | nf3an 2012 |
. . . . . . . . . . . . . . . . . . . . 21
  
  |
116 | | nfv 1760 |
. . . . . . . . . . . . . . . . . . . . 21
           |
117 | 115, 116 | nfan 2010 |
. . . . . . . . . . . . . . . . . . . 20
   
           |
118 | | nfv 1760 |
. . . . . . . . . . . . . . . . . . . 20
    |
119 | | simp3 1009 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
                       
                     |
120 | 119 | eqcomd 2456 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
                                             |
121 | | simp11 1037 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
                        |
122 | | simp2 1008 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
                        |
123 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                     
                       |
124 | | breq2 4405 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   
     |
125 | 124 | notbid 296 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   
     |
126 | 125 | ralbidv 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
  
        
             |
127 | 126 | cbvriotav 6261 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                                           |
128 | 127 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                                                                  |
129 | 123, 128 | eqtr2d 2485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                                             |
130 | 129 | 3ad2ant3 1030 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
                                             |
131 | 126 | cbvreuv 3020 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                                         |
132 | 19, 131 | sylib 200 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
 
                    |
133 | | riota1 6268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                                                                |
134 | 132, 133 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
          
         
                        |
135 | 134 | 3adant3 1027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
                               
         
                        |
136 | 130, 135 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
                              
            |
137 | 136 | simpld 461 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
                               |
138 | 121, 122,
119, 137 | syl3anc 1267 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
                               |
139 | 121, 122,
19 | syl2anc 666 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
                                           |
140 | 126 | riota2 6272 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         
                  
 
                                 |
141 | 138, 139,
140 | syl2anc 666 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
                                                         |
142 | 120, 141 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
                                  |
143 | 142 | 3adant1r 1260 |
. . . . . . . . . . . . . . . . . . . . . 22
   
         
                                  |
144 | 43 | sselda 3431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
   |
145 | 144 | 3adant2 1026 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
   |
146 | 145 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
               |
147 | 146 | 3ad2ant1 1028 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
         
                        |
148 | 74 | ad2antlr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
                     |
149 | 148 | 3adant3 1027 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
         
                                |
150 | | fniniseg 6001 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
        

        |
151 | 121, 3, 150 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
                                       |
152 | 138, 151 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
                              |
153 | 152 | simprd 465 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
                            |
154 | 153 | 3adant1r 1260 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
         
                            |
155 | 149, 154 | eqtrd 2484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
         
                            |
156 | 147, 155 | jca 535 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
         
                              |
157 | | fniniseg 6001 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
        

        |
158 | 3, 157 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
        

        |
159 | 158 | 3ad2ant1 1028 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
        

        |
160 | 159 | ad2antrr 731 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
                  

        |
161 | 160 | 3adant3 1027 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
         
                                       |
162 | 156, 161 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . . . 22
   
         
                               |
163 | | rspa 2754 |
. . . . . . . . . . . . . . . . . . . . . 22
           
       
    |
164 | 143, 162,
163 | syl2anc 666 |
. . . . . . . . . . . . . . . . . . . . 21
   
         
                     
    |
165 | 164 | 3exp 1206 |
. . . . . . . . . . . . . . . . . . . 20
                                   
      |
166 | 117, 118,
165 | rexlimd 2870 |
. . . . . . . . . . . . . . . . . . 19
              
                    
     |
167 | 71, 166 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
                 |
168 | 107, 167 | chvarv 2106 |
. . . . . . . . . . . . . . . . 17
                 |
169 | 99, 168 | chvarv 2106 |
. . . . . . . . . . . . . . . 16
                 |
170 | 91, 169 | chvarv 2106 |
. . . . . . . . . . . . . . 15
                 |
171 | 83, 170 | chvarv 2106 |
. . . . . . . . . . . . . 14
                 |
172 | 64, 65, 72, 75, 171 | syl31anc 1270 |
. . . . . . . . . . . . 13
                 |
173 | 172, 167 | jca 535 |
. . . . . . . . . . . 12
                     |
174 | | weso 4824 |
. . . . . . . . . . . . . . . 16
   |
175 | 8, 174 | syl 17 |
. . . . . . . . . . . . . . 15
   |
176 | 175 | adantr 467 |
. . . . . . . . . . . . . 14
 
        
  |
177 | 176 | 3ad2antl1 1169 |
. . . . . . . . . . . . 13
            
  |
178 | 43 | sselda 3431 |
. . . . . . . . . . . . . . 15
 
   |
179 | 178 | 3adant3 1027 |
. . . . . . . . . . . . . 14
 

  |
180 | 179 | adantr 467 |
. . . . . . . . . . . . 13
            
  |
181 | | sotrieq2 4782 |
. . . . . . . . . . . . 13
  
  
         |
182 | 177, 180,
146, 181 | syl12anc 1265 |
. . . . . . . . . . . 12
                       |
183 | 173, 182 | mpbird 236 |
. . . . . . . . . . 11
            
  |
184 | 55, 63, 183 | syl2anc 666 |
. . . . . . . . . 10
           
       |
185 | 184 | ex 436 |
. . . . . . . . 9
 
                 |
186 | 52, 53, 54, 185 | syl3anc 1267 |
. . . . . . . 8
 
     
         
   |
187 | 186 | ralrimivva 2808 |
. . . . . . 7
                     |
188 | 51, 187 | jca 535 |
. . . . . 6
        
 
         
   
    |
189 | | dff13 6157 |
. . . . . 6
 
            
 
         
   
    |
190 | 188, 189 | sylibr 216 |
. . . . 5
         |
191 | | riotaex 6254 |
. . . . . . . . . . . . . 14
                      |
192 | 191 | rgenw 2748 |
. . . . . . . . . . . . 13
                        |
193 | 192 | a1i 11 |
. . . . . . . . . . . 12
                          |
194 | 41 | fnmpt 5702 |
. . . . . . . . . . . 12
 
  
                     |
195 | 193, 194 | syl 17 |
. . . . . . . . . . 11
   |
196 | | dffn3 5734 |
. . . . . . . . . . . 12

   
  |
197 | 196 | biimpi 198 |
. . . . . . . . . . 11
       |
198 | 195, 197 | syl 17 |
. . . . . . . . . 10
       |
199 | 198 | ffvelrnda 6020 |
. . . . . . . . 9
 
       |
200 | | fvres 5877 |
. . . . . . . . . . 11
                         |
201 | 199, 200 | syl 17 |
. . . . . . . . . 10
 
                     |
202 | 17, 15 | sylibr 216 |
. . . . . . . . . . . . . 14
 
   |
203 | 191 | a1i 11 |
. . . . . . . . . . . . . 14
 
                        |
204 | 41 | fvmpt2 5955 |
. . . . . . . . . . . . . 14
                                                   |
205 | 202, 203,
204 | syl2anc 666 |
. . . . . . . . . . . . 13
 
                            |
206 | 205, 21 | eqeltrd 2528 |
. . . . . . . . . . . 12
 
              |
207 | | fvex 5873 |
. . . . . . . . . . . . . 14
     |
208 | | eleq1 2516 |
. . . . . . . . . . . . . . . 16
            
              |
209 | | eleq1 2516 |
. . . . . . . . . . . . . . . . 17
     
       |
210 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . 18
                   |
211 | 210 | eqeq1d 2452 |
. . . . . . . . . . . . . . . . 17
         
           |
212 | 209, 211 | anbi12d 716 |
. . . . . . . . . . . . . . . 16
                             |
213 | 208, 212 | bibi12d 323 |
. . . . . . . . . . . . . . 15
             

     
                              |
214 | 213 | imbi2d 318 |
. . . . . . . . . . . . . 14
      
               
            
    
              |
215 | 3, 150 | syl 17 |
. . . . . . . . . . . . . 14
        

        |
216 | 207, 214,
215 | vtocl 3099 |
. . . . . . . . . . . . 13
            
    
            |
217 | 216 | adantr 467 |
. . . . . . . . . . . 12
 
            
    
            |
218 | 206, 217 | mpbid 214 |
. . . . . . . . . . 11
 
                 |
219 | 218 | simprd 465 |
. . . . . . . . . 10
 
           |
220 | 201, 219 | eqtr2d 2485 |
. . . . . . . . 9
 
             |
221 | | fveq2 5863 |
. . . . . . . . . . 11
                       |
222 | 221 | eqeq2d 2460 |
. . . . . . . . . 10
       
   
             |
223 | 222 | rspcev 3149 |
. . . . . . . . 9
     
             
      |
224 | 199, 220,
223 | syl2anc 666 |
. . . . . . . 8
 
          |
225 | 224 | ralrimiva 2801 |
. . . . . . 7
     
      |
226 | 51, 225 | jca 535 |
. . . . . 6
        
 
         |
227 | | dffo3 6035 |
. . . . . 6
 
            
 
         |
228 | 226, 227 | sylibr 216 |
. . . . 5
         |
229 | 190, 228 | jca 535 |
. . . 4
                 |
230 | | df-f1o 5588 |
. . . 4
 
           
         |
231 | 229, 230 | sylibr 216 |
. . 3
         |
232 | | nfcv 2591 |
. . . . . 6
   |
233 | | nfcv 2591 |
. . . . . . . . 9
   |
234 | | nfriota1 6257 |
. . . . . . . . 9
                        |
235 | 233, 234 | nfmpt 4490 |
. . . . . . . 8
                          |
236 | 41, 235 | nfcxfr 2589 |
. . . . . . 7
   |
237 | 236 | nfrn 5076 |
. . . . . 6
   |
238 | 232, 237 | nfres 5106 |
. . . . 5
     |
239 | 238, 237,
233 | nff1o 5810 |
. . . 4
         |
240 | | reseq2 5099 |
. . . . 5
       |
241 | | id 22 |
. . . . 5
   |
242 | | eqidd 2451 |
. . . . 5
   |
243 | 240, 241,
242 | f1oeq123d 5809 |
. . . 4
                 |
244 | 239, 243 | rspce 3144 |
. . 3
                    |
245 | 47, 231, 244 | syl2anc 666 |
. 2
           |
246 | | reseq2 5099 |
. . . 4
       |
247 | | id 22 |
. . . 4
   |
248 | | eqidd 2451 |
. . . 4
   |
249 | 246, 247,
248 | f1oeq123d 5809 |
. . 3
        
        |
250 | 249 | cbvrexv 3019 |
. 2
                   |
251 | 245, 250 | sylib 200 |
1
           |