Step | Hyp | Ref
| Expression |
1 | | tgcgrxfr.a |
. . . 4
   |
2 | 1 | adantr 467 |
. . 3
 
       |
3 | | tgcgrxfr.p |
. . . 4
     |
4 | | tgcgrxfr.m |
. . . 4
     |
5 | | tgcgrxfr.i |
. . . 4
Itv   |
6 | | tgcgrxfr.g |
. . . . 5

TarskiG |
7 | 6 | adantr 467 |
. . . 4
 
     TarskiG |
8 | | tgcgrxfr.d |
. . . . 5
   |
9 | 8 | adantr 467 |
. . . 4
 
       |
10 | | tgcgrxfr.f |
. . . . 5
   |
11 | 10 | adantr 467 |
. . . 4
 
       |
12 | | simpr 463 |
. . . 4
 
           |
13 | 3, 4, 5, 7, 2, 9, 11, 12 | tgldim0itv 24548 |
. . 3
 
           |
14 | | tgcgrxfr.r |
. . . 4
cgrG   |
15 | | tgcgrxfr.b |
. . . . 5
   |
16 | 15 | adantr 467 |
. . . 4
 
       |
17 | | tgcgrxfr.c |
. . . . 5
   |
18 | 17 | adantr 467 |
. . . 4
 
       |
19 | 3, 4, 5, 7, 2, 16,
9, 12, 2 | tgldim0cgr 24549 |
. . . 4
 
           |
20 | 3, 4, 5, 7, 16, 18, 2, 12, 11 | tgldim0cgr 24549 |
. . . 4
 
           |
21 | 3, 4, 5, 7, 18, 2,
11, 12, 9 | tgldim0cgr 24549 |
. . . 4
 
           |
22 | 3, 4, 14, 7, 2, 16, 18, 9, 2, 11, 19, 20, 21 | trgcgr 24561 |
. . 3
 
                   |
23 | | eleq1 2517 |
. . . . 5
     
       |
24 | | eqidd 2452 |
. . . . . . 7
   |
25 | | id 22 |
. . . . . . 7
   |
26 | | eqidd 2452 |
. . . . . . 7
   |
27 | 24, 25, 26 | s3eqd 12959 |
. . . . . 6
               |
28 | 27 | breq2d 4414 |
. . . . 5
                             |
29 | 23, 28 | anbi12d 717 |
. . . 4
                   
                     |
30 | 29 | rspcev 3150 |
. . 3
  
                  
                    |
31 | 2, 13, 22, 30 | syl12anc 1266 |
. 2
 
                          |
32 | 6 | ad3antrrr 736 |
. . . . 5
          
      TarskiG |
33 | | simplr 762 |
. . . . 5
          
        |
34 | 8 | ad3antrrr 736 |
. . . . 5
          
        |
35 | 1 | ad3antrrr 736 |
. . . . 5
          
        |
36 | 15 | ad3antrrr 736 |
. . . . 5
          
        |
37 | 3, 4, 5, 32, 33, 34, 35, 36 | axtgsegcon 24512 |
. . . 4
          
       
           |
38 | 6 | ad7antr 744 |
. . . . . . . . . 10
              
      
          
            TarskiG |
39 | 33 | ad2antrr 732 |
. . . . . . . . . . 11
     
    
 
      
             |
40 | 39 | ad2antrr 732 |
. . . . . . . . . 10
              
      
          
              |
41 | 8 | ad7antr 744 |
. . . . . . . . . 10
              
      
          
              |
42 | | simplr 762 |
. . . . . . . . . . 11
     
    
 
      
             |
43 | 42 | ad2antrr 732 |
. . . . . . . . . 10
              
      
          
              |
44 | | simplr 762 |
. . . . . . . . . 10
              
      
          
              |
45 | | simpllr 769 |
. . . . . . . . . . 11
              
      
          
            
    
      |
46 | 45 | simpld 461 |
. . . . . . . . . 10
              
      
          
                  |
47 | | simprl 764 |
. . . . . . . . . 10
              
      
          
                  |
48 | 3, 4, 5, 38, 40, 41, 43, 44, 46, 47 | tgbtwnexch3 24538 |
. . . . . . . . 9
              
      
          
                  |
49 | 1 | ad7antr 744 |
. . . . . . . . . . 11
              
      
          
              |
50 | 17 | ad7antr 744 |
. . . . . . . . . . 11
              
      
          
              |
51 | 10 | ad7antr 744 |
. . . . . . . . . . 11
              
      
          
              |
