Step | Hyp | Ref
| Expression |
1 | | oveq2 6322 |
. . . . 5
       |
2 | 1 | eleq2d 2524 |
. . . 4
             |
3 | 2 | imbi2d 322 |
. . 3
                     |
4 | | oveq2 6322 |
. . . . 5
       |
5 | 4 | eleq2d 2524 |
. . . 4
     
       |
6 | 5 | imbi2d 322 |
. . 3
                     |
7 | | oveq2 6322 |
. . . . 5
       |
8 | 7 | eleq2d 2524 |
. . . 4
             |
9 | 8 | imbi2d 322 |
. . 3
                     |
10 | | oveq2 6322 |
. . . . 5
       |
11 | 10 | eleq2d 2524 |
. . . 4
     
       |
12 | 11 | imbi2d 322 |
. . 3
                     |
13 | | eldifi 3566 |
. . . . . . . 8
  
  |
14 | | oecl 7264 |
. . . . . . . 8
 
     |
15 | 13, 14 | sylan 478 |
. . . . . . 7
   
     |
16 | | om1 7268 |
. . . . . . 7
           |
17 | 15, 16 | syl 17 |
. . . . . 6
   
    
    |
18 | | ondif2 7229 |
. . . . . . . . 9
  
    |
19 | 18 | simprbi 470 |
. . . . . . . 8
  
  |
20 | 19 | adantr 471 |
. . . . . . 7
   
   |
21 | 13 | adantr 471 |
. . . . . . . 8
   
   |
22 | | simpr 467 |
. . . . . . . . 9
   
   |
23 | | dif20el 7232 |
. . . . . . . . . 10
  
  |
24 | 23 | adantr 471 |
. . . . . . . . 9
   

  |
25 | | oen0 7312 |
. . . . . . . . 9
         |
26 | 21, 22, 24, 25 | syl21anc 1275 |
. . . . . . . 8
   

    |
27 | | omordi 7292 |
. . . . . . . 8
                     |
28 | 21, 15, 26, 27 | syl21anc 1275 |
. . . . . . 7
   
     
       |
29 | 20, 28 | mpd 15 |
. . . . . 6
   
    
      |
30 | 17, 29 | eqeltrrd 2540 |
. . . . 5
   
         |
31 | | oesuc 7254 |
. . . . . 6
 
         |
32 | 13, 31 | sylan 478 |
. . . . 5
   
         |
33 | 30, 32 | eleqtrrd 2542 |
. . . 4
   
       |
34 | 33 | expcom 441 |
. . 3
 
         |
35 | | oecl 7264 |
. . . . . . . . . . 11
 
     |
36 | 13, 35 | sylan 478 |
. . . . . . . . . 10
   
     |
37 | | om1 7268 |
. . . . . . . . . 10
           |
38 | 36, 37 | syl 17 |
. . . . . . . . 9
   
    
    |
39 | 19 | adantr 471 |
. . . . . . . . . 10
   
   |
40 | 13 | adantr 471 |
. . . . . . . . . . 11
   
   |
41 | | simpr 467 |
. . . . . . . . . . . 12
   
   |
42 | 23 | adantr 471 |
. . . . . . . . . . . 12
   

  |
43 | | oen0 7312 |
. . . . . . . . . . . 12
         |
44 | 40, 41, 42, 43 | syl21anc 1275 |
. . . . . . . . . . 11
   

    |
45 | | omordi 7292 |
. . . . . . . . . . 11
                     |
46 | 40, 36, 44, 45 | syl21anc 1275 |
. . . . . . . . . 10
   
     
       |
47 | 39, 46 | mpd 15 |
. . . . . . . . 9
   
    
      |
48 | 38, 47 | eqeltrrd 2540 |
. . . . . . . 8
   
         |
49 | | oesuc 7254 |
. . . . . . . . 9
 
         |
50 | 13, 49 | sylan 478 |
. . . . . . . 8
   
         |
51 | 48, 50 | eleqtrrd 2542 |
. . . . . . 7
   
       |
