Step | Hyp | Ref
| Expression |
1 | | tgbtwncgr.p |
. . 3
     |
2 | | tgbtwncgr.m |
. . 3
     |
3 | | tgbtwncgr.i |
. . 3
Itv   |
4 | | tgbtwncgr.g |
. . . 4

TarskiG |
5 | 4 | adantr 465 |
. . 3
 
     TarskiG |
6 | | tgbtwncgr.b |
. . . 4
   |
7 | 6 | adantr 465 |
. . 3
 
       |
8 | | tgbtwncgr.d |
. . . 4
   |
9 | 8 | adantr 465 |
. . 3
 
       |
10 | | tgifscgr.f |
. . . 4
   |
11 | 10 | adantr 465 |
. . 3
 
       |
12 | | simpr 461 |
. . 3
 
           |
13 | | tgifscgr.h |
. . . 4
   |
14 | 13 | adantr 465 |
. . 3
 
       |
15 | 1, 2, 3, 5, 7, 9, 11, 12, 14 | tgldim0cgr 23078 |
. 2
 
           |
16 | 4 | ad2antrr 725 |
. . . . . . 7
         TarskiG |
17 | | tgbtwncgr.c |
. . . . . . . 8
   |
18 | 17 | ad2antrr 725 |
. . . . . . 7
           |
19 | 6 | ad2antrr 725 |
. . . . . . 7
           |
20 | | tgifscgr.1 |
. . . . . . . . 9
       |
21 | 20 | ad2antrr 725 |
. . . . . . . 8
               |
22 | | simpr 461 |
. . . . . . . . 9
           |
23 | 22 | oveq1d 6207 |
. . . . . . . 8
                   |
24 | 21, 23 | eleqtrd 2541 |
. . . . . . 7
               |
25 | 1, 2, 3, 16, 18, 19, 24 | axtgbtwnid 23045 |
. . . . . 6
           |
26 | 25 | oveq1d 6207 |
. . . . 5
               |
27 | | tgifscgr.6 |
. . . . . 6
       |
28 | 27 | ad2antrr 725 |
. . . . 5
               |
29 | 26, 28 | eqtr3d 2494 |
. . . 4
               |
30 | | tgifscgr.g |
. . . . . . 7
   |
31 | 30 | ad2antrr 725 |
. . . . . 6
           |
32 | 10 | ad2antrr 725 |
. . . . . 6
           |
33 | | tgifscgr.2 |
. . . . . . . 8
       |
34 | 33 | ad2antrr 725 |
. . . . . . 7
               |
35 | | tgifscgr.e |
. . . . . . . . . 10
   |
36 | 35 | ad2antrr 725 |
. . . . . . . . 9
           |
37 | | tgbtwncgr.a |
. . . . . . . . . 10
   |
38 | 37 | ad2antrr 725 |
. . . . . . . . 9
           |
39 | 22 | oveq2d 6208 |
. . . . . . . . . 10
               |
40 | | tgifscgr.3 |
. . . . . . . . . . 11
       |
41 | 40 | ad2antrr 725 |
. . . . . . . . . 10
               |
42 | 39, 41 | eqtr2d 2493 |
. . . . . . . . 9
               |
43 | 1, 2, 3, 16, 36, 31, 38, 42 | axtgcgrid 23042 |
. . . . . . . 8
           |
44 | 43 | oveq1d 6207 |
. . . . . . 7
                   |
45 | 34, 44 | eleqtrd 2541 |
. . . . . 6
               |
46 | 1, 2, 3, 16, 31, 32, 45 | axtgbtwnid 23045 |
. . . . 5
           |
47 | 46 | oveq1d 6207 |
. . . 4
               |
48 | 29, 47 | eqtrd 2492 |
. . 3
               |
49 | 4 | ad2antrr 725 |
. . . . . . . 8
         TarskiG |
50 | 49 | ad2antrr 725 |
. . . . . . 7
    
       
      TarskiG |
51 | 50 | ad2antrr 725 |
. . . . . 6
              
      
          
TarskiG |
52 | | simp-4r 766 |
. . . . . 6
              
      
             |
53 | 17 | ad2antrr 725 |
. . . . . . . 8
           |
54 | 53 | ad2antrr 725 |
. . . . . . 7
    
       
        |
55 | 54 | ad2antrr 725 |
. . . . . 6
              
      
          
  |
56 | 6 | ad6antr 735 |
. . . . . 6
              
      
          
  |
