Step | Hyp | Ref
| Expression |
1 | | simpllr 774 |
. . . . . . . 8
                              
                      
                       |
2 | 1 | simpld 465 |
. . . . . . 7
                              
                            |
3 | 2 | adantr 471 |
. . . . . 6
     
 
                       
                      
      |
4 | | simpr 467 |
. . . . . . 7
     
 
                       
                      
  |
5 | 4 | oveq2d 6331 |
. . . . . 6
     
 
                       
                                 |
6 | 3, 5 | eleqtrrd 2543 |
. . . . 5
     
 
                       
                      
      |
7 | 6 | olcd 399 |
. . . 4
     
 
                       
                                   |
8 | | simprl 769 |
. . . . . . 7
                              
                            |
9 | 8 | adantr 471 |
. . . . . 6
     
 
                       
                      
      |
10 | | simpr 467 |
. . . . . . 7
     
 
                       
                      
  |
11 | 10 | oveq2d 6331 |
. . . . . 6
     
 
                       
                                 |
12 | 9, 11 | eleqtrrd 2543 |
. . . . 5
     
 
                       
                      
      |
13 | 12 | orcd 398 |
. . . 4
     
 
                       
                                   |
14 | | df-ne 2635 |
. . . . . 6

  |
15 | | tgbtwnconn1.p |
. . . . . . . . . . 11
     |
16 | | tgbtwnconn1.i |
. . . . . . . . . . 11
Itv   |
17 | | tgbtwnconn1.g |
. . . . . . . . . . . . 13

TarskiG |
18 | 17 | ad4antr 743 |
. . . . . . . . . . . 12
                              
                      TarskiG |
19 | 18 | ad7antr 749 |
. . . . . . . . . . 11
           
                         
                                               
                            
     
TarskiG |
20 | | tgbtwnconn1.a |
. . . . . . . . . . . . 13
   |
21 | 20 | ad4antr 743 |
. . . . . . . . . . . 12
                              
                        |
22 | 21 | ad7antr 749 |
. . . . . . . . . . 11
           
                         
                                               
                            
     
  |
23 | | tgbtwnconn1.b |
. . . . . . . . . . . . 13
   |
24 | 23 | ad4antr 743 |
. . . . . . . . . . . 12
                              
                        |
25 | 24 | ad7antr 749 |
. . . . . . . . . . 11
           
                         
                                               
                            
     
  |
26 | | tgbtwnconn1.c |
. . . . . . . . . . . . 13
   |
27 | 26 | ad4antr 743 |
. . . . . . . . . . . 12
                              
                        |
28 | 27 | ad7antr 749 |
. . . . . . . . . . 11
           
                         
                                               
                            
     
  |
29 | | tgbtwnconn1.d |
. . . . . . . . . . . . 13
   |
30 | 29 | ad4antr 743 |
. . . . . . . . . . . 12
                              
                        |
31 | 30 | ad7antr 749 |
. . . . . . . . . . 11
           
                         
                                               
                            
     
  |
32 | | simp-11l 795 |
. . . . . . . . . . . 12
           
                         
                                               
                            
     
  |
33 | | tgbtwnconn1.1 |
. . . . . . . . . . . 12
   |
34 | 32, 33 | syl 17 |
. . . . . . . . . . 11
           
                         
                                               
                            
     
  |
35 | | tgbtwnconn1.2 |
. . . . . . . . . . . 12
       |
36 | 32, 35 | syl 17 |
. . . . . . . . . . 11
           
                         
                                               
                            
     
      |
37 | | tgbtwnconn1.3 |
. . . . . . . . . . . 12
       |
38 | 32, 37 | syl 17 |
. . . . . . . . . . 11
           
                         
                                               
                            
     
      |
39 | | eqid 2462 |
. . . . . . . . . . 11
         |
40 | | simp-4r 782 |
. . . . . . . . . . . 12
                              
                        |
41 | 40 | ad7antr 749 |
. . . . . . . . . . 11
           
                         
                                               
                            
     
  |
42 | | simplr 767 |
. . . . . . . . . . . 12
                              
                        |
43 | 42 | ad7antr 749 |
. . . . . . . . . . 11
           
                         
                                               
                            
     
  |
44 | | simp-6r 786 |
. . . . . . . . . . 11
           
                         
                                               
                            
     
  |
45 | | simp-4r 782 |
. . . . . . . . . . 11
           
                         
                                               
                            
     
  |
46 | 2 | ad7antr 749 |
. . . . . . . . . . 11
           
                         
                                               
                            
     
      |
