Step | Hyp | Ref
| Expression |
1 | | ssrab2 3516 |
. . . . . . . . . 10
   |
2 | | nnuz 11201 |
. . . . . . . . . 10
     |
3 | 1, 2 | sseqtri 3466 |
. . . . . . . . 9
       |
4 | | rabn0 3754 |
. . . . . . . . . 10
 
 
  |
5 | 4 | biimpri 210 |
. . . . . . . . 9
 
    |
6 | | infssuzcl 11252 |
. . . . . . . . 9
  
    
   inf 
 
     |
7 | 3, 5, 6 | sylancr 670 |
. . . . . . . 8
 
inf 
   
   |
8 | | nfrab1 2973 |
. . . . . . . . . 10
  
  |
9 | | nfcv 2594 |
. . . . . . . . . 10
   |
10 | | nfcv 2594 |
. . . . . . . . . 10
  |
11 | 8, 9, 10 | nfinf 8003 |
. . . . . . . . 9
 inf 
 
  |
12 | | nfcv 2594 |
. . . . . . . . 9
   |
13 | 11 | nfcsb1 3380 |
. . . . . . . . . 10
  inf      ![]_ ]_](_urbrack.gif)  |
14 | 13 | nfcri 2588 |
. . . . . . . . 9

inf 
    ![]_ ]_](_urbrack.gif)  |
15 | | csbeq1a 3374 |
. . . . . . . . . 10
 inf     inf      ![]_ ]_](_urbrack.gif)   |
16 | 15 | eleq2d 2516 |
. . . . . . . . 9
 inf     
inf      ![]_ ]_](_urbrack.gif)    |
17 | 11, 12, 14, 16 | elrabf 3196 |
. . . . . . . 8
inf 
 
  
inf 
 

inf 
    ![]_ ]_](_urbrack.gif)    |
18 | 7, 17 | sylib 200 |
. . . . . . 7
 
inf 
 

inf 
    ![]_ ]_](_urbrack.gif)    |
19 | 18 | simpld 461 |
. . . . . 6
 
inf 
     |
20 | 18 | simprd 465 |
. . . . . . 7
 
inf      ![]_ ]_](_urbrack.gif)   |
21 | 19 | nnred 10631 |
. . . . . . . . 9
 
inf 
     |
22 | 21 | ltnrd 9774 |
. . . . . . . 8
 
inf 
 

inf 
     |
23 | | eliun 4286 |
. . . . . . . . 9
   ..^inf 
    
  ..^inf 
       |
24 | 21 | ad2antrr 733 |
. . . . . . . . . . . 12
   
 ..^inf       
inf 
     |
25 | | elfzouz 11931 |
. . . . . . . . . . . . . . 15
  ..^inf 
 
        |
26 | 25, 2 | syl6eleqr 2542 |
. . . . . . . . . . . . . 14
  ..^inf 
 
    |
27 | 26 | ad2antlr 734 |
. . . . . . . . . . . . 13
   
 ..^inf       
  |
28 | 27 | nnred 10631 |
. . . . . . . . . . . 12
   
 ..^inf       
  |
29 | | simpr 463 |
. . . . . . . . . . . . . 14
   
 ..^inf       
  |
30 | | iundisj.1 |
. . . . . . . . . . . . . . . 16
   |
31 | 30 | eleq2d 2516 |
. . . . . . . . . . . . . . 15
 
   |
32 | 31 | elrab 3198 |
. . . . . . . . . . . . . 14
  
    |
33 | 27, 29, 32 | sylanbrc 671 |
. . . . . . . . . . . . 13
   
 ..^inf       

   |
34 | | infssuzle 11251 |
. . . . . . . . . . . . 13
  
    

 
inf 
     |
35 | 3, 33, 34 | sylancr 670 |
. . . . . . . . . . . 12
   
 ..^inf       
inf 
     |
36 | | elfzolt2 11936 |
. . . . . . . . . . . . 13
  ..^inf 
 
  inf       |
37 | 36 | ad2antlr 734 |
. . . . . . . . . . . 12
   
 ..^inf       
