Step | Hyp | Ref
| Expression |
1 | | 2z 10969 |
. . . 4
 |
2 | | uzid 11173 |
. . . 4
       |
3 | 1, 2 | ax-mp 5 |
. . 3
     |
4 | | istrkg.p |
. . . 4
     |
5 | | istrkg.d |
. . . 4
     |
6 | | istrkg.i |
. . . 4
Itv   |
7 | 4, 5, 6 | istrkgld 24507 |
. . 3
 
      DimTarskiG≥       ..^  



 
 ..^       
           
           
                           |
8 | 3, 7 | mpan2 677 |
. 2
  DimTarskiG≥       ..^  



 
 ..^       
           
           
                           |
9 | | r19.41v 2942 |
. . . . 5
    
   ..^                                                          ..^   
 


 
 ..^                                                          ..^      |
10 | | ancom 452 |
. . . . . 6
   
   ..^                                                          ..^   
    ..^  


 
 ..^       
           
           
                          |
11 | 10 | rexbii 2889 |
. . . . 5
    
   ..^                                                          ..^   

    ..^  


 
 ..^       
           
           
                          |
12 | | ancom 452 |
. . . . 5
   

   ..^                                                          ..^   
    ..^  



 
 ..^       
           
           
                          |
13 | 9, 11, 12 | 3bitr3ri 280 |
. . . 4
     ..^    

 
 ..^                                                        
    ..^    
   ..^                                                          |
14 | 13 | exbii 1718 |
. . 3
       ..^   


 
 ..^       
           
           
                       
  
    ..^    
   ..^                                                          |
15 | | rexcom4 3067 |
. . 3
        ..^   

 
 ..^       
           
           
                       
  
    ..^    
   ..^                                                          |
16 | | simpr 463 |
. . . . . . . . . 10
    ..^                                                                       |
17 | 16 | reximi 2855 |
. . . . . . . . 9
     ..^                                                       
                |
18 | 17 | reximi 2855 |
. . . . . . . 8
  
 
 ..^                                                       

                |
19 | 18 | adantl 468 |
. . . . . . 7
     ..^    
 
 ..^                                                         
                |
20 | 19 | exlimiv 1776 |
. . . . . 6
       ..^   

 
 ..^       
           
           
                        

                |
21 | 20 | adantl 468 |
. . . . 5
        ..^   

 
 ..^       
           
           
                          
                |
22 | | 1ex 9638 |
. . . . . . . . . 10
 |
23 | | vex 3048 |
. . . . . . . . . 10
 |
24 | 22, 23 | f1osn 5852 |
. . . . . . . . 9
  
           |
25 | | f1of1 5813 |
. . . . . . . . 9
                             |
26 | 24, 25 | mp1i 13 |
. . . . . . . 8
   
            |
27 | | snssi 4116 |
. . . . . . . 8
     |
28 | | f1ss 5784 |
. . . . . . . 8
                 
             |
29 | 26, 27, 28 | syl2anc 667 |
. . . . . . 7
   
          |
30 | | fzo12sn 11996 |
. . . . . . . . . . . 12
 ..^    |
31 | | mpteq1 4483 |
. . . . . . . . . . . 12
  ..^     ..^        |
32 | 30, 31 | ax-mp 5 |
. . . . . . . . . . 11
  ..^       |
33 | | fmptsn 6084 |
. . . . . . . . . . . 12
 
            |
34 | 22, 23, 33 | mp2an 678 |
. . . . . . . . . . 11
  
       |
35 | 32, 34 | eqtr4i 2476 |
. . . . . . . . . 10
  ..^        |
36 | 35 | a1i 11 |
. . . . . . . . 9
  ..^    
    |
37 | 30 | a1i 11 |
. . . . . . . . 9
 ..^     |
38 | | eqidd 2452 |
. . . . . . . . 9
  |
39 | 36, 37, 38 | f1eq123d 5809 |
. . . . . . . 8
   ..^     ..^                 |
40 | 39 | trud 1453 |
. . . . . . 7
   ..^     ..^  
             |
41 | 29, 40 | sylibr 216 |
. . . . . 6
   ..^     ..^     |
42 | | ral0 3874 |
. . . . . . . . . 10
      ..^          ..^     
    ..^          ..^     
    ..^          ..^        |
43 | | fzo0 11942 |
. . . . . . . . . . 11
 ..^  |
44 | 43 | raleqi 2991 |
. . . . . . . . . 10
 
 ..^       ..^    
     ..^          ..^    
     ..^          ..^    
     ..^      
      ..^          ..^     
    ..^          ..^     
    ..^          ..^         |
45 | 42, 44 | mpbir 213 |
. . . . . . . . 9
  ..^       ..^          ..^    
     ..^          ..^          ..^          ..^        |
