Metamath Proof Explorer

Theorem tgbtwnconn1

Description: Connectivity law for betweenness. Theorem 5.1 of Schwabhauser p. 39-41. In earlier presentations of Tarski's axioms, this theorem appeared as an additional axiom. It was derived from the other axioms by Gupta, 1965. (Contributed by Thierry Arnoux, 30-Apr-2019)

Ref Expression
Hypotheses tgbtwnconn1.p 
|- P = ( Base ` G )
tgbtwnconn1.i 
|- I = ( Itv ` G )
tgbtwnconn1.g 
|- ( ph -> G e. TarskiG )
tgbtwnconn1.a 
|- ( ph -> A e. P )
tgbtwnconn1.b 
|- ( ph -> B e. P )
tgbtwnconn1.c 
|- ( ph -> C e. P )
tgbtwnconn1.d 
|- ( ph -> D e. P )
tgbtwnconn1.1 
|- ( ph -> A =/= B )
tgbtwnconn1.2 
|- ( ph -> B e. ( A I C ) )
tgbtwnconn1.3 
|- ( ph -> B e. ( A I D ) )
Assertion tgbtwnconn1 
|- ( ph -> ( C e. ( A I D ) \/ D e. ( A I C ) ) )

Proof

Step Hyp Ref Expression
1 tgbtwnconn1.p 
 |-  P = ( Base ` G )
2 tgbtwnconn1.i 
 |-  I = ( Itv ` G )
3 tgbtwnconn1.g 
 |-  ( ph -> G e. TarskiG )
4 tgbtwnconn1.a 
 |-  ( ph -> A e. P )
5 tgbtwnconn1.b 
 |-  ( ph -> B e. P )
6 tgbtwnconn1.c 
 |-  ( ph -> C e. P )
7 tgbtwnconn1.d 
 |-  ( ph -> D e. P )
8 tgbtwnconn1.1 
 |-  ( ph -> A =/= B )
9 tgbtwnconn1.2 
 |-  ( ph -> B e. ( A I C ) )
10 tgbtwnconn1.3 
 |-  ( ph -> B e. ( A I D ) )
11 simpllr 
 |-  ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) -> ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) )
12 11 simpld 
 |-  ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) -> D e. ( A I e ) )
13 12 adantr 
 |-  ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C = e ) -> D e. ( A I e ) )
14 simpr 
 |-  ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C = e ) -> C = e )
15 14 oveq2d 
 |-  ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C = e ) -> ( A I C ) = ( A I e ) )
16 13 15 eleqtrrd 
 |-  ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C = e ) -> D e. ( A I C ) )
17 16 olcd 
 |-  ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C = e ) -> ( C e. ( A I D ) \/ D e. ( A I C ) ) )
18 simprl 
 |-  ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) -> C e. ( A I f ) )
19 18 adantr 
 |-  ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ D = f ) -> C e. ( A I f ) )
20 simpr 
 |-  ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ D = f ) -> D = f )
21 20 oveq2d 
 |-  ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ D = f ) -> ( A I D ) = ( A I f ) )
22 19 21 eleqtrrd 
 |-  ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ D = f ) -> C e. ( A I D ) )
23 22 orcd 
 |-  ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ D = f ) -> ( C e. ( A I D ) \/ D e. ( A I C ) ) )
24 df-ne 
 |-  ( C =/= e <-> -. C = e )
25 3 ad4antr 
 |-  ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) -> G e. TarskiG )
26 25 ad7antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) /\ h e. P ) /\ ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) ) /\ j e. P ) /\ ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) ) /\ x e. P ) /\ ( x e. ( C I e ) /\ x e. ( D I f ) ) ) -> G e. TarskiG )
27 4 ad4antr 
 |-  ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) -> A e. P )
28 27 ad7antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) /\ h e. P ) /\ ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) ) /\ j e. P ) /\ ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) ) /\ x e. P ) /\ ( x e. ( C I e ) /\ x e. ( D I f ) ) ) -> A e. P )
29 5 ad4antr 
 |-  ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) -> B e. P )
30 29 ad7antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) /\ h e. P ) /\ ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) ) /\ j e. P ) /\ ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) ) /\ x e. P ) /\ ( x e. ( C I e ) /\ x e. ( D I f ) ) ) -> B e. P )
31 6 ad4antr 
 |-  ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) -> C e. P )
32 31 ad7antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) /\ h e. P ) /\ ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) ) /\ j e. P ) /\ ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) ) /\ x e. P ) /\ ( x e. ( C I e ) /\ x e. ( D I f ) ) ) -> C e. P )
33 7 ad4antr 
 |-  ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) -> D e. P )
