Step | Hyp | Ref
| Expression |
1 | | mirreu.a |
. . . . . 6
   |
2 | 1 | adantr 471 |
. . . . 5
 
   |
3 | | eqidd 2462 |
. . . . 5
 
       |
4 | | simpr 467 |
. . . . . 6
 
   |
5 | | mirreu.p |
. . . . . . 7
     |
6 | | mirreu.d |
. . . . . . 7
     |
7 | | mirreu.i |
. . . . . . 7
Itv   |
8 | | mirreu.g |
. . . . . . . 8

TarskiG |
9 | 8 | adantr 471 |
. . . . . . 7
 
 TarskiG |
10 | 5, 6, 7, 9, 2, 2 | tgbtwntriv2 24579 |
. . . . . 6
 
       |
11 | 4, 10 | eqeltrrd 2540 |
. . . . 5
 
       |
12 | | oveq2 6322 |
. . . . . . . 8
       |
13 | 12 | eqeq1d 2463 |
. . . . . . 7
     
       |
14 | | oveq1 6321 |
. . . . . . . 8
           |
15 | 14 | eleq2d 2524 |
. . . . . . 7
 
   
       |
16 | 13, 15 | anbi12d 722 |
. . . . . 6
                
        |
17 | 16 | rspcev 3161 |
. . . . 5
             
    
       |
18 | 2, 3, 11, 17 | syl12anc 1274 |
. . . 4
 
 
    
       |
19 | 8 | ad3antrrr 741 |
. . . . . . . 8
   
 
                         TarskiG |
20 | | mirreu.m |
. . . . . . . . 9
   |
21 | 20 | ad3antrrr 741 |
. . . . . . . 8
   
 
                           |
22 | | simplrl 775 |
. . . . . . . 8
   
 
                           |
23 | | simprll 777 |
. . . . . . . . 9
   
 
                               |
24 | | simpllr 774 |
. . . . . . . . . 10
   
 
                           |
25 | 24 | oveq2d 6330 |
. . . . . . . . 9
   
 
                               |
26 | 23, 25 | eqtrd 2495 |
. . . . . . . 8
   
 
                               |
27 | 5, 6, 7, 19, 21, 22, 21, 26 | axtgcgrid 24559 |
. . . . . . 7
   
 
                           |
28 | | simplrr 776 |
. . . . . . . 8
   
 
                           |
29 | | simprrl 779 |
. . . . . . . . 9
   
 
                               |
30 | 29, 25 | eqtrd 2495 |
. . . . . . . 8
   
 
                               |
31 | 5, 6, 7, 19, 21, 28, 21, 30 | axtgcgrid 24559 |
. . . . . . 7
   
 
                           |
32 | 27, 31 | eqtr3d 2497 |
. . . . . 6
   
 
                           |
33 | 32 | ex 440 |
. . . . 5
    
 
                          |
34 | 33 | ralrimivva 2820 |
. . . 4
 
 

                          |
35 | 18, 34 | jca 539 |
. . 3
 
  
          

                           |
36 | 8 | adantr 471 |
. . . . . 6
 

TarskiG |
37 | 1 | adantr 471 |
. . . . . 6
 

  |
38 | 20 | adantr 471 |
. . . . . 6
 

  |
39 | 5, 6, 7, 36, 37, 38, 38, 37 | axtgsegcon 24560 |
. . . . 5
 


            |
40 | | ancom 456 |
. . . . . . . 8
      
   
    
       |
41 | 8 | adantr 471 |
. . . . . . . . . 10
 
 TarskiG |
42 | 1 | adantr 471 |
. . . . . . . . . 10
 
   |
43 | 20 | adantr 471 |
. . . . . . . . . 10
 
   |
44 | | simpr 467 |
. . . . . . . . . 10
 
   |
45 | 5, 6, 7, 41, 42, 43, 44 | tgbtwncomb 24581 |
. . . . . . . . 9
 
 
   
       |
46 | 45 | anbi2d 715 |
. . . . . . . 8
 
                
        |
47 | 40, 46 | syl5bb 265 |
. . . . . . 7
 
                
        |
48 | 47 | rexbidva 2909 |
. . . . . 6
            

    
        |
49 | 48 | adantr 471 |
. . . . 5
 

 

    
   

    
        |
50 | 39, 49 | mpbid 215 |
. . . 4
 


    
       |
51 | 8 | ad3antrrr 741 |
. . . . . . 7
     
                         TarskiG |
52 | 20 | ad3antrrr 741 |
. . . . . . 7
     
                           |
53 | 1 | ad3antrrr 741 |
. . . . . . 7
     
                           |
54 | | simplrl 775 |
. . . . . . 7
     
                           |
55 | | simplrr 776 |
. . . . . . 7
     
                           |
56 | | simpllr 774 |
. . . . . . 7
     
                           |
57 | | simprlr 778 |
. . . . . . . 8
     
                               |
58 | 5, 6, 7, 51, 54, 52, 53, 57 | tgbtwncom 24580 |
. . . . . . 7
     
                               |
59 | | simprrr 780 |
. . . . . . . 8
     
                               |
60 | 5, 6, 7, 51, 55, 52, 53, 59 | tgbtwncom 24580 |
. . . . . . 7
     
                               |
61 | | simprll 777 |
. . . . . . 7
     
                               |
62 | | simprrl 779 |
. . . . . . 7
     
                               |
63 | 5, 6, 7, 51, 52, 52, 53, 53, 54, 55, 56, 58, 60, 61, 62 | tgsegconeq 24578 |
. . . . . 6
     
                           |
64 | 63 | ex 440 |
. . . . 5
    
 
                          |
65 | 64 | ralrimivva 2820 |
. . . 4
 



                          |
66 | 50, 65 | jca 539 |
. . 3
 

 
    
             
         
          |
67 | 35, 66 | pm2.61dane 2722 |
. 2
       
     

      
         
     
    |
68 | | oveq2 6322 |
. . . . 5
       |
69 | 68 | eqeq1d 2463 |
. . . 4
     
       |
70 | | oveq1 6321 |
. . . . 5
           |
71 | 70 | eleq2d 2524 |
. . . 4
 
   
       |
72 | 69, 71 | anbi12d 722 |
. . 3
                
        |
73 | 72 | reu4 3243 |
. 2
      
           
     

      
         
     
    |
74 | 67, 73 | sylibr 217 |
1
              |