Step | Hyp | Ref
| Expression |
1 | | wunex2.u |
. . . . . . . 8

 |
2 | 1 | eleq2i 2521 |
. . . . . . 7

   |
3 | | frfnom 7152 |
. . . . . . . . 9
            
 
              |
4 | | wunex2.f |
. . . . . . . . . 10
        
     
              |
5 | 4 | fneq1i 5670 |
. . . . . . . . 9

            
 
               |
6 | 3, 5 | mpbir 213 |
. . . . . . . 8
 |
7 | | fnunirn 6158 |
. . . . . . . 8
   
       |
8 | 6, 7 | ax-mp 5 |
. . . . . . 7
         |
9 | 2, 8 | bitri 253 |
. . . . . 6

       |
10 | | elssuni 4227 |
. . . . . . . . . . 11
            |
11 | 10 | ad2antll 735 |
. . . . . . . . . 10
  
     
       |
12 | | ssun2 3598 |
. . . . . . . . . . 11
                 |
13 | | ssun1 3597 |
. . . . . . . . . . 11
                                
 
            |
14 | 12, 13 | sstri 3441 |
. . . . . . . . . 10
                                         |
15 | 11, 14 | syl6ss 3444 |
. . . . . . . . 9
  
     
                                     |
16 | | simprl 764 |
. . . . . . . . . 10
  
     
  |
17 | | fvex 5875 |
. . . . . . . . . . . 12
     |
18 | 17 | uniex 6587 |
. . . . . . . . . . . 12
      |
19 | 17, 18 | unex 6589 |
. . . . . . . . . . 11
            |
20 | | prex 4642 |
. . . . . . . . . . . . 13
  
 
 |
21 | 17 | mptex 6136 |
. . . . . . . . . . . . . 14
          |
22 | 21 | rnex 6727 |
. . . . . . . . . . . . 13
          |
23 | 20, 22 | unex 6589 |
. . . . . . . . . . . 12
     
           |
24 | 17, 23 | iunex 6773 |
. . . . . . . . . . 11
         
 
           |
25 | 19, 24 | unex 6589 |
. . . . . . . . . 10
                     
 
            |
26 | | id 22 |
. . . . . . . . . . . . 13
   |
27 | | unieq 4206 |
. . . . . . . . . . . . 13
     |
28 | 26, 27 | uneq12d 3589 |
. . . . . . . . . . . 12
         |
29 | | pweq 3954 |
. . . . . . . . . . . . . . . 16
 
   |
30 | | unieq 4206 |
. . . . . . . . . . . . . . . 16
     |
31 | 29, 30 | preq12d 4059 |
. . . . . . . . . . . . . . 15
   
 
  
    |
32 | | preq2 4052 |
. . . . . . . . . . . . . . . . . 18
         |
33 | 32 | cbvmptv 4495 |
. . . . . . . . . . . . . . . . 17
           |
34 | | preq1 4051 |
. . . . . . . . . . . . . . . . . 18
         |
35 | 34 | mpteq2dv 4490 |
. . . . . . . . . . . . . . . . 17
             |
36 | 33, 35 | syl5eq 2497 |
. . . . . . . . . . . . . . . 16
             |
37 | 36 | rneqd 5062 |
. . . . . . . . . . . . . . 15
             |
38 | 31, 37 | uneq12d 3589 |
. . . . . . . . . . . . . 14
      
                    |
39 | 38 | cbviunv 4317 |
. . . . . . . . . . . . 13

     
      
     
       |
40 | | mpteq1 4483 |
. . . . . . . . . . . . . . . 16
             |
41 | 40 | rneqd 5062 |
. . . . . . . . . . . . . . 15
             |
42 | 41 | uneq2d 3588 |
. . . . . . . . . . . . . 14
      
                    |
43 | 26, 42 | iuneq12d 4304 |
. . . . . . . . . . . . 13
 
     
      
     
        |
44 | 39, 43 | syl5eq 2497 |
. . . . . . . . . . . 12
 
     
      
     
        |
