Step | Hyp | Ref
| Expression |
1 | | elnc 6126 |
. . 3
 Nc 
     |
2 | | bren 6031 |
. . . . 5
            |
3 | | f1ocnv 5300 |
. . . . . . 7
                |
4 | | imaundi 5040 |
. . . . . . . . . . 11
                    |
5 | | imadmrn 5009 |
. . . . . . . . . . . . 13
     
  |
6 | 5 | a1i 10 |
. . . . . . . . . . . 12
                 |
7 | | f1odm 5291 |
. . . . . . . . . . . . 13
             |
8 | 7 | imaeq2d 4943 |
. . . . . . . . . . . 12
                  
    |
9 | | f1ofo 5294 |
. . . . . . . . . . . . 13
                 |
10 | | forn 5273 |
. . . . . . . . . . . . 13
           |
11 | 9, 10 | syl 15 |
. . . . . . . . . . . 12
           |
12 | 6, 8, 11 | 3eqtr3d 2393 |
. . . . . . . . . . 11
            
 
  |
13 | 4, 12 | syl5eqr 2399 |
. . . . . . . . . 10
                      |
14 | 13 | adantl 452 |
. . . . . . . . 9
   
             
        |
15 | | f1of1 5287 |
. . . . . . . . . . . . . 14
                 |
16 | | ssun1 3427 |
. . . . . . . . . . . . . 14

  |
17 | | f1ores 5301 |
. . . . . . . . . . . . . 14
         
 
 
            |
18 | 15, 16, 17 | sylancl 643 |
. . . . . . . . . . . . 13
                      |
19 | | f1ocnv 5300 |
. . . . . . . . . . . . 13
                            |
20 | | vex 2863 |
. . . . . . . . . . . . . . . . 17
 |
21 | 20 | cnvex 5103 |
. . . . . . . . . . . . . . . 16
  |
22 | | ncdisjun.1 |
. . . . . . . . . . . . . . . 16
 |
23 | 21, 22 | resex 5118 |
. . . . . . . . . . . . . . 15
 
  |
24 | 23 | cnvex 5103 |
. . . . . . . . . . . . . 14
  
  |
25 | 24 | f1oen 6034 |
. . . . . . . . . . . . 13
                     |
26 | 18, 19, 25 | 3syl 18 |
. . . . . . . . . . . 12
            
  |
27 | | elnc 6126 |
. . . . . . . . . . . 12
     
Nc        |
28 | 26, 27 | sylibr 203 |
. . . . . . . . . . 11
            
Nc   |
29 | 28 | adantl 452 |
. . . . . . . . . 10
   
            
Nc   |
30 | | ssun2 3428 |
. . . . . . . . . . . . . 14

  |
31 | | f1ores 5301 |
. . . . . . . . . . . . . 14
         
 
 
            |
32 | 15, 30, 31 | sylancl 643 |
. . . . . . . . . . . . 13
                      |
33 | | f1ocnv 5300 |
. . . . . . . . . . . . 13
                            |
34 | | ncdisjun.2 |
. . . . . . . . . . . . . . . 16
 |
35 | 21, 34 | resex 5118 |
. . . . . . . . . . . . . . 15
 
  |
36 | 35 | cnvex 5103 |
. . . . . . . . . . . . . 14
  
  |
37 | 36 | f1oen 6034 |
. . . . . . . . . . . . 13
                     |
38 | 32, 33, 37 | 3syl 18 |
. . . . . . . . . . . 12
            
  |
39 | 38 | adantl 452 |
. . . . . . . . . . 11
   
               |
40 | | elnc 6126 |
. . . . . . . . . . 11
     
Nc        |
41 | 39, 40 | sylibr 203 |
. . . . . . . . . 10
   
            
Nc   |
42 | | df-f1 4793 |
. . . . . . . . . . . . . 14
                     |
43 | 42 | simprbi 450 |
. . . . . . . . . . . . 13
            |
44 | | imain 5173 |
. . . . . . . . . . . . 13
                        |
45 | 15, 43, 44 | 3syl 18 |
. . . . . . . . . . . 12
            
 
              |
46 | 45 | adantl 452 |
. . . . . . . . . . 11
   
                             |
47 | | imaeq2 4939 |
. . . . . . . . . . . . 13
  
              |
48 | | ima0 5014 |
. . . . . . . . . . . . 13
      |
49 | 47, 48 | syl6eq 2401 |
. . . . . . . . . . . 12
  
         |
50 | 49 | adantr 451 |
. . . . . . . . . . 11
   
                 |
51 | 46, 50 | eqtr3d 2387 |
. . . . . . . . . 10
   
             
        |
52 | | eladdci 4400 |
. . . . . . . . . 10
      
Nc      Nc                          Nc Nc    |
53 | 29, 41, 51, 52 | syl3anc 1182 |
. . . . . . . . 9
   
             
      Nc Nc    |
54 | 14, 53 | eqeltrrd 2428 |
. . . . . . . 8
   
       
Nc Nc    |
55 | 54 | ex 423 |
. . . . . . 7
  
        Nc Nc     |
56 | 3, 55 | syl5 28 |
. . . . . 6
  
      
Nc Nc     |
57 | 56 | exlimdv 1636 |
. . . . 5
  
 
      Nc Nc     |
58 | 2, 57 | syl5bi 208 |
. . . 4
  
  
Nc Nc     |
59 | | eladdc 4399 |
. . . . 5
 Nc Nc   Nc  
Nc          |
60 | | simplrl 736 |
. . . . . . . . . 10
    

Nc Nc      Nc   |
61 | | elnc 6126 |
. . . . . . . . . 10
 Nc   |
62 | 60, 61 | sylib 188 |
. . . . . . . . 9
    

Nc Nc        |
63 | | simplrr 737 |
. . . . . . . . . 10
    

Nc Nc      Nc   |
64 | | elnc 6126 |
. . . . . . . . . 10
 Nc   |
65 | 63, 64 | sylib 188 |
. . . . . . . . 9
    

Nc Nc        |
66 | | simpr 447 |
. . . . . . . . 9
    

Nc Nc       
  |
67 | | simpll 730 |
. . . . . . . . 9
    

Nc Nc       
  |
68 | | unen 6049 |
. . . . . . . . 9
  
   
      
   |
69 | 62, 65, 66, 67, 68 | syl22anc 1183 |
. . . . . . . 8
    

Nc Nc       
    |
70 | | breq1 4643 |
. . . . . . . 8
  
  
       |
71 | 69, 70 | syl5ibrcom 213 |
. . . . . . 7
    

Nc Nc              |
72 | 71 | expimpd 586 |
. . . . . 6
   

Nc Nc      
  
     |
73 | 72 | rexlimdvva 2746 |
. . . . 5
  
 
Nc   Nc    
  
     |
74 | 59, 73 | syl5bi 208 |
. . . 4
  

Nc Nc       |
75 | 58, 74 | impbid 183 |
. . 3
  
  
Nc Nc     |
76 | 1, 75 | syl5bb 248 |
. 2
  

Nc   Nc Nc     |
77 | 76 | eqrdv 2351 |
1
  
Nc  
Nc Nc    |