Step | Hyp | Ref
| Expression |
1 | | isomnimap 6957 |
. 2
 
Omni                    |
2 | | fveq1 5372 |
. . . . . . . . 9
                 |
3 | 2 | eqeq1d 2121 |
. . . . . . . 8
        
  
       |
4 | 3 | rexbidv 2410 |
. . . . . . 7
     
   

  
       |
5 | 2 | eqeq1d 2121 |
. . . . . . . 8
        
  
       |
6 | 5 | ralbidv 2409 |
. . . . . . 7
     
   

  
       |
7 | 4, 6 | orbi12d 765 |
. . . . . 6
                                      |
8 | | simplr 502 |
. . . . . 6
                               
            |
9 | | isomninnlem.g |
. . . . . . . . . . . . 13
frec        |
10 | 9 | frechashgf1o 10088 |
. . . . . . . . . . . 12
     |
11 | | f1ocnv 5334 |
. . . . . . . . . . . 12
    
       |
12 | | f1of 5321 |
. . . . . . . . . . . 12
     
       |
13 | 10, 11, 12 | mp2b 8 |
. . . . . . . . . . 11
      |
14 | | 0nn0 8890 |
. . . . . . . . . . . 12
 |
15 | | 1nn0 8891 |
. . . . . . . . . . . 12
 |
16 | | prssi 3642 |
. . . . . . . . . . . 12
 
   
  |
17 | 14, 15, 16 | mp2an 420 |
. . . . . . . . . . 11
    |
18 | | fssres 5254 |
. . . . . . . . . . 11
            
             |
19 | 13, 17, 18 | mp2an 420 |
. . . . . . . . . 10
 
            |
20 | | ffn 5228 |
. . . . . . . . . 10
  
            
         |
21 | 19, 20 | ax-mp 7 |
. . . . . . . . 9
 
        |
22 | | fvres 5397 |
. . . . . . . . . . 11
                     |
23 | | elpri 3514 |
. . . . . . . . . . . 12
        |
24 | | fveq2 5373 |
. . . . . . . . . . . . . 14
             |
25 | | 0zd 8964 |
. . . . . . . . . . . . . . . . . 18
  |
26 | 25, 9 | frec2uz0d 10059 |
. . . . . . . . . . . . . . . . 17
      |
27 | 26 | mptru 1321 |
. . . . . . . . . . . . . . . 16
     |
28 | | peano1 4466 |
. . . . . . . . . . . . . . . . 17
 |
29 | | f1ocnvfv 5632 |
. . . . . . . . . . . . . . . . 17
                    |
30 | 10, 28, 29 | mp2an 420 |
. . . . . . . . . . . . . . . 16
    
       |
31 | 27, 30 | ax-mp 7 |
. . . . . . . . . . . . . . 15
      |
32 | | 0lt2o 6290 |
. . . . . . . . . . . . . . 15
 |
33 | 31, 32 | eqeltri 2185 |
. . . . . . . . . . . . . 14
      |
34 | 24, 33 | syl6eqel 2203 |
. . . . . . . . . . . . 13
        |
35 | | fveq2 5373 |
. . . . . . . . . . . . . 14
             |
36 | | df-1o 6265 |
. . . . . . . . . . . . . . . . . 18
 |
37 | 36 | fveq2i 5376 |
. . . . . . . . . . . . . . . . 17
         |
38 | 28 | a1i 9 |
. . . . . . . . . . . . . . . . . . 19
  |
39 | 25, 9, 38 | frec2uzsucd 10061 |
. . . . . . . . . . . . . . . . . 18
            |
40 | 39 | mptru 1321 |
. . . . . . . . . . . . . . . . 17
  
        |
41 | 27 | oveq1i 5736 |
. . . . . . . . . . . . . . . . . 18
         |
42 | | 0p1e1 8738 |
. . . . . . . . . . . . . . . . . 18
   |
43 | 41, 42 | eqtri 2133 |
. . . . . . . . . . . . . . . . 17
       |
44 | 37, 40, 43 | 3eqtri 2137 |
. . . . . . . . . . . . . . . 16
     |
45 | | 1onn 6368 |
. . . . . . . . . . . . . . . . 17
 |