34 33 ad7antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) /\ h e. P ) /\ ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) ) /\ j e. P ) /\ ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) ) /\ x e. P ) /\ ( x e. ( C I e ) /\ x e. ( D I f ) ) ) -> D e. P )
35 simp-11l 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) /\ h e. P ) /\ ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) ) /\ j e. P ) /\ ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) ) /\ x e. P ) /\ ( x e. ( C I e ) /\ x e. ( D I f ) ) ) -> ph )
36 35 8 syl 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) /\ h e. P ) /\ ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) ) /\ j e. P ) /\ ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) ) /\ x e. P ) /\ ( x e. ( C I e ) /\ x e. ( D I f ) ) ) -> A =/= B )
37 35 9 syl 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) /\ h e. P ) /\ ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) ) /\ j e. P ) /\ ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) ) /\ x e. P ) /\ ( x e. ( C I e ) /\ x e. ( D I f ) ) ) -> B e. ( A I C ) )
38 35 10 syl 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) /\ h e. P ) /\ ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) ) /\ j e. P ) /\ ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) ) /\ x e. P ) /\ ( x e. ( C I e ) /\ x e. ( D I f ) ) ) -> B e. ( A I D ) )
39 eqid 
 |-  ( dist ` G ) = ( dist ` G )
40 simp-4r 
 |-  ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) -> e e. P )
41 40 ad7antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) /\ h e. P ) /\ ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) ) /\ j e. P ) /\ ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) ) /\ x e. P ) /\ ( x e. ( C I e ) /\ x e. ( D I f ) ) ) -> e e. P )
42 simplr 
 |-  ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) -> f e. P )
43 42 ad7antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) /\ h e. P ) /\ ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) ) /\ j e. P ) /\ ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) ) /\ x e. P ) /\ ( x e. ( C I e ) /\ x e. ( D I f ) ) ) -> f e. P )
44 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) /\ h e. P ) /\ ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) ) /\ j e. P ) /\ ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) ) /\ x e. P ) /\ ( x e. ( C I e ) /\ x e. ( D I f ) ) ) -> h e. P )
45 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) /\ h e. P ) /\ ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) ) /\ j e. P ) /\ ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) ) /\ x e. P ) /\ ( x e. ( C I e ) /\ x e. ( D I f ) ) ) -> j e. P )
46 12 ad7antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) /\ h e. P ) /\ ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) ) /\ j e. P ) /\ ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) ) /\ x e. P ) /\ ( x e. ( C I e ) /\ x e. ( D I f ) ) ) -> D e. ( A I e ) )
47 18 ad7antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) /\ h e. P ) /\ ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) ) /\ j e. P ) /\ ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) ) /\ x e. P ) /\ ( x e. ( C I e ) /\ x e. ( D I f ) ) ) -> C e. ( A I f ) )
48 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) /\ h e. P ) /\ ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) ) /\ j e. P ) /\ ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) ) /\ x e. P ) /\ ( x e. ( C I e ) /\ x e. ( D I f ) ) ) -> ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) )
49 48 simpld 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) /\ h e. P ) /\ ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) ) /\ j e. P ) /\ ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) ) /\ x e. P ) /\ ( x e. ( C I e ) /\ x e. ( D I f ) ) ) -> e e. ( A I h ) )
50 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) /\ h e. P ) /\ ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) ) /\ j e. P ) /\ ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) ) /\ x e. P ) /\ ( x e. ( C I e ) /\ x e. ( D I f ) ) ) -> ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) )
51 50 simpld 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) /\ h e. P ) /\ ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) ) /\ j e. P ) /\ ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) ) /\ x e. P ) /\ ( x e. ( C I e ) /\ x e. ( D I f ) ) ) -> f e. ( A I j ) )
52 11 simprd 
 |-  ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) -> ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) )
53 52 ad7antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) /\ h e. P ) /\ ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) ) /\ j e. P ) /\ ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) ) /\ x e. P ) /\ ( x e. ( C I e ) /\ x e. ( D I f ) ) ) -> ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) )
54 1 39 2 26 34 41 34 32 53 tgcgrcomlr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) /\ h e. P ) /\ ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) ) /\ j e. P ) /\ ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) ) /\ x e. P ) /\ ( x e. ( C I e ) /\ x e. ( D I f ) ) ) -> ( e ( dist ` G ) D ) = ( C ( dist ` G ) D ) )
55 simprr 
 |-  ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) -> ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) )