inf 
 
   |
38 | 24, 28, 24, 35, 37 | lelttrd 9798 |
. . . . . . . . . . 11
   
 ..^inf       
inf 
   inf       |
39 | 38 | ex 436 |
. . . . . . . . . 10
  
 ..^inf       
inf 
   inf        |
40 | 39 | rexlimdva 2881 |
. . . . . . . . 9
 
   ..^inf       inf 
   inf        |
41 | 23, 40 | syl5bi 221 |
. . . . . . . 8
 
   ..^inf 
     inf 
   inf        |
42 | 22, 41 | mtod 181 |
. . . . . . 7
 
  ..^inf         |
43 | 20, 42 | eldifd 3417 |
. . . . . 6
 
 inf      ![]_ ]_](_urbrack.gif)
  ..^inf 
        |
44 | | csbeq1 3368 |
. . . . . . . . 9
 inf       ![]_ ]_](_urbrack.gif) inf      ![]_ ]_](_urbrack.gif)   |
45 | | oveq2 6303 |
. . . . . . . . . 10
 inf      ..^  ..^inf 
      |
46 | 45 | iuneq1d 4306 |
. . . . . . . . 9
 inf       ..^    ..^inf 
       |
47 | 44, 46 | difeq12d 3554 |
. . . . . . . 8
 inf      
 ![]_ ]_](_urbrack.gif)
  ..^    inf      ![]_ ]_](_urbrack.gif)
  ..^inf 
        |
48 | 47 | eleq2d 2516 |
. . . . . . 7
 inf         ![]_ ]_](_urbrack.gif)   ..^  
 inf      ![]_ ]_](_urbrack.gif)
  ..^inf 
         |
49 | 48 | rspcev 3152 |
. . . . . 6
 inf      inf 
 
  ![]_ ]_](_urbrack.gif)   ..^inf 
       
   ![]_ ]_](_urbrack.gif)   ..^     |
50 | 19, 43, 49 | syl2anc 667 |
. . . . 5
 
    ![]_ ]_](_urbrack.gif)
  ..^     |
51 | | nfv 1763 |
. . . . . 6

   ..^    |
52 | | nfcsb1v 3381 |
. . . . . . . 8
  
 ![]_ ]_](_urbrack.gif)  |
53 | | nfcv 2594 |
. . . . . . . 8
  
 ..^   |
54 | 52, 53 | nfdif 3556 |
. . . . . . 7
     ![]_ ]_](_urbrack.gif)
  ..^    |
55 | 54 | nfcri 2588 |
. . . . . 6

   ![]_ ]_](_urbrack.gif)   ..^    |
56 | | csbeq1a 3374 |
. . . . . . . 8
   ![]_ ]_](_urbrack.gif)   |
57 | | oveq2 6303 |
. . . . . . . . 9
  ..^  ..^   |
58 | 57 | iuneq1d 4306 |
. . . . . . . 8
   ..^    ..^    |
59 | 56, 58 | difeq12d 3554 |
. . . . . . 7
    ..^      ![]_ ]_](_urbrack.gif)
  ..^     |
60 | 59 | eleq2d 2516 |
. . . . . 6
     ..^  
 
 ![]_ ]_](_urbrack.gif)
  ..^      |
61 | 51, 55, 60 | cbvrex 3018 |
. . . . 5
   
 ..^   
   ![]_ ]_](_urbrack.gif)   ..^     |
62 | 50, 61 | sylibr 216 |
. . . 4
 
    ..^     |
63 | | eldifi 3557 |
. . . . 5
  
 ..^  
  |
64 | 63 | reximi 2857 |
. . . 4
   
 ..^   
  |
65 | 62, 64 | impbii 191 |
. . 3
 

   ..^     |
66 | | eliun 4286 |
. . 3
 
   |
67 | | eliun 4286 |
. . 3
   
 ..^   
   ..^     |
68 | 65, 66, 67 | 3bitr4i 281 |
. 2
 
    ..^     |
69 | 68 | eqriv 2450 |
1
 
   ..^    |