46 | | f1ocnvfv 5632 |
. . . . . . . . . . . . . . . . 17
      
             |
47 | 10, 45, 46 | mp2an 420 |
. . . . . . . . . . . . . . . 16
            |
48 | 44, 47 | ax-mp 7 |
. . . . . . . . . . . . . . 15
      |
49 | | 1lt2o 6291 |
. . . . . . . . . . . . . . 15
 |
50 | 48, 49 | eqeltri 2185 |
. . . . . . . . . . . . . 14
      |
51 | 35, 50 | syl6eqel 2203 |
. . . . . . . . . . . . 13
        |
52 | 34, 51 | jaoi 688 |
. . . . . . . . . . . 12
          |
53 | 23, 52 | syl 14 |
. . . . . . . . . . 11
           |
54 | 22, 53 | eqeltrd 2189 |
. . . . . . . . . 10
                |
55 | 54 | rgen 2457 |
. . . . . . . . 9
      
        |
56 | | ffnfv 5530 |
. . . . . . . . 9
  
          
  
       
                |
57 | 21, 55, 56 | mpbir2an 907 |
. . . . . . . 8
 
            |
58 | | elmapi 6516 |
. . . . . . . . 9
               |
59 | 58 | adantl 273 |
. . . . . . . 8
                                   |
60 | | fco2 5245 |
. . . . . . . 8
                                |
61 | 57, 59, 60 | sylancr 408 |
. . . . . . 7
                           
       |
62 | | 2onn 6369 |
. . . . . . . . 9
 |
63 | 62 | a1i 9 |
. . . . . . . 8
                            |
64 | | simpll 501 |
. . . . . . . 8
                            |
65 | 63, 64 | elmapd 6508 |
. . . . . . 7
                                          |
66 | 61, 65 | mpbird 166 |
. . . . . 6
                           
     |
67 | 7, 8, 66 | rspcdva 2763 |
. . . . 5
                           
       
          |
68 | | nfv 1489 |
. . . . . . . . 9

 |
69 | | nfcv 2253 |
. . . . . . . . . 10
     |
70 | | nfre1 2448 |
. . . . . . . . . . 11
  
     |
71 | | nfra1 2438 |
. . . . . . . . . . 11
  
     |
72 | 70, 71 | nfor 1534 |
. . . . . . . . . 10
               |
73 | 69, 72 | nfralxy 2443 |
. . . . . . . . 9
  
         
      |
74 | 68, 73 | nfan 1525 |
. . . . . . . 8
                     |
75 | | nfv 1489 |
. . . . . . . 8

      |
76 | 74, 75 | nfan 1525 |
. . . . . . 7
         
                  |
77 | | simplr 502 |
. . . . . . . . . . . . . 14
         
                         |
78 | 77, 58 | syl 14 |
. . . . . . . . . . . . 13
         
                           |
79 | | simpr 109 |
. . . . . . . . . . . . 13
         
                    |
80 | 78, 79 | ffvelrnd 5508 |
. . . . . . . . . . . 12
         
                           |
81 | 17, 80 | sseldi 3059 |
. . . . . . . . . . 11
         
                        |
82 | | f1ocnvfv2 5631 |
. . . . . . . . . . 11
                              |
83 | 10, 81, 82 | sylancr 408 |
. . . . . . . . . 10
         
                                     |
84 | 83 | adantr 272 |
. . . . . . . . 9
     
        

                                        |
85 | | fvco3 5444 |
. . . . . . . . . . . . . 14
        
                   |
86 | 78, 85 | sylancom 414 |
. . . . . . . . . . . . 13
         
                                    |
87 | 86 | eqeq1d 2121 |
. . . . . . . . . . . 12
         
                         
            |
88 | 87 | biimpa 292 |
. . . . . . . . . . 11
     
        

                                |
89 | 88 | fveq2d 5377 |
. . . . . . . . . 10
     
        

                                        |
90 | 89, 27 | syl6eq 2161 |
. . . . . . . . 9
     
        

                                    |
91 | 84, 90 | eqtr3d 2147 |
. . . . . . . 8
     
        

                           |
92 | 91 | exp31 359 |
. . . . . . 7
                                           |
93 | 76, 92 | reximdai 2502 |
. . . . . 6
                           
       
       |
