Step | Hyp | Ref
| Expression |
1 | | nn0suc 6736 |
. . . 4
 

   |
2 | | simp1 1030 |
. . . . . 6
  


  |
3 | 2 | necon2bi 2673 |
. . . . 5

 

   |
4 | | vex 3034 |
. . . . . . . . . . . 12
 |
5 | 4 | sucid 5509 |
. . . . . . . . . . 11
 |
6 | | eleq2 2538 |
. . . . . . . . . . 11
     |
7 | 5, 6 | mpbiri 241 |
. . . . . . . . . 10
   |
8 | 7 | adantl 473 |
. . . . . . . . 9
 
   |
9 | | breq1 4398 |
. . . . . . . . . . . 12
 
   |
10 | 9 | rexbidv 2892 |
. . . . . . . . . . 11
  

   |
11 | | breq2 4399 |
. . . . . . . . . . . 12
 
   |
12 | 11 | cbvrexv 3006 |
. . . . . . . . . . 11
 
   |
13 | 10, 12 | syl6bb 269 |
. . . . . . . . . 10
  

   |
14 | 13 | rspcv 3132 |
. . . . . . . . 9
  


   |
15 | 8, 14 | syl 17 |
. . . . . . . 8
 
  

    |
16 | | eleq2 2538 |
. . . . . . . . . . . . . . 15
     |
17 | 16 | biimpa 492 |
. . . . . . . . . . . . . 14
 

  |
18 | 17 | 3ad2antl2 1193 |
. . . . . . . . . . . . 13
    

   |
19 | | nnon 6717 |
. . . . . . . . . . . . . . . . . 18
   |
20 | | suceloni 6659 |
. . . . . . . . . . . . . . . . . 18

  |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . . . . . 17

  |
22 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . 18
     |
23 | 22 | biimparc 495 |
. . . . . . . . . . . . . . . . 17
  
  |
24 | 21, 23 | sylan 479 |
. . . . . . . . . . . . . . . 16
 
   |
25 | 24 | 3adant3 1050 |
. . . . . . . . . . . . . . 15
 
 
   |
26 | | onelon 5455 |
. . . . . . . . . . . . . . 15
 
   |
27 | 25, 26 | sylan 479 |
. . . . . . . . . . . . . 14
    

   |
28 | | simpl1 1033 |
. . . . . . . . . . . . . . 15
    

   |
29 | 28, 19 | syl 17 |
. . . . . . . . . . . . . 14
    

   |
30 | | onsssuc 5517 |
. . . . . . . . . . . . . 14
 
     |
31 | 27, 29, 30 | syl2anc 673 |
. . . . . . . . . . . . 13
    

     |
32 | 18, 31 | mpbird 240 |
. . . . . . . . . . . 12
    


  |
33 | | ssdomg 7633 |
. . . . . . . . . . . 12
 
   |
34 | 4, 32, 33 | mpsyl 64 |
. . . . . . . . . . 11
    

   |
35 | | domnsym 7716 |
. . . . . . . . . . 11

  |
36 | 34, 35 | syl 17 |
. . . . . . . . . 10
    

   |
37 | 36 | nrexdv 2842 |
. . . . . . . . 9
 
 
    |
38 | 37 | 3expia 1233 |
. . . . . . . 8
 
  


   |
39 | 15, 38 | pm2.65d 180 |
. . . . . . 7
 



  |
40 | 39 | intn3an3d 1409 |
. . . . . 6
 

 

   |
41 | 40 | rexlimiva 2868 |
. . . . 5
  


   |
42 | 3, 41 | jaoi 386 |
. . . 4
  
  

   |
43 | 1, 42 | syl 17 |
. . 3
 


   |
44 | 43 | con2i 124 |
. 2
  


  |
45 | | ordom 6720 |
. . 3
 |
46 | | eloni 5440 |
. . . 4
   |
47 | 46 | 3ad2ant2 1052 |
. . 3
  


  |
48 | | ordtri1 5463 |
. . 3
  

   |
49 | 45, 47, 48 | sylancr 676 |
. 2
  



   |
50 | 44, 49 | mpbird 240 |
1
  


  |