Step | Hyp | Ref
| Expression |
1 | | omex 8148 |
. . . . 5
 |
2 | 1 | 0dom 7702 |
. . . 4
 |
3 | | breq1 4405 |
. . . 4
 
 
   |
4 | 2, 3 | mpbiri 237 |
. . 3
 
   |
5 | 4 | a1d 26 |
. 2
 
    
   |
6 | | n0 3741 |
. . 3
      |
7 | | ne0i 3737 |
. . . . . . . . . 10
  
  |
8 | | unieq 4206 |
. . . . . . . . . . . 12

    |
9 | | uni0 4225 |
. . . . . . . . . . . 12
  |
10 | 8, 9 | syl6eq 2501 |
. . . . . . . . . . 11

   |
11 | 10 | necon3i 2656 |
. . . . . . . . . 10
 
  |
12 | 7, 11 | syl 17 |
. . . . . . . . 9
    |
13 | 12 | adantl 468 |
. . . . . . . 8
    
    |
14 | | simpl1 1011 |
. . . . . . . . 9
    
    |
15 | | reldom 7575 |
. . . . . . . . . 10
 |
16 | 15 | brrelexi 4875 |
. . . . . . . . 9

  |
17 | | 0sdomg 7701 |
. . . . . . . . 9
 
   |
18 | 14, 16, 17 | 3syl 18 |
. . . . . . . 8
    
  
   |
19 | 13, 18 | mpbird 236 |
. . . . . . 7
    
 
  |
20 | | fodomr 7723 |
. . . . . . 7
  
       |
21 | 19, 14, 20 | syl2anc 667 |
. . . . . 6
    
         |
22 | | omelon 8151 |
. . . . . . . . . . . 12
 |
23 | | onenon 8383 |
. . . . . . . . . . . 12
   |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . 11
 |
25 | | xpnum 8385 |
. . . . . . . . . . 11
    
  |
26 | 24, 24, 25 | mp2an 678 |
. . . . . . . . . 10
   |
27 | | simplrr 771 |
. . . . . . . . . . . . . . . . . . 19
     
          
      |
28 | | fof 5793 |
. . . . . . . . . . . . . . . . . . 19
           |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . . . . . 18
     
          
      |
30 | | simprl 764 |
. . . . . . . . . . . . . . . . . 18
     
          
  |
31 | 29, 30 | ffvelrnd 6023 |
. . . . . . . . . . . . . . . . 17
     
          
      |
32 | 31 | adantr 467 |
. . . . . . . . . . . . . . . 16
               
 
               |
33 | | elssuni 4227 |
. . . . . . . . . . . . . . . 16
            |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . . . 15
               
 
                |
35 | 31, 33 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
     
          
       |
36 | | simpll3 1049 |
. . . . . . . . . . . . . . . . . . . . 21
     
          
   |
37 | | soss 4773 |
. . . . . . . . . . . . . . . . . . . . 21
      

       |
38 | 35, 36, 37 | sylc 62 |
. . . . . . . . . . . . . . . . . . . 20
     
          
      |
39 | | simpll2 1048 |
. . . . . . . . . . . . . . . . . . . . 21
     
          
  |
40 | 39, 31 | sseldd 3433 |
. . . . . . . . . . . . . . . . . . . 20
     
          
      |
41 | | finnisoeu 8544 |
. . . . . . . . . . . . . . . . . . . 20
                             |
42 | 38, 40, 41 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . 19
     
          
                  |
43 | | iotacl 5569 |
. . . . . . . . . . . . . . . . . . 19
                
  
                                   |
44 | 42, 43 | syl 17 |
. . . . . . . . . . . . . . . . . 18
     
          
  
                                   |
45 | | iotaex 5563 |
. . . . . . . . . . . . . . . . . . 19
                    |
46 | | isoeq1 6210 |
. . . . . . . . . . . . . . . . . . 19
                   
                                                     |
47 | | isoeq1 6210 |
. . . . . . . . . . . . . . . . . . . 20
 
              
                  |
48 | 47 | cbvabv 2575 |
. . . . . . . . . . . . . . . . . . 19

                                  |