52 | | suceloni 6666 |
. . . . . . . . 9

  |
53 | | oecl 7264 |
. . . . . . . . 9
 
     |
54 | 13, 52, 53 | syl2an 484 |
. . . . . . . 8
   
     |
55 | | ontr1 5487 |
. . . . . . . 8
                     |
56 | 54, 55 | syl 17 |
. . . . . . 7
   
      
            |
57 | 51, 56 | mpan2d 685 |
. . . . . 6
   
             |
58 | 57 | expcom 441 |
. . . . 5
 
               |
59 | 58 | adantr 471 |
. . . 4
 
        
        |
60 | 59 | a2d 29 |
. . 3
 
         
           |
61 | | bi2.04 367 |
. . . . . 6
          
   
        |
62 | 61 | ralbii 2830 |
. . . . 5
 

          
           |
63 | | r19.21v 2804 |
. . . . 5
 

  
          
        |
64 | 62, 63 | bitri 257 |
. . . 4
 

             
        |
65 | | limsuc 6702 |
. . . . . . . . . 10


   |
66 | 65 | biimpa 491 |
. . . . . . . . 9
     |
67 | | elex 3065 |
. . . . . . . . . . . . 13
   |
68 | | sucexb 6662 |
. . . . . . . . . . . . . 14

  |
69 | | sucidg 5519 |
. . . . . . . . . . . . . 14
   |
70 | 68, 69 | sylbir 218 |
. . . . . . . . . . . . 13
   |
71 | 67, 70 | syl 17 |
. . . . . . . . . . . 12

  |
72 | | eleq2 2528 |
. . . . . . . . . . . . . 14
     |
73 | | oveq2 6322 |
. . . . . . . . . . . . . . 15
       |
74 | 73 | eleq2d 2524 |
. . . . . . . . . . . . . 14
             |
75 | 72, 74 | imbi12d 326 |
. . . . . . . . . . . . 13
  
     
        |
76 | 75 | rspcv 3157 |
. . . . . . . . . . . 12
   
    
         |
77 | 71, 76 | mpid 42 |
. . . . . . . . . . 11
   
    
       |
78 | 77 | anc2li 564 |
. . . . . . . . . 10
   
    
         |
79 | 74 | rspcev 3161 |
. . . . . . . . . . 11
      

      |
80 | | eliun 4296 |
. . . . . . . . . . 11
     

      |
81 | 79, 80 | sylibr 217 |
. . . . . . . . . 10
      
  
    |
82 | 78, 81 | syl6 34 |
. . . . . . . . 9
   
    
  
     |
83 | 66, 82 | syl 17 |
. . . . . . . 8
    

       
     |
84 | 83 | adantr 471 |
. . . . . . 7
  

    

        
    |
85 | 13 | adantl 472 |
. . . . . . . . . 10
       |
86 | | simpl 463 |
. . . . . . . . . 10
       |
87 | 23 | adantl 472 |
. . . . . . . . . 10
       |
88 | | vex 3059 |
. . . . . . . . . . 11
 |
89 | | oelim 7261 |
. . . . . . . . . . 11
         
    |
90 | 88, 89 | mpanlr1 697 |
. . . . . . . . . 10
       
    |
91 | 85, 86, 87, 90 | syl21anc 1275 |
. . . . . . . . 9
        
   |
92 | 91 | adantlr 726 |
. . . . . . . 8
  

     
    |
93 | 92 | eleq2d 2524 |
. . . . . . 7
  

          
     |
94 | 84, 93 | sylibrd 242 |
. . . . . 6
  

    

            |
95 | 94 | ex 440 |
. . . . 5
   
   

             |
96 | 95 | a2d 29 |
. . . 4
        
     
           |
97 | 64, 96 | syl5bi 225 |
. . 3
    

         
          |
98 | 3, 6, 9, 12, 34, 60, 97 | tfindsg2 6714 |
. 2
 
           |
99 | 98 | impancom 446 |
1
 
           |