Step | Hyp | Ref
| Expression |
1 | | breq2 4399 |
. . . 4

  
     |
2 | 1 | rexbidv 2892 |
. . 3

   

     |
3 | | breq2 4399 |
. . . 4
   
     |
4 | 3 | rexbidv 2892 |
. . 3
  
 

     |
5 | | breq2 4399 |
. . . 4
     
   |
6 | 5 | rexbidv 2892 |
. . 3
       
   |
7 | | ordom 6720 |
. . . . . 6
 |
8 | 7 | a1i 11 |
. . . . 5
 
   |
9 | | simpl 464 |
. . . . 5
 

  |
10 | | 0fin 7817 |
. . . . . . . 8
 |
11 | | eleq1 2537 |
. . . . . . . 8


   |
12 | 10, 11 | mpbiri 241 |
. . . . . . 7

  |
13 | 12 | necon3bi 2669 |
. . . . . 6
   |
14 | 13 | adantl 473 |
. . . . 5
 
   |
15 | | tz7.5 5451 |
. . . . 5
 


    |
16 | 8, 9, 14, 15 | syl3anc 1292 |
. . . 4
 
  
   |
17 | | en0 7650 |
. . . . . 6
       |
18 | | incom 3616 |
. . . . . . 7
     |
19 | 18 | eqeq1i 2476 |
. . . . . 6
  
    |
20 | 17, 19 | bitri 257 |
. . . . 5
       |
21 | 20 | rexbii 2881 |
. . . 4
     
   |
22 | 16, 21 | sylibr 217 |
. . 3
 
   
  |
23 | | simplrl 778 |
. . . . . . . . . . 11
   
    
 
  |
24 | | omsson 6715 |
. . . . . . . . . . 11
 |
25 | 23, 24 | syl6ss 3430 |
. . . . . . . . . 10
   
    
 
  |
26 | 25 | ssdifssd 3560 |
. . . . . . . . 9
   
    
 
    |
27 | | simplr 770 |
. . . . . . . . . . . 12
  
 
  |
28 | | ssel2 3413 |
. . . . . . . . . . . . . . 15
 
   |
29 | | onfin2 7782 |
. . . . . . . . . . . . . . . . 17

  |
30 | | inss2 3644 |
. . . . . . . . . . . . . . . . 17
   |
31 | 29, 30 | eqsstri 3448 |
. . . . . . . . . . . . . . . 16
 |
32 | | peano2 6732 |
. . . . . . . . . . . . . . . 16

  |
33 | 31, 32 | sseldi 3416 |
. . . . . . . . . . . . . . 15

  |
34 | 28, 33 | syl 17 |
. . . . . . . . . . . . . 14
 

  |
35 | 34 | adantlr 729 |
. . . . . . . . . . . . 13
  
 
  |
36 | | ssfi 7810 |
. . . . . . . . . . . . . 14
 
   |
37 | 36 | ex 441 |
. . . . . . . . . . . . 13
 
   |
38 | 35, 37 | syl 17 |
. . . . . . . . . . . 12
  
 
    |
39 | 27, 38 | mtod 182 |
. . . . . . . . . . 11
  
 
  |
40 | | ssdif0 3741 |
. . . . . . . . . . . 12

    |
41 | 40 | necon3bbii 2690 |
. . . . . . . . . . 11

    |
42 | 39, 41 | sylib 201 |
. . . . . . . . . 10
  
 
    |
43 | 42 | ad2ant2lr 762 |
. . . . . . . . 9
   
    
 
    |
44 | | onint 6641 |
. . . . . . . . 9
              |
45 | 26, 43, 44 | syl2anc 673 |
. . . . . . . 8
   
    
 
 
     |
46 | 45 | eldifad 3402 |
. . . . . . 7
   
    
 
 
   |
47 | | simprr 774 |
. . . . . . . . 9
   
    
 
    |
48 | | vex 3034 |
. . . . . . . . . . 11
 |