94 | 83 | adantr 272 |
. . . . . . . . 9
     
        

                                        |
95 | 86 | adantr 272 |
. . . . . . . . . . . 12
     
        

                                       |
96 | | simpr 109 |
. . . . . . . . . . . 12
     
        

                              |
97 | 95, 96 | eqtr3d 2147 |
. . . . . . . . . . 11
     
        

                                |
98 | 97 | fveq2d 5377 |
. . . . . . . . . 10
     
        

                                        |
99 | 98, 44 | syl6eq 2161 |
. . . . . . . . 9
     
        

                                    |
100 | 94, 99 | eqtr3d 2147 |
. . . . . . . 8
     
        

                           |
101 | 100 | ex 114 |
. . . . . . 7
         
                                 |
102 | 76, 101 | ralimdaa 2470 |
. . . . . 6
                           
               |
103 | 93, 102 | orim12d 758 |
. . . . 5
                                              
             |
104 | 67, 103 | mpd 13 |
. . . 4
                           
            |
105 | 104 | ralrimiva 2477 |
. . 3
            
      
                    |
106 | | fveq1 5372 |
. . . . . . . . 9
               |
107 | 106 | eqeq1d 2121 |
. . . . . . . 8
                 |
108 | 107 | rexbidv 2410 |
. . . . . . 7
    
    
         |
109 | 106 | eqeq1d 2121 |
. . . . . . . 8
                 |
110 | 109 | ralbidv 2409 |
. . . . . . 7
    
    
         |
111 | 108, 110 | orbi12d 765 |
. . . . . 6
                 
 
               |
112 | | simplr 502 |
. . . . . 6
                                  
            |
113 | | f1of 5321 |
. . . . . . . . . . . 12
    
      |
114 | 10, 113 | ax-mp 7 |
. . . . . . . . . . 11
     |
115 | | omelon 4480 |
. . . . . . . . . . . . 13
 |
116 | 115 | onelssi 4309 |
. . . . . . . . . . . 12
   |
117 | 62, 116 | ax-mp 7 |
. . . . . . . . . . 11
 |
118 | | fssres 5254 |
. . . . . . . . . . 11
               |
119 | 114, 117,
118 | mp2an 420 |
. . . . . . . . . 10
       |
120 | | ffn 5228 |
. . . . . . . . . 10
 
    
    |
121 | 119, 120 | ax-mp 7 |
. . . . . . . . 9
   |
122 | | fvres 5397 |
. . . . . . . . . . 11
             |
123 | | elpri 3514 |
. . . . . . . . . . . . 13
        |
124 | | df2o3 6279 |
. . . . . . . . . . . . 13
    |
125 | 123, 124 | eleq2s 2207 |
. . . . . . . . . . . 12
     |
126 | | fveq2 5373 |
. . . . . . . . . . . . . 14

          |
127 | | c0ex 7678 |
. . . . . . . . . . . . . . . 16
 |
128 | 127 | prid1 3593 |
. . . . . . . . . . . . . . 15
    |
129 | 27, 128 | eqeltri 2185 |
. . . . . . . . . . . . . 14
        |
130 | 126, 129 | syl6eqel 2203 |
. . . . . . . . . . . . 13

         |
131 | | fveq2 5373 |
. . . . . . . . . . . . . 14
           |
132 | | 1ex 7679 |
. . . . . . . . . . . . . . . 16
 |
133 | 132 | prid2 3594 |
. . . . . . . . . . . . . . 15
    |
134 | 44, 133 | eqeltri 2185 |
. . . . . . . . . . . . . 14
        |
135 | 131, 134 | syl6eqel 2203 |
. . . . . . . . . . . . 13
          |
136 | 130, 135 | jaoi 688 |
. . . . . . . . . . . 12
            |
137 | 125, 136 | syl 14 |
. . . . . . . . . . 11
          |
138 | 122, 137 | eqeltrd 2189 |
. . . . . . . . . 10
            |
139 | 138 | rgen 2457 |
. . . . . . . . 9
           |
140 | | ffnfv 5530 |
. . . . . . . . 9
 
       
                |
141 | 121, 139,
140 | mpbir2an 907 |
. . . . . . . 8
          |
142 | | elmapi 6516 |
. . . . . . . . 9
         |