45 | 28, 44 | uneq12d 3589 |
. . . . . . . . . . 11
     
     
               
 
         |
46 | | id 22 |
. . . . . . . . . . . . 13
           |
47 | | unieq 4206 |
. . . . . . . . . . . . 13
             |
48 | 46, 47 | uneq12d 3589 |
. . . . . . . . . . . 12
                     |
49 | | mpteq1 4483 |
. . . . . . . . . . . . . . 15
                     |
50 | 49 | rneqd 5062 |
. . . . . . . . . . . . . 14
                     |
51 | 50 | uneq2d 3588 |
. . . . . . . . . . . . 13
          
                        |
52 | 46, 51 | iuneq12d 4304 |
. . . . . . . . . . . 12
     
     
               
 
            |
53 | 48, 52 | uneq12d 3589 |
. . . . . . . . . . 11
         
     
                            
 
             |
54 | 4, 45, 53 | frsucmpt2 7157 |
. . . . . . . . . 10
                                                               
 
             |
55 | 16, 25, 54 | sylancl 668 |
. . . . . . . . 9
  
     
                                         |
56 | 15, 55 | sseqtr4d 3469 |
. . . . . . . 8
  
     
      |
57 | | fvssunirn 5888 |
. . . . . . . . 9
  
 
 |
58 | 57, 1 | sseqtr4i 3465 |
. . . . . . . 8
  
  |
59 | 56, 58 | syl6ss 3444 |
. . . . . . 7
  
     
  |
60 | 59 | rexlimdvaa 2880 |
. . . . . 6
  
       |
61 | 9, 60 | syl5bi 221 |
. . . . 5
 
   |
62 | 61 | ralrimiv 2800 |
. . . 4
 
  |
63 | | dftr3 4501 |
. . . 4
    |
64 | 62, 63 | sylibr 216 |
. . 3
   |
65 | | 1on 7189 |
. . . . . . . 8
 |
66 | | unexg 6592 |
. . . . . . . 8
    
  |
67 | 65, 66 | mpan2 677 |
. . . . . . 7
 
   |
68 | 4 | fveq1i 5866 |
. . . . . . . 8
             
     
                 |
69 | | fr0g 7153 |
. . . . . . . 8
            
     
                    |
70 | 68, 69 | syl5eq 2497 |
. . . . . . 7
           |
71 | 67, 70 | syl 17 |
. . . . . 6
         |
72 | | fvssunirn 5888 |
. . . . . . 7
      |
73 | 72, 1 | sseqtr4i 3465 |
. . . . . 6
     |
74 | 71, 73 | syl6eqssr 3483 |
. . . . 5
 
   |
75 | 74 | unssbd 3612 |
. . . 4
   |
76 | | 1n0 7197 |
. . . 4
 |
77 | | ssn0 3767 |
. . . 4
 
   |
78 | 75, 76, 77 | sylancl 668 |
. . 3
   |
79 | | pweq 3954 |
. . . . . . . . . . . . . . 15
 
   |
80 | | unieq 4206 |
. . . . . . . . . . . . . . 15
     |
81 | 79, 80 | preq12d 4059 |
. . . . . . . . . . . . . 14
   
 
  
    |
82 | | preq1 4051 |
. . . . . . . . . . . . . . . 16
         |
83 | 82 | mpteq2dv 4490 |
. . . . . . . . . . . . . . 15
                     |
84 | 83 | rneqd 5062 |
. . . . . . . . . . . . . 14
                     |
85 | 81, 84 | uneq12d 3589 |
. . . . . . . . . . . . 13
      
                            |
86 | 85 | ssiun2s 4322 |
. . . . . . . . . . . 12
          
                                  |
87 | 86 | ad2antll 735 |
. . . . . . . . . . 11
  
     
     
         
         
 
            |
88 | | ssun2 3598 |
. . . . . . . . . . . . 13
         
 
         
                     
 
            |