49 | | vex 3034 |
. . . . . . . . . . 11
 |
50 | | en2sn 7667 |
. . . . . . . . . . 11
 
       |
51 | 48, 49, 50 | mp2an 686 |
. . . . . . . . . 10
     |
52 | 51 | a1i 11 |
. . . . . . . . 9
   
    
 
      |
53 | | simprl 772 |
. . . . . . . . . . . 12
   
    
 
  |
54 | 23, 53 | sseldd 3419 |
. . . . . . . . . . 11
   
    
 
  |
55 | | nnord 6719 |
. . . . . . . . . . 11
   |
56 | 54, 55 | syl 17 |
. . . . . . . . . 10
   
    
 
  |
57 | | ordirr 5448 |
. . . . . . . . . . . 12

  |
58 | | inss1 3643 |
. . . . . . . . . . . . 13
   |
59 | 58 | sseli 3414 |
. . . . . . . . . . . 12
     |
60 | 57, 59 | nsyl 125 |
. . . . . . . . . . 11

    |
61 | | disjsn 4023 |
. . . . . . . . . . 11
   
  
    |
62 | 60, 61 | sylibr 217 |
. . . . . . . . . 10

 
      |
63 | 56, 62 | syl 17 |
. . . . . . . . 9
   
    
 
 
      |
64 | | nnord 6719 |
. . . . . . . . . . . 12
   |
65 | | ordirr 5448 |
. . . . . . . . . . . 12

  |
66 | 64, 65 | syl 17 |
. . . . . . . . . . 11

  |
67 | | disjsn 4023 |
. . . . . . . . . . 11
    
  |
68 | 66, 67 | sylibr 217 |
. . . . . . . . . 10
 
     |
69 | 68 | ad2antrr 740 |
. . . . . . . . 9
   
    
 
      |
70 | | unen 7670 |
. . . . . . . . 9
                

                 |
71 | 47, 52, 63, 69, 70 | syl22anc 1293 |
. . . . . . . 8
   
    
 
 
          |
72 | | simprr 774 |
. . . . . . . . . . . . . . . 16
   
     

    |
73 | | simplrl 778 |
. . . . . . . . . . . . . . . . 17
   
     

    |
74 | 73, 24 | syl6ss 3430 |
. . . . . . . . . . . . . . . 16
   
     

    |
75 | | ordsuc 6660 |
. . . . . . . . . . . . . . . . . 18

  |
76 | 56, 75 | sylib 201 |
. . . . . . . . . . . . . . . . 17
   
    
 
  |
77 | 76 | adantrr 731 |
. . . . . . . . . . . . . . . 16
   
     

    |
78 | | simp2 1031 |
. . . . . . . . . . . . . . . . . . . . 21
     |
79 | 78 | ssdifssd 3560 |
. . . . . . . . . . . . . . . . . . . 20
       |
80 | | simpl1 1033 |
. . . . . . . . . . . . . . . . . . . . . 22
  

   |
81 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . . 22
  


  |
82 | 80, 81 | eldifd 3401 |
. . . . . . . . . . . . . . . . . . . . 21
  

     |
83 | 82 | ex 441 |
. . . . . . . . . . . . . . . . . . . 20
   
     |
84 | | onnmin 6649 |
. . . . . . . . . . . . . . . . . . . 20
    
 
     |
85 | 79, 83, 84 | syl6an 554 |
. . . . . . . . . . . . . . . . . . 19
   
      |
86 | 85 | con4d 108 |
. . . . . . . . . . . . . . . . . 18
          |
87 | 86 | imp 436 |
. . . . . . . . . . . . . . . . 17
  

 
 
  |
88 | | simp3 1032 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
89 | | ordsucss 6664 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
90 | 88, 89 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
       |
91 | 90 | imp 436 |
. . . . . . . . . . . . . . . . . . . 20
  


  |
92 | 91 | sscond 3559 |
. . . . . . . . . . . . . . . . . . 19
  

       |
