tgbtwnconn22

Description: Double connectivity law for betweenness. (Contributed by Thierry Arnoux, 1-Dec-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$
	tgbtwnconn22.e	$⊢ φ \to E \in P$
	tgbtwnconn22.1	$⊢ φ \to A \neq B$
	tgbtwnconn22.2	$⊢ φ \to C \neq B$
	tgbtwnconn22.3	$⊢ φ \to B \in (A I C)$
	tgbtwnconn22.4	$⊢ φ \to B \in (A I D)$
	tgbtwnconn22.5	$⊢ φ \to B \in (C I E)$
Assertion	tgbtwnconn22	$⊢ φ \to B \in (D I E)$

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

Metamath Proof Explorer

Theorem tgbtwnconn22

Proof