89 | 88, 55 | syl5sseqr 3481 |
. . . . . . . . . . . 12
  
     
         
 
         
      |
90 | 89, 58 | syl6ss 3444 |
. . . . . . . . . . 11
  
     
         
 
         
  |
91 | 87, 90 | sstrd 3442 |
. . . . . . . . . 10
  
     
     
         
  |
92 | 91 | unssad 3611 |
. . . . . . . . 9
  
     
  
    |
93 | | vex 3048 |
. . . . . . . . . . 11
 |
94 | 93 | pwex 4586 |
. . . . . . . . . 10
  |
95 | 93 | uniex 6587 |
. . . . . . . . . 10
  |
96 | 94, 95 | prss 4126 |
. . . . . . . . 9
            |
97 | 92, 96 | sylibr 216 |
. . . . . . . 8
  
     
 
    |
98 | 97 | simprd 465 |
. . . . . . 7
  
     
   |
99 | 97 | simpld 461 |
. . . . . . 7
  
     
   |
100 | 1 | eleq2i 2521 |
. . . . . . . . . 10

   |
101 | | fnunirn 6158 |
. . . . . . . . . . 11
   
       |
102 | 6, 101 | ax-mp 5 |
. . . . . . . . . 10
         |
103 | 100, 102 | bitri 253 |
. . . . . . . . 9

       |
104 | | simplrl 770 |
. . . . . . . . . . . . . . . . 17
                
  |
105 | | simprl 764 |
. . . . . . . . . . . . . . . . 17
                
  |
106 | | ordom 6701 |
. . . . . . . . . . . . . . . . . 18
 |
107 | | ordunel 6654 |
. . . . . . . . . . . . . . . . . 18
       |
108 | 106, 107 | mp3an1 1351 |
. . . . . . . . . . . . . . . . 17
 
     |
109 | 104, 105,
108 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
                     |
110 | | ssun1 3597 |
. . . . . . . . . . . . . . . . 17

  |
111 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . 19
           |
112 | 111 | sseq2d 3460 |
. . . . . . . . . . . . . . . . . 18
     
   
           |
113 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . 19
           |
114 | 113 | sseq2d 3460 |
. . . . . . . . . . . . . . . . . 18
     
   
           |
115 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . 19
       
   |
116 | 115 | sseq2d 3460 |
. . . . . . . . . . . . . . . . . 18
                     |
117 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . 19
          
    |
118 | 117 | sseq2d 3460 |
. . . . . . . . . . . . . . . . . 18
       
   
             |
119 | | ssid 3451 |
. . . . . . . . . . . . . . . . . . 19
         |
120 | 119 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
           |
121 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
122 | | suceq 5488 |
. . . . . . . . . . . . . . . . . . . . . . 23

  |
123 | 122 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
124 | 121, 123 | sseq12d 3461 |
. . . . . . . . . . . . . . . . . . . . 21
     
   
           |
125 | | ssun1 3597 |
. . . . . . . . . . . . . . . . . . . . . . 23
                |
126 | 125, 13 | sstri 3441 |
. . . . . . . . . . . . . . . . . . . . . 22
                                        |
127 | 25, 54 | mpan2 677 |
. . . . . . . . . . . . . . . . . . . . . 22
                          
 
             |
128 | 126, 127 | syl5sseqr 3481 |
. . . . . . . . . . . . . . . . . . . . 21
           |
129 | 124, 128 | vtoclga 3113 |
. . . . . . . . . . . . . . . . . . . 20
           |
130 | 129 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . 19
   
           |
131 | | sstr2 3439 |
. . . . . . . . . . . . . . . . . . 19
             
       
       |
132 | 130, 131 | syl5com 31 |
. . . . . . . . . . . . . . . . . 18
   
                     |
133 | 112, 114,
116, 118, 120, 132 | findsg 6720 |
. . . . . . . . . . . . . . . . 17
     
               |
134 | 110, 133 | mpan2 677 |
. . . . . . . . . . . . . . . 16
   
    
        |
