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	$⊢ φ \to G \in 𝒢_{Tarski}$
	tgbtwnconn1.a	$⊢ φ \to A \in P$
	tgbtwnconn1.b	$⊢ φ \to B \in P$
	tgbtwnconn1.c	$⊢ φ \to C \in P$
	tgbtwnconn1.d	$⊢ φ \to D \in P$
	tgbtwnconn1.1	$⊢ φ \to A \neq B$
	tgbtwnconn1.2	$⊢ φ \to B \in (A I C)$
	tgbtwnconn1.3	$⊢ φ \to B \in (A I D)$
Assertion	tgbtwnconn1	$⊢ φ \to (C \in (A I D) \lor D \in (A I C))$

Proof

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

Metamath Proof Explorer

Theorem tgbtwnconn1

Proof