Step | Hyp | Ref
| Expression |
1 | | elex 3040 |
. . . . 5
   |
2 | | sucexb 6655 |
. . . . 5

  |
3 | 1, 2 | sylibr 217 |
. . . 4
   |
4 | | sssucid 5507 |
. . . . 5
 |
5 | | elpwg 3950 |
. . . . 5
 

   |
6 | 4, 5 | mpbiri 241 |
. . . 4
    |
7 | | limsucncmpi.1 |
. . . . . . 7
 |
8 | | limuni 5490 |
. . . . . . 7

   |
9 | 7, 8 | ax-mp 5 |
. . . . . 6
  |
10 | | elin 3608 |
. . . . . . . . . 10
   
     |
11 | | elpwi 3951 |
. . . . . . . . . . 11
 
  |
12 | 11 | anim1i 578 |
. . . . . . . . . 10
  
     |
13 | 10, 12 | sylbi 200 |
. . . . . . . . 9
    
   |
14 | | nlim0 5488 |
. . . . . . . . . . . . . . . 16
 |
15 | 7, 14 | 2th 247 |
. . . . . . . . . . . . . . 15

  |
16 | | xor3 364 |
. . . . . . . . . . . . . . 15
 

    |
17 | 15, 16 | mpbir 214 |
. . . . . . . . . . . . . 14
   |
18 | | limeq 5442 |
. . . . . . . . . . . . . . 15

    |
19 | 18 | necon3bi 2669 |
. . . . . . . . . . . . . 14
 
   |
20 | 17, 19 | ax-mp 5 |
. . . . . . . . . . . . 13
 |
21 | | uni0 4217 |
. . . . . . . . . . . . 13
  |
22 | 20, 21 | neeqtrri 2716 |
. . . . . . . . . . . 12
  |
23 | | unieq 4198 |
. . . . . . . . . . . . 13

    |
24 | 23 | neeq2d 2703 |
. . . . . . . . . . . 12

 
    |
25 | 22, 24 | mpbiri 241 |
. . . . . . . . . . 11

   |
26 | 25 | a1i 11 |
. . . . . . . . . 10
 
      |
27 | | limord 5489 |
. . . . . . . . . . . . . 14

  |
28 | | ordsson 6635 |
. . . . . . . . . . . . . 14

  |
29 | 7, 27, 28 | mp2b 10 |
. . . . . . . . . . . . 13
 |
30 | | sstr2 3425 |
. . . . . . . . . . . . 13
     |
31 | 29, 30 | mpi 20 |
. . . . . . . . . . . 12
   |
32 | | ordunifi 7839 |
. . . . . . . . . . . . 13
 

   |
33 | 32 | 3expia 1233 |
. . . . . . . . . . . 12
 
      |
34 | 31, 33 | sylan 479 |
. . . . . . . . . . 11
 
      |
35 | | ssel 3412 |
. . . . . . . . . . . . 13
  
    |
36 | 7, 27 | ax-mp 5 |
. . . . . . . . . . . . . 14
 |
37 | | nordeq 5449 |
. . . . . . . . . . . . . 14
  
    |
38 | 36, 37 | mpan 684 |
. . . . . . . . . . . . 13
 
   |
39 | 35, 38 | syl6 33 |
. . . . . . . . . . . 12
  
    |
40 | 39 | adantr 472 |
. . . . . . . . . . 11
 
  
    |
41 | 34, 40 | syld 44 |
. . . . . . . . . 10
 
      |
42 | 26, 41 | pm2.61dne 2729 |
. . . . . . . . 9
 
    |
43 | 13, 42 | syl 17 |
. . . . . . . 8
       |
44 | 43 | neneqd 2648 |
. . . . . . 7
   
   |
45 | 44 | nrex 2841 |
. . . . . 6

      |
46 | | unieq 4198 |
. . . . . . . . 9
     |
47 | 46 | eqeq2d 2481 |
. . . . . . . 8
 
     |
48 | | pweq 3945 |
. . . . . . . . . . 11
 
   |
49 | 48 | ineq1d 3624 |
. . . . . . . . . 10
  
      |
50 | 49 | rexeqdv 2980 |
. . . . . . . . 9
  
 
 
     
    |
51 | 50 | notbid 301 |
. . . . . . . 8
      
          |
52 | 47, 51 | anbi12d 725 |
. . . . . . 7
          
      
     |
53 | 52 | rspcev 3136 |
. . . . . 6
         
                |
54 | 9, 45, 53 | mpanr12 699 |
. . . . 5
          
    |
55 | | rexanali 2839 |
. . . . 5
           
        
    |
56 | 54, 55 | sylib 201 |
. . . 4
  
 
     
    |
57 | 3, 6, 56 | 3syl 18 |
. . 3
              |
58 | | imnan 429 |
. . 3
  
 
     
  
         
     |
59 | 57, 58 | mpbi 213 |
. 2
         
    |
60 | | ordunisuc 6678 |
. . . . 5

   |
61 | 7, 27, 60 | mp2b 10 |
. . . 4
  |
62 | 61 | eqcomi 2480 |
. . 3

 |
63 | 62 | iscmp 20480 |
. 2

 
       
     |
64 | 59, 63 | mtbir 306 |
1
 |