135 | 109, 104,
134 | syl2anc 667 |
. . . . . . . . . . . . . . 15
                    
        |
136 | | simplrr 771 |
. . . . . . . . . . . . . . 15
                       |
137 | 135, 136 | sseldd 3433 |
. . . . . . . . . . . . . 14
                         |
138 | 82 | mpteq2dv 4490 |
. . . . . . . . . . . . . . . . 17
                
        |
139 | 138 | rneqd 5062 |
. . . . . . . . . . . . . . . 16
                         |
140 | 81, 139 | uneq12d 3589 |
. . . . . . . . . . . . . . 15
      
                                |
141 | 140 | ssiun2s 4322 |
. . . . . . . . . . . . . 14
    
       
                                        |
142 | 137, 141 | syl 17 |
. . . . . . . . . . . . 13
                                                               |
143 | | ssun2 3598 |
. . . . . . . . . . . . . . 15
           
 
    
      
                           
 
    
         |
144 | | fvex 5875 |
. . . . . . . . . . . . . . . . . 18
       |
145 | 144 | uniex 6587 |
. . . . . . . . . . . . . . . . . 18
        |
146 | 144, 145 | unex 6589 |
. . . . . . . . . . . . . . . . 17
                |
147 | 144 | mptex 6136 |
. . . . . . . . . . . . . . . . . . . 20
    
       |
148 | 147 | rnex 6727 |
. . . . . . . . . . . . . . . . . . 19
            |
149 | 20, 148 | unex 6589 |
. . . . . . . . . . . . . . . . . 18
     
             |
150 | 144, 149 | iunex 6773 |
. . . . . . . . . . . . . . . . 17
           
 
    
        |
151 | 146, 150 | unex 6589 |
. . . . . . . . . . . . . . . 16
                           
 
    
         |
152 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
    
     
    |
153 | | unieq 4206 |
. . . . . . . . . . . . . . . . . . 19
    
       
    |
154 | 152, 153 | uneq12d 3589 |
. . . . . . . . . . . . . . . . . 18
    
                      |
155 | | mpteq1 4483 |
. . . . . . . . . . . . . . . . . . . . 21
    
           
        |
156 | 155 | rneqd 5062 |
. . . . . . . . . . . . . . . . . . . 20
    
                    |
157 | 156 | uneq2d 3588 |
. . . . . . . . . . . . . . . . . . 19
    
       
                          |
158 | 152, 157 | iuneq12d 4304 |
. . . . . . . . . . . . . . . . . 18
    
  
     
                 
 
    
         |
159 | 154, 158 | uneq12d 3589 |
. . . . . . . . . . . . . . . . 17
    
      
     
                                  
 
    
          |
160 | 4, 45, 159 | frsucmpt2 7157 |
. . . . . . . . . . . . . . . 16
                
                                  
       
                     
 
    
          |
161 | 109, 151,
160 | sylancl 668 |
. . . . . . . . . . . . . . 15
                    
       
                     
 
    
          |
162 | 143, 161 | syl5sseqr 3481 |
. . . . . . . . . . . . . 14
                 
                                 |
163 | | fvssunirn 5888 |
. . . . . . . . . . . . . . 15
  
     |
164 | 163, 1 | sseqtr4i 3465 |
. . . . . . . . . . . . . 14
  
    |
165 | 162, 164 | syl6ss 3444 |
. . . . . . . . . . . . 13
                 
                           |
166 | 142, 165 | sstrd 3442 |
. . . . . . . . . . . 12
                                     |
167 | 166 | unssbd 3612 |
. . . . . . . . . . 11
                              |
168 | | ssun2 3598 |
. . . . . . . . . . . . . . . . . . 19

  |
169 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
       |
170 | 168, 169 | syl5sseqr 3481 |
. . . . . . . . . . . . . . . . . 18
     |
171 | 170 | biantrud 510 |
. . . . . . . . . . . . . . . . 17
   
     |