93 | | intss 4247 |
. . . . . . . . . . . . . . . . . . 19
  
          |
94 | 92, 93 | syl 17 |
. . . . . . . . . . . . . . . . . 18
  

         |
95 | | simpl2 1034 |
. . . . . . . . . . . . . . . . . . 19
  

   |
96 | | ordelon 5454 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
97 | 88, 96 | sylan 479 |
. . . . . . . . . . . . . . . . . . 19
  

   |
98 | | onmindif 5519 |
. . . . . . . . . . . . . . . . . . 19
 
      |
99 | 95, 97, 98 | syl2anc 673 |
. . . . . . . . . . . . . . . . . 18
  

  
   |
100 | 94, 99 | sseldd 3419 |
. . . . . . . . . . . . . . . . 17
  

  
   |
101 | 87, 100 | impbida 850 |
. . . . . . . . . . . . . . . 16
          |
102 | 72, 74, 77, 101 | syl3anc 1292 |
. . . . . . . . . . . . . . 15
   
     

         |
103 | | df-suc 5436 |
. . . . . . . . . . . . . . . 16
     |
104 | 103 | eleq2i 2541 |
. . . . . . . . . . . . . . 15

      |
105 | 102, 104 | syl6bb 269 |
. . . . . . . . . . . . . 14
   
     

             |
106 | 105 | expr 626 |
. . . . . . . . . . . . 13
   
    
 

   
        |
107 | 106 | pm5.32rd 652 |
. . . . . . . . . . . 12
   
    
 
          
    |
108 | | elin 3608 |
. . . . . . . . . . . 12
     
       |
109 | | elin 3608 |
. . . . . . . . . . . 12
               |
110 | 107, 108,
109 | 3bitr4g 296 |
. . . . . . . . . . 11
   
    
 
   
 
         |
111 | 110 | eqrdv 2469 |
. . . . . . . . . 10
   
    
 
  

         |
112 | | indir 3682 |
. . . . . . . . . 10
               |
113 | 111, 112 | syl6eq 2521 |
. . . . . . . . 9
   
    
 
  

           |
114 | | snssi 4107 |
. . . . . . . . . . . 12
  
  |
115 | | df-ss 3404 |
. . . . . . . . . . . 12
           |
116 | 114, 115 | sylib 201 |
. . . . . . . . . . 11
         |
117 | 116 | uneq2d 3579 |
. . . . . . . . . 10
                 |
118 | 117 | ad2antrl 742 |
. . . . . . . . 9
   
    
 
 
              |
119 | 113, 118 | eqtrd 2505 |
. . . . . . . 8
   
    
 
  

         |
120 | | df-suc 5436 |
. . . . . . . . 9
     |
121 | 120 | a1i 11 |
. . . . . . . 8
   
    
 
      |
122 | 71, 119, 121 | 3brtr4d 4426 |
. . . . . . 7
   
    
 
  

   |
123 | | ineq1 3618 |
. . . . . . . . 9
  
     

   |
124 | 123 | breq1d 4405 |
. . . . . . . 8
  
      
     |
125 | 124 | rspcev 3136 |
. . . . . . 7
       
   
    |
126 | 46, 122, 125 | syl2anc 673 |
. . . . . 6
   
    
 

    |
127 | 126 | rexlimdvaa 2872 |
. . . . 5
  
   
 
  
   |
128 | | ineq1 3618 |
. . . . . . 7
 
     |
129 | 128 | breq1d 4405 |
. . . . . 6
   
     |
130 | 129 | cbvrexv 3006 |
. . . . 5
   

    |
131 | 127, 130 | syl6ib 234 |
. . . 4
  
   
 
  
   |
132 | 131 | ex 441 |
. . 3
  
  
    
    |
133 | 2, 4, 6, 22, 132 | finds2 6740 |
. 2
  
   
   |
134 | 133 | impcom 437 |
1
  
    
  |