tgbtwnconn2

Description: Another connectivity law for betweenness. Theorem 5.2 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$
	tgbtwnconn2.1	$⊢ φ \to A \neq B$
	tgbtwnconn2.2	$⊢ φ \to B \in (A I C)$
	tgbtwnconn2.3	$⊢ φ \to B \in (A I D)$
Assertion	tgbtwnconn2	$⊢ φ \to (C \in (B I D) \lor D \in (B I C))$

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		tgbtwnconn2.1	$⊢ φ \to A \neq B$
9		tgbtwnconn2.2	$⊢ φ \to B \in (A I C)$
10		tgbtwnconn2.3	$⊢ φ \to B \in (A I D)$
11		eqid	$⊢ dist (G) = dist (G)$
12	3	adantr	$⊢ (φ \land C \in (A I D)) \to G \in 𝒢_{Tarski}$
13	4	adantr	$⊢ (φ \land C \in (A I D)) \to A \in P$
14	5	adantr	$⊢ (φ \land C \in (A I D)) \to B \in P$
15	6	adantr	$⊢ (φ \land C \in (A I D)) \to C \in P$
16	7	adantr	$⊢ (φ \land C \in (A I D)) \to D \in P$
17	9	adantr	$⊢ (φ \land C \in (A I D)) \to B \in (A I C)$
18		simpr	$⊢ (φ \land C \in (A I D)) \to C \in (A I D)$
19	1 11 2 12 13 14 15 16 17 18	tgbtwnexch3	$⊢ (φ \land C \in (A I D)) \to C \in (B I D)$
20	19	orcd	$⊢ (φ \land C \in (A I D)) \to (C \in (B I D) \lor D \in (B I C))$
21	3	adantr	$⊢ (φ \land D \in (A I C)) \to G \in 𝒢_{Tarski}$
22	4	adantr	$⊢ (φ \land D \in (A I C)) \to A \in P$
23	5	adantr	$⊢ (φ \land D \in (A I C)) \to B \in P$
24	7	adantr	$⊢ (φ \land D \in (A I C)) \to D \in P$
25	6	adantr	$⊢ (φ \land D \in (A I C)) \to C \in P$
26	10	adantr	$⊢ (φ \land D \in (A I C)) \to B \in (A I D)$
27		simpr	$⊢ (φ \land D \in (A I C)) \to D \in (A I C)$
28	1 11 2 21 22 23 24 25 26 27	tgbtwnexch3	$⊢ (φ \land D \in (A I C)) \to D \in (B I C)$
29	28	olcd	$⊢ (φ \land D \in (A I C)) \to (C \in (B I D) \lor D \in (B I C))$
30	1 2 3 4 5 6 7 8 9 10	tgbtwnconn1	$⊢ φ \to (C \in (A I D) \lor D \in (A I C))$
31	20 29 30	mpjaodan	$⊢ φ \to (C \in (B I D) \lor D \in (B I C))$

Metamath Proof Explorer

Theorem tgbtwnconn2

Proof