172 | 171 | bicomd 205 |
. . . . . . . . . . . . . . . 16
    
    |
173 | | fveq2 5865 |
. . . . . . . . . . . . . . . . 17
          
    |
174 | 173 | sseq2d 3460 |
. . . . . . . . . . . . . . . 16
       
   
             |
175 | 172, 174 | imbi12d 322 |
. . . . . . . . . . . . . . 15
     

                        |
176 | | eleq1 2517 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
177 | 176 | anbi2d 710 |
. . . . . . . . . . . . . . . . . . 19
    
    |
178 | | sseq1 3453 |
. . . . . . . . . . . . . . . . . . 19
 
   |
179 | 177, 178 | anbi12d 717 |
. . . . . . . . . . . . . . . . . 18
   
 
 

    |
180 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . 19
           |
181 | 180 | sseq1d 3459 |
. . . . . . . . . . . . . . . . . 18
     
   
           |
182 | 179, 181 | imbi12d 322 |
. . . . . . . . . . . . . . . . 17
               
   
             |
183 | 112, 114,
116, 114, 120, 132 | findsg 6720 |
. . . . . . . . . . . . . . . . 17
   
           |
184 | 182, 183 | chvarv 2107 |
. . . . . . . . . . . . . . . 16
   
           |
185 | 184 | expl 624 |
. . . . . . . . . . . . . . 15
  
    
       |
186 | 175, 185 | vtoclga 3113 |
. . . . . . . . . . . . . 14
           
     |
187 | 109, 105,
186 | sylc 62 |
. . . . . . . . . . . . 13
                    
        |
188 | | simprr 766 |
. . . . . . . . . . . . 13
                       |
189 | 187, 188 | sseldd 3433 |
. . . . . . . . . . . 12
                         |
190 | | prex 4642 |
. . . . . . . . . . . 12
    |
191 | | eqid 2451 |
. . . . . . . . . . . . 13
    
                  |
192 | | preq2 4052 |
. . . . . . . . . . . . 13
         |
193 | 191, 192 | elrnmpt1s 5082 |
. . . . . . . . . . . 12
                            |
194 | 189, 190,
193 | sylancl 668 |
. . . . . . . . . . 11
                                 |
195 | 167, 194 | sseldd 3433 |
. . . . . . . . . 10
                      |
196 | 195 | rexlimdvaa 2880 |
. . . . . . . . 9
  
     
 
   
      |
197 | 103, 196 | syl5bi 221 |
. . . . . . . 8
  
     

      |
198 | 197 | ralrimiv 2800 |
. . . . . . 7
  
     

     |
199 | 98, 99, 198 | 3jca 1188 |
. . . . . 6
  
     
 

       |
200 | 199 | rexlimdvaa 2880 |
. . . . 5
  
     
         |
201 | 9, 200 | syl5bi 221 |
. . . 4
    

       |
202 | 201 | ralrimiv 2800 |
. . 3
 
 

       |
203 | | rdgfun 7134 |
. . . . . . . . 9
           
 
             |
204 | | omex 8148 |
. . . . . . . . 9
 |
205 | | resfunexg 6130 |
. . . . . . . . 9
         
     
                                           |
206 | 203, 204,
205 | mp2an 678 |
. . . . . . . 8
            
 
              |
207 | 4, 206 | eqeltri 2525 |
. . . . . . 7
 |
208 | 207 | rnex 6727 |
. . . . . 6
 |
209 | 208 | uniex 6587 |
. . . . 5
  |
210 | 1, 209 | eqeltri 2525 |
. . . 4
 |
211 | | iswun 9129 |
. . . 4
 
WUni 

 
          |
212 | 210, 211 | ax-mp 5 |
. . 3
 WUni  
 

        |
213 | 64, 78, 202, 212 | syl3anbrc 1192 |
. 2
 WUni |
214 | 74 | unssad 3611 |
. 2
   |
215 | 213, 214 | jca 535 |
1
 
WUni    |