57 | | simplr 754 |
. . . . . 6
              
      
             |
58 | 30 | ad4antr 731 |
. . . . . . 7
    
       
        |
59 | 58 | ad2antrr 725 |
. . . . . 6
              
      
          
  |
60 | 10 | ad6antr 735 |
. . . . . 6
              
      
          
  |
61 | 8 | ad6antr 735 |
. . . . . 6
              
      
          
  |
62 | 13 | ad6antr 735 |
. . . . . 6
              
      
          
  |
63 | | simpllr 758 |
. . . . . . . 8
              
      
                   |
64 | 63 | simprd 463 |
. . . . . . 7
              
      
             |
65 | 64 | necomd 2719 |
. . . . . 6
              
      
             |
66 | 37 | ad2antrr 725 |
. . . . . . . . 9
           |
67 | 66 | ad4antr 731 |
. . . . . . . 8
              
      
          
  |
68 | 20 | ad6antr 735 |
. . . . . . . 8
              
      
          
      |
69 | 63 | simpld 459 |
. . . . . . . 8
              
      
          
      |
70 | 1, 2, 3, 51, 67, 56, 55, 52, 68, 69 | tgbtwnexch3 23067 |
. . . . . . 7
              
      
          
      |
71 | 1, 2, 3, 51, 56, 55, 52, 70 | tgbtwncom 23061 |
. . . . . 6
              
      
          
      |
72 | 35 | ad6antr 735 |
. . . . . . . 8
              
      
          
  |
73 | 33 | ad6antr 735 |
. . . . . . . 8
              
      
          
      |
74 | | simprl 755 |
. . . . . . . 8
              
      
          
      |
75 | 1, 2, 3, 51, 72, 60, 59, 57, 73, 74 | tgbtwnexch3 23067 |
. . . . . . 7
              
      
          
      |
76 | 1, 2, 3, 51, 60, 59, 57, 75 | tgbtwncom 23061 |
. . . . . 6
              
      
          
      |
77 | | simprr 756 |
. . . . . . . 8
              
      
                 |
78 | 77 | eqcomd 2459 |
. . . . . . 7
              
      
                 |
79 | 1, 2, 3, 51, 55, 52, 59, 57, 78 | tgcgrcomlr 23053 |
. . . . . 6
              
      
                 |
80 | | tgifscgr.4 |
. . . . . . . 8
       |
81 | 80 | ad6antr 735 |
. . . . . . 7
              
      
                 |
82 | 1, 2, 3, 51, 56, 55, 60, 59, 81 | tgcgrcomlr 23053 |
. . . . . 6
              
      
                 |
83 | | simp-5r 768 |
. . . . . . 7
              
      
             |
84 | 40 | ad6antr 735 |
. . . . . . 7
              
      
                 |
85 | | tgifscgr.5 |
. . . . . . . 8
       |
86 | 85 | ad6antr 735 |
. . . . . . 7
              
      
                 |
87 | 27 | ad6antr 735 |
. . . . . . 7
              
      
                 |
88 | 1, 2, 3, 51, 67, 55, 52, 72, 59, 57, 61, 62, 83, 69, 74, 84, 78, 86, 87 | axtg5seg 23044 |
. . . . . 6
              
      
                 |
89 | 1, 2, 3, 51, 52, 55, 56, 57, 59, 60, 61, 62, 65, 71, 76, 79, 82, 88, 87 | axtg5seg 23044 |
. . . . 5
              
      
                 |
90 | 35 | ad4antr 731 |
. . . . . 6
    
       
        |
91 | | simplr 754 |
. . . . . 6
    
       
        |
92 | 1, 2, 3, 50, 90, 58, 54, 91 | axtgsegcon 23043 |
. . . . 5
    
       
       
           |
93 | 89, 92 | r19.29a 2960 |
. . . 4
    
       
            |
94 | | simplr 754 |
. . . . 5
               |
95 | 1, 2, 3, 49, 66, 53, 94 | tgbtwndiff 23079 |
. . . 4
         
        |
96 | 93, 95 | r19.29a 2960 |
. . 3
               |
97 | | exmidne 2654 |
. . . 4
   |
98 | 97 | a1i 11 |
. . 3
 
    

   |
99 | 48, 96, 98 | mpjaodan 784 |
. 2
 
    
      |
100 | 1, 37 | tgldimor 23075 |
. 2
     
       |
101 | 15, 99, 100 | mpjaodan 784 |
1
       |