49 | 45, 46, 48 | elab2 3188 |
. . . . . . . . . . . . . . . . . 18
                    
                                  
                 |
50 | 44, 49 | sylib 200 |
. . . . . . . . . . . . . . . . 17
     
          
  
                                 |
51 | | isof1o 6216 |
. . . . . . . . . . . . . . . . 17
                                                                        |
52 | | f1of 5814 |
. . . . . . . . . . . . . . . . 17
                                   
  
                                  |
53 | 50, 51, 52 | 3syl 18 |
. . . . . . . . . . . . . . . 16
     
          
  
                                  |
54 | 53 | ffvelrnda 6022 |
. . . . . . . . . . . . . . 15
               
 
                                      |
55 | 34, 54 | sseldd 3433 |
. . . . . . . . . . . . . 14
               
 
                                   |
56 | | simprl 764 |
. . . . . . . . . . . . . . 15
                |
57 | 56 | ad2antrr 732 |
. . . . . . . . . . . . . 14
               
 
            |
58 | 55, 57 | ifclda 3913 |
. . . . . . . . . . . . 13
     
          
              
                        |
59 | 58 | ralrimivva 2809 |
. . . . . . . . . . . 12
             
                                        |
60 | | eqid 2451 |
. . . . . . . . . . . . 13
                
                                                              |
61 | 60 | fmpt2 6860 |
. . . . . . . . . . . 12
 
                                                                                      |
62 | 59, 61 | sylib 200 |
. . . . . . . . . . 11
              
                                              |
63 | | eluni 4201 |
. . . . . . . . . . . . 13
 
      |
64 | | simplrr 771 |
. . . . . . . . . . . . . . . . 17
     
                 |
65 | | simprr 766 |
. . . . . . . . . . . . . . . . 17
     
             |
66 | | foelrn 6041 |
. . . . . . . . . . . . . . . . 17
     

       |
67 | 64, 65, 66 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
     
                  |
68 | | simprrl 774 |
. . . . . . . . . . . . . . . . . . . 20
     
           
      
  |
69 | | ordom 6701 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
70 | | simpll2 1048 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
           
      
  |
71 | | simplrr 771 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
           
      
      |
72 | 71, 28 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
           
      
      |
73 | 72, 68 | ffvelrnd 6023 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
           
      
      |
74 | 70, 73 | sseldd 3433 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
           
      
      |
75 | | ficardom 8395 |
. . . . . . . . . . . . . . . . . . . . . . 23
               |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
     
           
      
          |
77 | | ordelss 5439 |
. . . . . . . . . . . . . . . . . . . . . 22
                     |
78 | 69, 76, 77 | sylancr 669 |
. . . . . . . . . . . . . . . . . . . . 21
     
           
      
          |
79 | | elssuni 4227 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
            |
80 | 73, 79 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
           
      
       |
81 | | simpll3 1049 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
           
      
   |
82 | | soss 4773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      

       |
83 | 80, 81, 82 | sylc 62 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
           
      
      |
84 | | finnisoeu 8544 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                             |
85 | 83, 74, 84 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
           
      
                  |
86 | | iotacl 5569 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                
  
                                   |
87 | 85, 86 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
           
      
  
                                   |
88 | | iotaex 5563 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                    |
89 | | isoeq1 6210 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                   
                                                     |
90 | | isoeq1 6210 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
              
                  |
91 | 90 | cbvabv 2575 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26

                                  |
92 | 88, 89, 91 | elab2 3188 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                    
                                  
                 |
93 | 87, 92 | sylib 200 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
           
      
  
                                 |
94 | | isof1o 6216 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                                                        |
95 | 93, 94 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
           
      
  
                                  |
96 | | f1ocnv 5826 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                   
                                      |
97 | | f1of 5814 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
                                                                      |
98 | 95, 96, 97 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . 22
     
           
      
                                      |
99 | | simprll 772 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
           
      
  |
100 | | simprrr 775 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
           
      
      |
101 | 99, 100 | eleqtrd 2531 |
. . . . . . . . . . . . . . . . . . . . . 22
     
           
      
      |