46 | 45 | jctl 544 |
. . . . . . . 8
              
 
 ..^       ..^    
     ..^          ..^    
     ..^          ..^    
     ..^                        |
47 | 46 | reximi 2855 |
. . . . . . 7
               

 
 ..^       ..^    
     ..^          ..^    
     ..^          ..^    
     ..^                        |
48 | 47 | reximi 2855 |
. . . . . 6
  
             


 
 ..^       ..^    
     ..^          ..^    
     ..^          ..^    
     ..^                        |
49 | | ovex 6318 |
. . . . . . . 8
 ..^  |
50 | 49 | mptex 6136 |
. . . . . . 7
  ..^   |
51 | | f1eq1 5774 |
. . . . . . . 8
   ..^      ..^  
  ..^     ..^      |
52 | | nfmpt1 4492 |
. . . . . . . . . . . . 13
    ..^   |
53 | 52 | nfeq2 2607 |
. . . . . . . . . . . 12
   ..^   |
54 | | nfv 1761 |
. . . . . . . . . . . 12
  
  |
55 | 53, 54 | nfan 2011 |
. . . . . . . . . . 11
     ..^      |
56 | | simpll 760 |
. . . . . . . . . . . . . . 15
     ..^    
 ..^    ..^    |
57 | 56 | fveq1d 5867 |
. . . . . . . . . . . . . 14
     ..^    
 ..^         ..^       |
58 | 57 | oveq1d 6305 |
. . . . . . . . . . . . 13
     ..^    
 ..^            ..^        |
59 | 56 | fveq1d 5867 |
. . . . . . . . . . . . . 14
     ..^    
 ..^         ..^       |
60 | 59 | oveq1d 6305 |
. . . . . . . . . . . . 13
     ..^    
 ..^            ..^        |
61 | 58, 60 | eqeq12d 2466 |
. . . . . . . . . . . 12
     ..^    
 ..^             
     ..^    
     ..^         |
62 | 57 | oveq1d 6305 |
. . . . . . . . . . . . 13
     ..^    
 ..^            ..^        |
63 | 59 | oveq1d 6305 |
. . . . . . . . . . . . 13
     ..^    
 ..^            ..^        |
64 | 62, 63 | eqeq12d 2466 |
. . . . . . . . . . . 12
     ..^    
 ..^             
     ..^    
     ..^         |
65 | 57 | oveq1d 6305 |
. . . . . . . . . . . . 13
     ..^    
 ..^            ..^        |
66 | 59 | oveq1d 6305 |
. . . . . . . . . . . . 13
     ..^    
 ..^            ..^        |
67 | 65, 66 | eqeq12d 2466 |
. . . . . . . . . . . 12
     ..^    
 ..^             
     ..^    
     ..^         |
68 | 61, 64, 67 | 3anbi123d 1339 |
. . . . . . . . . . 11
     ..^    
 ..^               
          
                   ..^          ..^    
     ..^          ..^          ..^          ..^          |
69 | 55, 68 | ralbida 2821 |
. . . . . . . . . 10
    ..^  
   
 ..^                                        
 ..^       ..^          ..^          ..^          ..^          ..^          ..^          |
70 | 69 | anbi1d 711 |
. . . . . . . . 9
    ..^  
      ..^             
                                        
 
 ..^       ..^    
     ..^          ..^    
     ..^          ..^    
     ..^                         |
71 | 70 | 2rexbidva 2907 |
. . . . . . . 8
   ..^   

   ..^                                                      


 
 ..^       ..^    
     ..^          ..^    
     ..^          ..^    
     ..^                         |
72 | 51, 71 | anbi12d 717 |
. . . . . . 7
   ..^       ..^    
   ..^                                                           ..^     ..^    
   ..^       ..^          ..^          ..^          ..^          ..^          ..^                          |
73 | 50, 72 | spcev 3141 |
. . . . . 6
    ..^     ..^    
 
 ..^       ..^          ..^          ..^          ..^          ..^          ..^                             ..^  


 
 ..^       
           
           
                          |
74 | 41, 48, 73 | syl2an 480 |
. . . . 5
   
                     ..^    
   ..^                                                          |
75 | 21, 74 | impbida 843 |
. . . 4
        ..^   

 
 ..^       
           
           
                       


                 |
76 | 75 | rexbiia 2888 |
. . 3
        ..^   

 
 ..^       
           
           
                       



                |
77 | 14, 15, 76 | 3bitr2i 277 |
. 2
       ..^   


 
 ..^       
           
           
                       



                |
78 | 8, 77 | syl6bb 265 |
1
  DimTarskiG≥  

                 |