tgbtwnconn3

Description: Inner connectivity law for betweenness. Theorem 5.3 of Schwabhauser p. 41. (Contributed by Thierry Arnoux, 17-May-2019)

	Ref	Expression
Hypotheses	tgbtwnconn.p	$⊢ P = {Base}_{G}$
	tgbtwnconn.i	$⊢ I = Itv (G)$
	tgbtwnconn.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tgbtwnconn.a	$⊢ φ \to A \in P$
	tgbtwnconn.b	$⊢ φ \to B \in P$
	tgbtwnconn.c	$⊢ φ \to C \in P$
	tgbtwnconn.d	$⊢ φ \to D \in P$
	tgbtwnconn3.1	$⊢ φ \to B \in (A I D)$
	tgbtwnconn3.2	$⊢ φ \to C \in (A I D)$
Assertion	tgbtwnconn3	$⊢ φ \to (B \in (A I C) \lor C \in (A I B))$

Proof

Step	Hyp	Ref	Expression
1		tgbtwnconn.p	$⊢ P = {Base}_{G}$
2		tgbtwnconn.i	$⊢ I = Itv (G)$
3		tgbtwnconn.g	$⊢ φ \to G \in 𝒢_{Tarski}$
4		tgbtwnconn.a	$⊢ φ \to A \in P$
5		tgbtwnconn.b	$⊢ φ \to B \in P$
6		tgbtwnconn.c	$⊢ φ \to C \in P$
7		tgbtwnconn.d	$⊢ φ \to D \in P$
8		tgbtwnconn3.1	$⊢ φ \to B \in (A I D)$
9		tgbtwnconn3.2	$⊢ φ \to C \in (A I D)$
10		eqid	$⊢ dist (G) = dist (G)$
11	3	adantr	$⊢ (φ \land \|P\| = 1) \to G \in 𝒢_{Tarski}$
12	5	adantr	$⊢ (φ \land \|P\| = 1) \to B \in P$
13	4	adantr	$⊢ (φ \land \|P\| = 1) \to A \in P$
14	6	adantr	$⊢ (φ \land \|P\| = 1) \to C \in P$
15		simpr	$⊢ (φ \land \|P\| = 1) \to \|P\| = 1$
16	1 10 2 11 12 13 14 15	tgldim0itv	$⊢ (φ \land \|P\| = 1) \to B \in (A I C)$
17	16	orcd	$⊢ (φ \land \|P\| = 1) \to (B \in (A I C) \lor C \in (A I B))$
18	3	ad3antrrr	$⊢ (((φ \land 2 \leq \|P\|) \land p \in P) \land (A \in (D I p) \land A \neq p)) \to G \in 𝒢_{Tarski}$
19		simplr	$⊢ (((φ \land 2 \leq \|P\|) \land p \in P) \land (A \in (D I p) \land A \neq p)) \to p \in P$
20	4	ad3antrrr	$⊢ (((φ \land 2 \leq \|P\|) \land p \in P) \land (A \in (D I p) \land A \neq p)) \to A \in P$
21	5	ad3antrrr	$⊢ (((φ \land 2 \leq \|P\|) \land p \in P) \land (A \in (D I p) \land A \neq p)) \to B \in P$
22	6	ad3antrrr	$⊢ (((φ \land 2 \leq \|P\|) \land p \in P) \land (A \in (D I p) \land A \neq p)) \to C \in P$
23		simprr	$⊢ (((φ \land 2 \leq \|P\|) \land p \in P) \land (A \in (D I p) \land A \neq p)) \to A \neq p$
24	23	necomd	$⊢ (((φ \land 2 \leq \|P\|) \land p \in P) \land (A \in (D I p) \land A \neq p)) \to p \neq A$
25	7	ad3antrrr	$⊢ (((φ \land 2 \leq \|P\|) \land p \in P) \land (A \in (D I p) \land A \neq p)) \to D \in P$
26	8	ad3antrrr	$⊢ (((φ \land 2 \leq \|P\|) \land p \in P) \land (A \in (D I p) \land A \neq p)) \to B \in (A I D)$
27		simprl	$⊢ (((φ \land 2 \leq \|P\|) \land p \in P) \land (A \in (D I p) \land A \neq p)) \to A \in (D I p)$
28	1 10 2 18 25 20 19 27	tgbtwncom	$⊢ (((φ \land 2 \leq \|P\|) \land p \in P) \land (A \in (D I p) \land A \neq p)) \to A \in (p I D)$
29	1 10 2 18 21 20 19 25 26 28	tgbtwnintr	$⊢ (((φ \land 2 \leq \|P\|) \land p \in P) \land (A \in (D I p) \land A \neq p)) \to A \in (B I p)$
30	1 10 2 18 21 20 19 29	tgbtwncom	$⊢ (((φ \land 2 \leq \|P\|) \land p \in P) \land (A \in (D I p) \land A \neq p)) \to A \in (p I B)$
31	9	ad3antrrr	$⊢ (((φ \land 2 \leq \|P\|) \land p \in P) \land (A \in (D I p) \land A \neq p)) \to C \in (A I D)$
32	1 10 2 18 20 22 25 31	tgbtwncom	$⊢ (((φ \land 2 \leq \|P\|) \land p \in P) \land (A \in (D I p) \land A \neq p)) \to C \in (D I A)$
33	1 10 2 18 25 22 20 19 32 27	tgbtwnexch3	$⊢ (((φ \land 2 \leq \|P\|) \land p \in P) \land (A \in (D I p) \land A \neq p)) \to A \in (C I p)$
34	1 10 2 18 22 20 19 33	tgbtwncom	$⊢ (((φ \land 2 \leq \|P\|) \land p \in P) \land (A \in (D I p) \land A \neq p)) \to A \in (p I C)$
35	1 2 18 19 20 21 22 24 30 34	tgbtwnconn2	$⊢ (((φ \land 2 \leq \|P\|) \land p \in P) \land (A \in (D I p) \land A \neq p)) \to (B \in (A I C) \lor C \in (A I B))$
36	3	adantr	$⊢ (φ \land 2 \leq \|P\|) \to G \in 𝒢_{Tarski}$
37	7	adantr	$⊢ (φ \land 2 \leq \|P\|) \to D \in P$
38	4	adantr	$⊢ (φ \land 2 \leq \|P\|) \to A \in P$
39		simpr	$⊢ (φ \land 2 \leq \|P\|) \to 2 \leq \|P\|$
40	1 10 2 36 37 38 39	tgbtwndiff	$⊢ (φ \land 2 \leq \|P\|) \to \exists p \in P (A \in (D I p) \land A \neq p)$
41	35 40	r19.29a	$⊢ (φ \land 2 \leq \|P\|) \to (B \in (A I C) \lor C \in (A I B))$
42	1 4	tgldimor	$⊢ φ \to (\|P\| = 1 \lor 2 \leq \|P\|)$
43	17 41 42	mpjaodan	$⊢ φ \to (B \in (A I C) \lor C \in (A I B))$

Metamath Proof Explorer

Theorem tgbtwnconn3

Proof