52 | | simp-5r 779 |
. . . . . . . . . . . . 13
              
      
          
            
       |
53 | 52 | simprd 465 |
. . . . . . . . . . . 12
              
      
          
              |
54 | 53 | necomd 2679 |
. . . . . . . . . . 11
              
      
          
              |
55 | 3, 4, 5, 38, 40, 41, 43, 44, 46, 47 | tgbtwnexch 24542 |
. . . . . . . . . . 11
              
      
          
                  |
56 | 52 | simpld 461 |
. . . . . . . . . . . 12
              
      
          
                  |
57 | 3, 4, 5, 38, 51, 41, 40, 56 | tgbtwncom 24532 |
. . . . . . . . . . 11
              
      
          
                  |
58 | 15 | ad7antr 744 |
. . . . . . . . . . . 12
              
      
          
              |
59 | | tgcgrxfr.1 |
. . . . . . . . . . . . 13
       |
60 | 59 | ad7antr 744 |
. . . . . . . . . . . 12
              
      
          
                  |
61 | 45 | simprd 465 |
. . . . . . . . . . . 12
              
      
          
                  |
62 | | simprr 766 |
. . . . . . . . . . . 12
              
      
          
            
     |
63 | 3, 4, 5, 38, 41, 43, 44, 49, 58, 50, 48, 60, 61, 62 | tgcgrextend 24529 |
. . . . . . . . . . 11
              
      
          
                  |
64 | | tgcgrxfr.2 |
. . . . . . . . . . . . 13
       |
65 | 64 | ad7antr 744 |
. . . . . . . . . . . 12
              
      
          
                  |
66 | 65 | eqcomd 2457 |
. . . . . . . . . . 11
              
      
          
                  |
67 | 3, 4, 5, 38, 41, 49, 50, 40, 44, 51, 54, 55, 57, 63, 66 | tgsegconeq 24530 |
. . . . . . . . . 10
              
      
          
              |
68 | 67 | oveq2d 6306 |
. . . . . . . . 9
              
      
          
                      |
69 | 48, 68 | eleqtrd 2531 |
. . . . . . . 8
              
      
          
                  |
70 | 61 | eqcomd 2457 |
. . . . . . . . 9
              
      
          
                  |
71 | 67 | oveq2d 6306 |
. . . . . . . . . 10
              
      
          
            
     |
72 | 62, 71 | eqtr3d 2487 |
. . . . . . . . 9
              
      
          
                  |
73 | 3, 4, 5, 6, 1, 17,
8, 10, 64 | tgcgrcomlr 24524 |
. . . . . . . . . 10
       |
74 | 73 | ad7antr 744 |
. . . . . . . . 9
              
      
          
                  |
75 | 3, 4, 14, 38, 49, 58, 50, 41, 43, 51, 70, 72, 74 | trgcgr 24561 |
. . . . . . . 8
              
      
          
                          |
76 | 69, 75 | jca 535 |
. . . . . . 7
              
      
          
                                |
77 | 32 | ad2antrr 732 |
. . . . . . . 8
     
    
 
      
          
TarskiG |
78 | 36 | ad2antrr 732 |
. . . . . . . 8
     
    
 
      
          
  |
79 | 17 | ad5antr 740 |
. . . . . . . 8
     
    
 
      
          
  |
80 | 3, 4, 5, 77, 39, 42, 78, 79 | axtgsegcon 24512 |
. . . . . . 7
     
    
 
      
           
            |
81 | 76, 80 | r19.29a 2932 |
. . . . . 6
     
    
 
      
                               |
82 | 81 | ex 436 |
. . . . 5
    
      
      
 
    
                         |
83 | 82 | reximdva 2862 |
. . . 4
          
       
          
                     |
84 | 37, 83 | mpd 15 |
. . 3
          
                           |
85 | 6 | adantr 467 |
. . . 4
 
    
TarskiG |
86 | 10 | adantr 467 |
. . . 4
 
    
  |
87 | 8 | adantr 467 |
. . . 4
 
    
  |
88 | | simpr 463 |
. . . 4
 
    
      |
89 | 3, 4, 5, 85, 86, 87, 88 | tgbtwndiff 24550 |
. . 3
 
    

        |
90 | 84, 89 | r19.29a 2932 |
. 2
 
    

                    |
91 | 3, 1 | tgldimor 24546 |
. 2
     
       |
92 | 31, 90, 91 | mpjaodan 795 |
1
                      |