56 55 ad7antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) /\ h e. P ) /\ ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) ) /\ j e. P ) /\ ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) ) /\ x e. P ) /\ ( x e. ( C I e ) /\ x e. ( D I f ) ) ) -> ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) )
57 48 simprd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) /\ h e. P ) /\ ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) ) /\ j e. P ) /\ ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) ) /\ x e. P ) /\ ( x e. ( C I e ) /\ x e. ( D I f ) ) ) -> ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) )
58 50 simprd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) /\ h e. P ) /\ ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) ) /\ j e. P ) /\ ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) ) /\ x e. P ) /\ ( x e. ( C I e ) /\ x e. ( D I f ) ) ) -> ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) )
59 simplr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) /\ h e. P ) /\ ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) ) /\ j e. P ) /\ ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) ) /\ x e. P ) /\ ( x e. ( C I e ) /\ x e. ( D I f ) ) ) -> x e. P )
60 simprl 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) /\ h e. P ) /\ ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) ) /\ j e. P ) /\ ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) ) /\ x e. P ) /\ ( x e. ( C I e ) /\ x e. ( D I f ) ) ) -> x e. ( C I e ) )
61 simprr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) /\ h e. P ) /\ ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) ) /\ j e. P ) /\ ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) ) /\ x e. P ) /\ ( x e. ( C I e ) /\ x e. ( D I f ) ) ) -> x e. ( D I f ) )
62 simp-7r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) /\ h e. P ) /\ ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) ) /\ j e. P ) /\ ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) ) /\ x e. P ) /\ ( x e. ( C I e ) /\ x e. ( D I f ) ) ) -> C =/= e )
63 1 2 26 28 30 32 34 36 37 38 39 41 43 44 45 46 47 49 51 54 56 57 58 59 60 61 62 tgbtwnconn1lem3 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) /\ h e. P ) /\ ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) ) /\ j e. P ) /\ ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) ) /\ x e. P ) /\ ( x e. ( C I e ) /\ x e. ( D I f ) ) ) -> D = f )
64 1 39 2 25 27 31 42 18 tgbtwncom 
 |-  ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) -> C e. ( f I A ) )
65 1 39 2 25 27 33 40 12 tgbtwncom 
 |-  ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) -> D e. ( e I A ) )
66 1 39 2 25 42 40 27 31 33 64 65 axtgpasch 
 |-  ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) -> E. x e. P ( x e. ( C I e ) /\ x e. ( D I f ) ) )
67 66 ad5antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) /\ h e. P ) /\ ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) ) /\ j e. P ) /\ ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) ) -> E. x e. P ( x e. ( C I e ) /\ x e. ( D I f ) ) )
68 63 67 r19.29a 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) /\ h e. P ) /\ ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) ) /\ j e. P ) /\ ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) ) -> D = f )
69 1 39 2 25 27 42 29 33 axtgsegcon 
 |-  ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) -> E. j e. P ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) )
70 69 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) /\ h e. P ) /\ ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) ) -> E. j e. P ( f e. ( A I j ) /\ ( f ( dist ` G ) j ) = ( B ( dist ` G ) D ) ) )
71 68 70 r19.29a 
 |-  ( ( ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) /\ h e. P ) /\ ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) ) -> D = f )
72 1 39 2 25 27 40 29 31 axtgsegcon 
 |-  ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) -> E. h e. P ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) )
73 72 adantr 
 |-  ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) -> E. h e. P ( e e. ( A I h ) /\ ( e ( dist ` G ) h ) = ( B ( dist ` G ) C ) ) )
74 71 73 r19.29a 
 |-  ( ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) /\ C =/= e ) -> D = f )
75 74 ex 
 |-  ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) -> ( C =/= e -> D = f ) )
76 24 75 biimtrrid 
 |-  ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) -> ( -. C = e -> D = f ) )
77 76 orrd 
 |-  ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) -> ( C = e \/ D = f ) )
78 17 23 77 mpjaodan 
 |-  ( ( ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) /\ f e. P ) /\ ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) ) -> ( C e. ( A I D ) \/ D e. ( A I C ) ) )
79 1 39 2 3 4 6 6 7 axtgsegcon 
 |-  ( ph -> E. f e. P ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) )
80 79 ad2antrr 
 |-  ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) -> E. f e. P ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) )
81 78 80 r19.29a 
 |-  ( ( ( ph /\ e e. P ) /\ ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) ) -> ( C e. ( A I D ) \/ D e. ( A I C ) ) )
82 1 39 2 3 4 7 7 6 axtgsegcon 
 |-  ( ph -> E. e e. P ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) )
83 81 82 r19.29a 
 |-  ( ph -> ( C e. ( A I D ) \/ D e. ( A I C ) ) )