Proof of Theorem tz9.12lem3
Step | Hyp | Ref
| Expression |
1 | | tz9.12lem.2 |
. . . . . . . . . . 11
  
       |
2 | 1 | funmpt2 5626 |
. . . . . . . . . 10
 |
3 | | fveq2 5879 |
. . . . . . . . . . . . . . 15
           |
4 | 3 | eleq2d 2534 |
. . . . . . . . . . . . . 14
     
       |
5 | 4 | rspcev 3136 |
. . . . . . . . . . . . 13
 
     
      |
6 | | rabn0 3755 |
. . . . . . . . . . . . 13
 
            |
7 | 5, 6 | sylibr 217 |
. . . . . . . . . . . 12
 
     
       |
8 | | intex 4557 |
. . . . . . . . . . . 12
 
      
       |
9 | 7, 8 | sylib 201 |
. . . . . . . . . . 11
 
      
       |
10 | | vex 3034 |
. . . . . . . . . . . 12
 |
11 | | eleq1 2537 |
. . . . . . . . . . . . . . . 16
     
       |
12 | 11 | rabbidv 3022 |
. . . . . . . . . . . . . . 15
       
       |
13 | 12 | inteqd 4231 |
. . . . . . . . . . . . . 14
         
       |
14 | 13 | eleq1d 2533 |
. . . . . . . . . . . . 13
   
    
          |
15 | 1 | dmmpt 5337 |
. . . . . . . . . . . . 13
          |
16 | 14, 15 | elrab2 3186 |
. . . . . . . . . . . 12

           |
17 | 10, 16 | mpbiran 932 |
. . . . . . . . . . 11

         |
18 | 9, 17 | sylibr 217 |
. . . . . . . . . 10
 
    
  |
19 | | funfvima 6157 |
. . . . . . . . . 10
               |
20 | 2, 18, 19 | sylancr 676 |
. . . . . . . . 9
 
                 |
21 | | tz9.12lem.1 |
. . . . . . . . . . 11
 |
22 | 21, 1 | tz9.12lem2 8277 |
. . . . . . . . . 10
      |
23 | 21, 1 | tz9.12lem1 8276 |
. . . . . . . . . . . 12
     |
24 | | onsucuni 6674 |
. . . . . . . . . . . 12
    
           |
25 | 23, 24 | ax-mp 5 |
. . . . . . . . . . 11
          |
26 | 25 | sseli 3414 |
. . . . . . . . . 10
                    |
27 | | r1ord2 8270 |
. . . . . . . . . 10
                       
            |
28 | 22, 26, 27 | mpsyl 64 |
. . . . . . . . 9
                            |
29 | 20, 28 | syl6 33 |
. . . . . . . 8
 
             
            |
30 | 29 | imp 436 |
. . . . . . 7
        
                   |
31 | 13, 1 | fvmptg 5961 |
. . . . . . . . . . . 12
   
                   |
32 | 10, 31 | mpan 684 |
. . . . . . . . . . 11
  
          
       |
33 | 8, 32 | sylbi 200 |
. . . . . . . . . 10
 
                  |
34 | | ssrab2 3500 |
. . . . . . . . . . 11
       |
35 | | onint 6641 |
. . . . . . . . . . 11
  
    
      
       
       |
36 | 34, 35 | mpan 684 |
. . . . . . . . . 10
 
            
       |
37 | 33, 36 | eqeltrd 2549 |
. . . . . . . . 9
 
                 |
38 | | fveq2 5879 |
. . . . . . . . . . . 12
                   |
39 | 38 | eleq2d 2534 |
. . . . . . . . . . 11
         
           |
40 | 4 | cbvrabv 3030 |
. . . . . . . . . . 11
      
      |
41 | 39, 40 | elrab2 3186 |
. . . . . . . . . 10
          
                |
42 | 41 | simprbi 471 |
. . . . . . . . 9
                     |
43 | 7, 37, 42 | 3syl 18 |
. . . . . . . 8
 
    
          |
44 | 43 | adantr 472 |
. . . . . . 7
        
          |
45 | 30, 44 | sseldd 3419 |
. . . . . 6
        
           |
46 | 45 | exp31 615 |
. . . . 5
         
          |
47 | 46 | com3r 81 |
. . . 4
      
             |
48 | 47 | rexlimdv 2870 |
. . 3
  
                |
49 | 48 | ralimia 2794 |
. 2
 

   

           |
50 | | r1suc 8259 |
. . . . 5
                           |
51 | 22, 50 | ax-mp 5 |
. . . 4
  
         
       |
52 | 51 | eleq2i 2541 |
. . 3
                      |
53 | 21 | elpw 3948 |
. . 3
    
     
           |
54 | | dfss3 3408 |
. . 3
         

           |
55 | 52, 53, 54 | 3bitri 279 |
. 2
          
           |
56 | 49, 55 | sylibr 217 |
1
 

   
           |