Theorem tgbtwnconn1 24669

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.)

Hypotheses

Ref	Expression
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

Ref	Expression
tgbtwnconn1	|- ( ph -> ( C e. ( A I D ) \/ D e. ( A I C ) ) )

Proof of Theorem tgbtwnconn1

Dummy variables e f h j x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpllr 774	. . . . . . . 8 |- ( ( ( ( ( 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 ) ) )
2	1	simpld 465	. . . . . . 7 |- ( ( ( ( ( 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 ) )
3	2	adantr 471	. . . . . 6 |- ( ( ( ( ( ( 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 ) )
4		simpr 467	. . . . . . 7 |- ( ( ( ( ( ( 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 )
5	4	oveq2d 6331	. . . . . 6 |- ( ( ( ( ( ( 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 ) )
6	3, 5	eleqtrrd 2543	. . . . 5 |- ( ( ( ( ( ( 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 ) )
7	6	olcd 399	. . . 4 |- ( ( ( ( ( ( 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 ) ) )
8		simprl 769	. . . . . . 7 |- ( ( ( ( ( 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 ) )
9	8	adantr 471	. . . . . 6 |- ( ( ( ( ( ( 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 ) )
10		simpr 467	. . . . . . 7 |- ( ( ( ( ( ( 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 )
11	10	oveq2d 6331	. . . . . 6 |- ( ( ( ( ( ( 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 ) )
12	9, 11	eleqtrrd 2543	. . . . 5 |- ( ( ( ( ( ( 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 ) )
13	12	orcd 398	. . . 4 |- ( ( ( ( ( ( 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 ) ) )
14		df-ne 2635	. . . . . 6 |- ( C =/= e <-> -. C = e )
15		tgbtwnconn1.p	. . . . . . . . . . 11 |- P = ( Base ` G )
16		tgbtwnconn1.i	. . . . . . . . . . 11 |- I = (Itv ` G )
17		tgbtwnconn1.g	. . . . . . . . . . . . 13 |- ( ph -> G e. TarskiG )
18	17	ad4antr 743	. . . . . . . . . . . 12 |- ( ( ( ( ( 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 )
19	18	ad7antr 749	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 )
20		tgbtwnconn1.a	. . . . . . . . . . . . 13 |- ( ph -> A e. P )
21	20	ad4antr 743	. . . . . . . . . . . 12 |- ( ( ( ( ( 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 )
22	21	ad7antr 749	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 )
23		tgbtwnconn1.b	. . . . . . . . . . . . 13 |- ( ph -> B e. P )
24	23	ad4antr 743	. . . . . . . . . . . 12 |- ( ( ( ( ( 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 )
25	24	ad7antr 749	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 )
26		tgbtwnconn1.c	. . . . . . . . . . . . 13 |- ( ph -> C e. P )
27	26	ad4antr 743	. . . . . . . . . . . 12 |- ( ( ( ( ( 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 )
28	27	ad7antr 749	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 )
29		tgbtwnconn1.d	. . . . . . . . . . . . 13 |- ( ph -> D e. P )
30	29	ad4antr 743	. . . . . . . . . . . 12 |- ( ( ( ( ( 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 )
31	30	ad7antr 749	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 )
32		simp-11l 795	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 )
33		tgbtwnconn1.1	. . . . . . . . . . . 12 |- ( ph -> A =/= B )
34	32, 33	syl 17	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 )
35		tgbtwnconn1.2	. . . . . . . . . . . 12 |- ( ph -> B e. ( A I C ) )
36	32, 35	syl 17	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 ) )
37		tgbtwnconn1.3	. . . . . . . . . . . 12 |- ( ph -> B e. ( A I D ) )
38	32, 37	syl 17	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 2462	. . . . . . . . . . 11 |- ( dist ` G ) = ( dist ` G )
40		simp-4r 782	. . . . . . . . . . . 12 |- ( ( ( ( ( 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 749	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 767	. . . . . . . . . . . 12 |- ( ( ( ( ( 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 749	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 786	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 782	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( ( 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	2	ad7antr 749	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( ( 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	8	ad7antr 749	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 784	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 465	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 774	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 465	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( ( 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	1	simprd 469	. . . . . . . . . . . . 13 |- ( ( ( ( ( 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 749	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( ( ( ( ( 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	15, 39, 16, 19, 31, 41, 31, 28, 53	tgcgrcomlr 24573	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 771	. . . . . . . . . . . 12 |- ( ( ( ( ( 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 749	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 469	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 469	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 767	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 769	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 771	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 788	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( ( 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	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 |- ( ( ( ( ( ( ( ( ( ( ( ( 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	15, 39, 16, 18, 21, 27, 42, 8	tgbtwncom 24581	. . . . . . . . . . . 12 |- ( ( ( ( ( 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	15, 39, 16, 18, 21, 30, 40, 2	tgbtwncom 24581	. . . . . . . . . . . 12 |- ( ( ( ( ( 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	15, 39, 16, 18, 42, 40, 21, 27, 30, 64, 65	axtgpasch 24564	. . . . . . . . . . 11 |- ( ( ( ( ( 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 745	. . . . . . . . . 10 |- ( ( ( ( ( ( ( ( ( ( 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 2944	. . . . . . . . 9 |- ( ( ( ( ( ( ( ( ( ( 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	15, 39, 16, 18, 21, 42, 24, 30	axtgsegcon 24561	. . . . . . . . . 10 |- ( ( ( ( ( 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 741	. . . . . . . . 9 |- ( ( ( ( ( ( ( ( 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 2944	. . . . . . . 8 |- ( ( ( ( ( ( ( ( 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	15, 39, 16, 18, 21, 40, 24, 27	axtgsegcon 24561	. . . . . . . . 9 |- ( ( ( ( ( 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 471	. . . . . . . 8 |- ( ( ( ( ( ( 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 2944	. . . . . . 7 |- ( ( ( ( ( ( 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 440	. . . . . 6 |- ( ( ( ( ( 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	14, 75	syl5bir 226	. . . . 5 |- ( ( ( ( ( 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 384	. . . 4 |- ( ( ( ( ( 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	7, 13, 77	mpjaodan 800	. . 3 |- ( ( ( ( ( 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	15, 39, 16, 17, 20, 26, 26, 29	axtgsegcon 24561	. . . 4 |- ( ph -> E. f e. P ( C e. ( A I f ) /\ ( C ( dist ` G ) f ) = ( C ( dist ` G ) D ) ) )
80	79	ad2antrr 737	. . 3 |- ( ( ( 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 2944	. 2 |- ( ( ( 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	15, 39, 16, 17, 20, 29, 29, 26	axtgsegcon 24561	. 2 |- ( ph -> E. e e. P ( D e. ( A I e ) /\ ( D ( dist ` G ) e ) = ( D ( dist ` G ) C ) ) )
83	81, 82	r19.29a 2944	1 |- ( ph -> ( C e. ( A I D ) \/ D e. ( A I C ) ) )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 374   /\ wa 375   = wceq 1455   e. wcel 1898   =/= wne 2633   E.wrex 2750   ` cfv 5601  (class class class)co 6315   Basecbs 15170   distcds 15248  TarskiGcstrkg 24527  Itvcitv 24533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4529  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-cnex 9621  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641  ax-pre-mulgt0 9642

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-om 6720  df-1st 6820  df-2nd 6821  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-1o 7208  df-oadd 7212  df-er 7389  df-pm 7501  df-en 7596  df-dom 7597  df-sdom 7598  df-fin 7599  df-card 8399  df-cda 8624  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-sub 9888  df-neg 9889  df-nn 10638  df-2 10696  df-3 10697  df-n0 10899  df-z 10967  df-uz 11189  df-fz 11814  df-fzo 11947  df-hash 12548  df-word 12697  df-concat 12699  df-s1 12700  df-s2 12981  df-s3 12982  df-trkgc 24545  df-trkgb 24546  df-trkgcb 24547  df-trkg 24550  df-cgrg 24605

This theorem is referenced by:  tgbtwnconn2  24670  tgbtwnconnln1  24674  hltr  24704  hlbtwn  24705