102 | 98, 101 | ffvelrnd 6023 |
. . . . . . . . . . . . . . . . . . . . 21
     
           
      
                                  |
103 | 78, 102 | sseldd 3433 |
. . . . . . . . . . . . . . . . . . . 20
     
           
      
                          |
104 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           |
105 | 104 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                   |
106 | 105 | eleq2d 2514 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         
           |
107 | | isoeq4 6213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                
               
                  |
108 | 105, 107 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
              
                  |
109 | | isoeq5 6214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
         
              
                  |
110 | 104, 109 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
              
                  |
111 | 108, 110 | bitrd 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
              
                  |
112 | 111 | iotabidv 5567 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                         |
113 | 112 | fveq1d 5867 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                           
                     |
114 | 106, 113 | ifbieq1d 3904 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                                                           |
115 | | eleq1 2517 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                 
                                   |
116 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                                   
                      
                      |
117 | 115, 116 | ifbieq1d 3904 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                                                   
                                                                               |
118 | | fvex 5875 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                                |
119 | | vex 3048 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
120 | 118, 119 | ifex 3949 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                      
                      
                       |
121 | 114, 117,
60, 120 | ovmpt2 6432 |
. . . . . . . . . . . . . . . . . . . . . 22
                                             
                                                                                                             
                        |
122 | 68, 103, 121 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . 21
     
           
      
   
                                                                                                                            
                        |
123 | 102 | iftrued 3889 |
. . . . . . . . . . . . . . . . . . . . 21
     
           
      
                                      
                      
                                                                       |
124 | | f1ocnvfv2 6176 |
. . . . . . . . . . . . . . . . . . . . . 22
    
                               
                                                      |
125 | 95, 101, 124 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . 21
     
           
      
                                                 |
126 | 122, 123,
125 | 3eqtrrd 2490 |
. . . . . . . . . . . . . . . . . . . 20
     
           
      
                  
                                                  |
127 | | rspceov 6329 |
. . . . . . . . . . . . . . . . . . . 20
                                                                                              
                                              |
128 | 68, 103, 126, 127 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . 19
     
           
      
                                               |
129 | 128 | expr 620 |
. . . . . . . . . . . . . . . . . 18
     
                                                                  |
130 | 129 | expd 438 |
. . . . . . . . . . . . . . . . 17
     
                 
                                                |
131 | 130 | rexlimdv 2877 |
. . . . . . . . . . . . . . . 16
     
            
                                                    |
132 | 67, 131 | mpd 15 |
. . . . . . . . . . . . . . 15
     
                                                          |
133 | 132 | ex 436 |
. . . . . . . . . . . . . 14
                                                                |
134 | 133 | exlimdv 1779 |
. . . . . . . . . . . . 13
                
                                                 |
135 | 63, 134 | syl5bi 221 |
. . . . . . . . . . . 12
                                                               |
136 | 135 | ralrimiv 2800 |
. . . . . . . . . . 11
             
  
                                              |
137 | | foov 6443 |
. . . . . . . . . . 11
                                              
                                               
  
                                               |
138 | 62, 136, 137 | sylanbrc 670 |
. . . . . . . . . 10
              
                                              |
139 | | fodomnum 8488 |
. . . . . . . . . 10
  
                                                     |
140 | 26, 138, 139 | mpsyl 65 |
. . . . . . . . 9
             
    |
141 | | xpomen 8446 |
. . . . . . . . 9
   |
142 | | domentr 7628 |
. . . . . . . . 9
       
   |
143 | 140, 141,
142 | sylancl 668 |
. . . . . . . 8
             
  |
144 | 143 | expr 620 |
. . . . . . 7
    
      
    |
145 | 144 | exlimdv 1779 |
. . . . . 6
    
            |
146 | 21, 145 | mpd 15 |
. . . . 5
    
     |
147 | 146 | expcom 437 |
. . . 4
     
    |
148 | 147 | exlimiv 1776 |
. . 3
           |
149 | 6, 148 | sylbi 199 |
. 2
 
 
      |
150 | 5, 149 | pm2.61ine 2707 |
1
 
     |