Proof of Theorem rp-isfinite6
Step | Hyp | Ref
| Expression |
1 | | exmid 421 |
. . . 4

  |
2 | 1 | biantrur 513 |
. . 3

 

   |
3 | | andir 884 |
. . 3
       

    |
4 | 2, 3 | bitri 257 |
. 2

 
 
    |
5 | | simpl 463 |
. . . 4
     |
6 | | 0fin 7825 |
. . . . . 6
 |
7 | | eleq1a 2535 |
. . . . . 6


   |
8 | 6, 7 | ax-mp 5 |
. . . . 5

  |
9 | 8 | ancli 558 |
. . . 4


   |
10 | 5, 9 | impbii 192 |
. . 3
  
  |
11 | | rp-isfinite5 36207 |
. . . . . 6

       |
12 | | df-rex 2755 |
. . . . . 6
        
       |
13 | 11, 12 | bitri 257 |
. . . . 5

      
   |
14 | 13 | anbi2i 705 |
. . . 4
      
        |
15 | | df-rex 2755 |
. . . . 5
                |
16 | | en0 7658 |
. . . . . . . . . . . . . . 15

  |
17 | 16 | bicomi 207 |
. . . . . . . . . . . . . 14

  |
18 | | ensymb 7643 |
. . . . . . . . . . . . . 14

  |
19 | 17, 18 | bitri 257 |
. . . . . . . . . . . . 13

  |
20 | 19 | notbii 302 |
. . . . . . . . . . . 12

  |
21 | | elnn0 10900 |
. . . . . . . . . . . . . 14

    |
22 | 21 | anbi1i 706 |
. . . . . . . . . . . . 13
     
  

       |
23 | | andir 884 |
. . . . . . . . . . . . 13
  

    
     
          |
24 | 22, 23 | bitri 257 |
. . . . . . . . . . . 12
     
      
          |
25 | 20, 24 | anbi12i 708 |
. . . . . . . . . . 11
      
              
     |
26 | | andi 883 |
. . . . . . . . . . 11
 
           
  
 

   
       
     |
27 | 25, 26 | bitri 257 |
. . . . . . . . . 10
      
        
       
     |
28 | | 3anass 995 |
. . . . . . . . . . . 12
 
    

    
    |
29 | | 3anass 995 |
. . . . . . . . . . . 12
 
   
 

   
    |
30 | 28, 29 | orbi12i 528 |
. . . . . . . . . . 11
  
   
 
   
        
       
     |
31 | 30 | bicomi 207 |
. . . . . . . . . 10
       
       
  
 
     
   
    |
32 | 27, 31 | sylbb 202 |
. . . . . . . . 9
      
 
 
     
   
    |
33 | | simp2 1015 |
. . . . . . . . . 10
 
       |
34 | | oveq2 6323 |
. . . . . . . . . . . 12
           |
35 | | fz10 11849 |
. . . . . . . . . . . 12
     |
36 | 34, 35 | syl6eq 2512 |
. . . . . . . . . . 11
       |
37 | | simp2 1015 |
. . . . . . . . . . . . 13
 
               |
38 | | simp3 1016 |
. . . . . . . . . . . . 13
 
               |
39 | 37, 38 | eqbrtrrd 4439 |
. . . . . . . . . . . 12
 
           |
40 | | simp1 1014 |
. . . . . . . . . . . 12
 
           |
41 | 39, 40 | pm2.21dd 179 |
. . . . . . . . . . 11
 
           |
42 | 36, 41 | syl3an2 1310 |
. . . . . . . . . 10
 
   
   |
43 | 33, 42 | jaoi 385 |
. . . . . . . . 9
  
   
 
   
 
  |
44 | 32, 43 | syl 17 |
. . . . . . . 8
      
 
  |
45 | | simprr 771 |
. . . . . . . 8
      
 
      |
46 | 44, 45 | jca 539 |
. . . . . . 7
      
 
        |
47 | | nngt0 10666 |
. . . . . . . . . . . 12
   |
48 | | hash0 12580 |
. . . . . . . . . . . . 13
     |
49 | 48 | a1i 11 |
. . . . . . . . . . . 12
       |
50 | | nnnn0 10905 |
. . . . . . . . . . . . 13
   |
51 | | hashfz1 12561 |
. . . . . . . . . . . . 13

          |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . 12
           |
53 | 47, 49, 52 | 3brtr4d 4447 |
. . . . . . . . . . 11
               |
54 | | fzfi 12217 |
. . . . . . . . . . . 12
     |
55 | | hashsdom 12592 |
. . . . . . . . . . . 12
 
                         |
56 | 6, 54, 55 | mp2an 683 |
. . . . . . . . . . 11
                   |
57 | 53, 56 | sylib 201 |
. . . . . . . . . 10
       |
58 | 57 | anim1i 576 |
. . . . . . . . 9
     
 
       
   |
59 | | sdomentr 7732 |
. . . . . . . . . . 11
             |
60 | | sdomnen 7624 |
. . . . . . . . . . 11

  |
61 | 59, 60 | syl 17 |
. . . . . . . . . 10
             |
62 | | ensymb 7643 |
. . . . . . . . . . . 12

  |
63 | 62, 16 | bitri 257 |
. . . . . . . . . . 11

  |
64 | 63 | notbii 302 |
. . . . . . . . . 10

  |
65 | 61, 64 | sylib 201 |
. . . . . . . . 9
          
  |
66 | 58, 65 | syl 17 |
. . . . . . . 8
     
   |
67 | 50 | anim1i 576 |
. . . . . . . 8
     
     
   |
68 | 66, 67 | jca 539 |
. . . . . . 7
     
  
        |
69 | 46, 68 | impbii 192 |
. . . . . 6
      
          |
70 | 69 | exbii 1729 |
. . . . 5
    
     
      
   |
71 | | 19.42v 1845 |
. . . . 5
    
     

  
        |
72 | 15, 70, 71 | 3bitr2ri 282 |
. . . 4
    
     
       |
73 | 14, 72 | bitri 257 |
. . 3
          |
74 | 10, 73 | orbi12i 528 |
. 2
      
         |
75 | 4, 74 | bitri 257 |
1

         |