47 | 8 | ad7antr 749 |
. . . . . . . . . . 11
           
                         
                                               
                            
     
      |
48 | | simp-5r 784 |
. . . . . . . . . . . 12
           
                         
                                               
                            
     
                        |
49 | 48 | simpld 465 |
. . . . . . . . . . 11
           
                         
                                               
                            
     
      |
50 | | simpllr 774 |
. . . . . . . . . . . 12
           
                         
                                               
                            
     
                        |
51 | 50 | simpld 465 |
. . . . . . . . . . 11
           
                         
                                               
                            
     
      |
52 | 1 | simprd 469 |
. . . . . . . . . . . . 13
                              
                                        |
53 | 52 | ad7antr 749 |
. . . . . . . . . . . 12
           
                         
                                               
                            
     
                  |
54 | 15, 39, 16, 19, 31, 41, 31, 28, 53 | tgcgrcomlr 24573 |
. . . . . . . . . . 11
           
                         
                                               
                            
     
                  |
55 | | simprr 771 |
. . . . . . . . . . . 12
                              
                                        |
56 | 55 | ad7antr 749 |
. . . . . . . . . . 11
           
                         
                                               
                            
     
                  |
57 | 48 | simprd 469 |
. . . . . . . . . . 11
           
                         
                                               
                            
     
                  |
58 | 50 | simprd 469 |
. . . . . . . . . . 11
           
                         
                                               
                            
     
                  |
59 | | simplr 767 |
. . . . . . . . . . 11
           
                         
                                               
                            
     
  |
60 | | simprl 769 |
. . . . . . . . . . 11
           
                         
                                               
                            
     
      |
61 | | simprr 771 |
. . . . . . . . . . 11
           
                         
                                               
                            
     
      |
62 | | simp-7r 788 |
. . . . . . . . . . 11
           
                         
                                               
                            
     
  |
63 | 15, 16, 19, 22, 25, 28, 31, 34, 36, 38, 39, 41, 43, 44, 45, 46, 47, 49, 51, 54, 56, 57, 58, 59, 60, 61, 62 | tgbtwnconn1lem3 24668 |
. . . . . . . . . 10
           
                         
                                               
                            
     
  |
64 | 15, 39, 16, 18, 21, 27, 42, 8 | tgbtwncom 24581 |
. . . . . . . . . . . 12
                              
                            |
65 | 15, 39, 16, 18, 21, 30, 40, 2 | tgbtwncom 24581 |
. . . . . . . . . . . 12
                              
                            |
66 | 15, 39, 16, 18, 42, 40, 21, 27, 30, 64, 65 | axtgpasch 24564 |
. . . . . . . . . . 11
                              
                      
            |
67 | 66 | ad5antr 745 |
. . . . . . . . . 10
         
 
                       
                                               
                       
            |
68 | 63, 67 | r19.29a 2944 |
. . . . . . . . 9
         
 
                       
                                               
                         |
69 | 15, 39, 16, 18, 21, 42, 24, 30 | axtgsegcon 24561 |
. . . . . . . . . 10
                              
                      
                        |
70 | 69 | ad3antrrr 741 |
. . . . . . . . 9
       
                         
                                                                        |
71 | 68, 70 | r19.29a 2944 |
. . . . . . . 8
       
                         
                                                 |
72 | 15, 39, 16, 18, 21, 40, 24, 27 | axtgsegcon 24561 |
. . . . . . . . 9
                              
                      
                        |
73 | 72 | adantr 471 |
. . . . . . . 8
     
 
                       
                       
                        |
74 | 71, 73 | r19.29a 2944 |
. . . . . . 7
     
 
                       
                         |
75 | 74 | ex 440 |
. . . . . 6
                              
                          |
76 | 14, 75 | syl5bir 226 |
. . . . 5
                              
                      
   |
77 | 76 | orrd 384 |
. . . 4
                              
                      
   |
78 | 7, 13, 77 | mpjaodan 800 |
. . 3
                              
                      
           |
79 | 15, 39, 16, 17, 20, 26, 26, 29 | axtgsegcon 24561 |
. . . 4
  
                       |
80 | 79 | ad2antrr 737 |
. . 3
    
                      
                        |
81 | 78, 80 | r19.29a 2944 |
. 2
    
                      
           |
82 | 15, 39, 16, 17, 20, 29, 29, 26 | axtgsegcon 24561 |
. 2
  
                       |
83 | 81, 82 | r19.29a 2944 |
1
             |