143 | 142 | adantl 273 |
. . . . . . . 8
                                |
144 | | fco2 5245 |
. . . . . . . 8
                           |
145 | 141, 143,
144 | sylancr 408 |
. . . . . . 7
                          
          |
146 | | prexg 4091 |
. . . . . . . . . 10
 
      |
147 | 14, 15, 146 | mp2an 420 |
. . . . . . . . 9
    |
148 | 147 | a1i 9 |
. . . . . . . 8
                               |
149 | | simpll 501 |
. . . . . . . 8
                            |
150 | 148, 149 | elmapd 6508 |
. . . . . . 7
                                 
            |
151 | 145, 150 | mpbird 166 |
. . . . . 6
                          
        |
152 | 111, 112,
151 | rspcdva 2763 |
. . . . 5
                           
                |
153 | | nfcv 2253 |
. . . . . . . . . 10
        |
154 | | nfre1 2448 |
. . . . . . . . . . 11
  
     |
155 | | nfra1 2438 |
. . . . . . . . . . 11
  
     |
156 | 154, 155 | nfor 1534 |
. . . . . . . . . 10
               |
157 | 153, 156 | nfralxy 2443 |
. . . . . . . . 9
  
                   |
158 | 68, 157 | nfan 1525 |
. . . . . . . 8
                        |
159 | | nfv 1489 |
. . . . . . . 8

   |
160 | 158, 159 | nfan 1525 |
. . . . . . 7
            
               |
161 | 143 | adantr 272 |
. . . . . . . . . . . . 13
            
                     |
162 | 117 | a1i 9 |
. . . . . . . . . . . . 13
            
                 |
163 | 161, 162 | fssd 5241 |
. . . . . . . . . . . 12
            
                     |
164 | | simpr 109 |
. . . . . . . . . . . 12
            
                 |
165 | 163, 164 | ffvelrnd 5508 |
. . . . . . . . . . 11
            
                     |
166 | | f1ocnvfv1 5630 |
. . . . . . . . . . 11
                              |
167 | 10, 165, 166 | sylancr 408 |
. . . . . . . . . 10
            
                                  |
168 | 167 | adantr 272 |
. . . . . . . . 9
     
                                                 |
169 | | fvco3 5444 |
. . . . . . . . . . . . . 14
     
                 |
170 | 161, 169 | sylancom 414 |
. . . . . . . . . . . . 13
            
                               |
171 | 170 | eqeq1d 2121 |
. . . . . . . . . . . 12
            
                                 |
172 | 171 | biimpa 292 |
. . . . . . . . . . 11
     
                                        |
173 | 172 | fveq2d 5377 |
. . . . . . . . . 10
     
                                                  |
174 | 173, 31 | syl6eq 2161 |
. . . . . . . . 9
     
                                             |
175 | 168, 174 | eqtr3d 2147 |
. . . . . . . 8
     
                                    |
176 | 175 | exp31 359 |
. . . . . . 7
                                          |
177 | 160, 176 | reximdai 2502 |
. . . . . 6
                           
      
       |
178 | 167 | adantr 272 |
. . . . . . . . 9
     
                                                 |
179 | 170 | eqeq1d 2121 |
. . . . . . . . . . . 12
            
                                 |
180 | 179 | biimpa 292 |
. . . . . . . . . . 11
     
                                        |
181 | 180 | fveq2d 5377 |
. . . . . . . . . 10
     
                                                  |
182 | 181, 48 | syl6eq 2161 |
. . . . . . . . 9
     
                                             |
183 | 178, 182 | eqtr3d 2147 |
. . . . . . . 8
     
                                    |
184 | 183 | ex 114 |
. . . . . . 7
            
                             |
185 | 160, 184 | ralimdaa 2470 |
. . . . . 6
                           
      
       |
186 | 177, 185 | orim12d 758 |
. . . . 5
                                          
 
    
        |
187 | 152, 186 | mpd 13 |
. . . 4
                           
    
       |
188 | 187 | ralrimiva 2477 |
. . 3
                     
     
            |
189 | 105, 188 | impbida 568 |
. 2
  
         
    
        
             |
190 | 1, 189 | bitrd 187 |
1
 
Omni                       |