Metamath Proof Explorer

Theorem tgbtwnintr

Description: Inner transitivity law for betweenness. Left-hand side of Theorem 3.5 of Schwabhauser p. 30. (Contributed by Thierry Arnoux, 18-Mar-2019)

		Ref	Expression
	Hypotheses	tkgeom.p	$⊢ P = {Base}_{G}$
		tkgeom.d	$⊢ \underset{˙}{-} = dist (G)$
		tkgeom.i	$⊢ I = Itv (G)$
		tkgeom.g	$⊢ φ \to G \in 𝒢_{Tarski}$
		tgbtwnintr.1	$⊢ φ \to A \in P$
		tgbtwnintr.2	$⊢ φ \to B \in P$
		tgbtwnintr.3	$⊢ φ \to C \in P$
		tgbtwnintr.4	$⊢ φ \to D \in P$
		tgbtwnintr.5	$⊢ φ \to A \in (B I D)$
		tgbtwnintr.6	$⊢ φ \to B \in (C I D)$
	Assertion	tgbtwnintr	$⊢ φ \to B \in (A I C)$

Proof

Step	Hyp	Ref	Expression
1		tkgeom.p	$⊢ P = {Base}_{G}$
2		tkgeom.d	$⊢ \underset{˙}{-} = dist (G)$
3		tkgeom.i	$⊢ I = Itv (G)$
4		tkgeom.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		tgbtwnintr.1	$⊢ φ \to A \in P$
6		tgbtwnintr.2	$⊢ φ \to B \in P$
7		tgbtwnintr.3	$⊢ φ \to C \in P$
8		tgbtwnintr.4	$⊢ φ \to D \in P$
9		tgbtwnintr.5	$⊢ φ \to A \in (B I D)$
10		tgbtwnintr.6	$⊢ φ \to B \in (C I D)$
11	4	ad2antrr	$⊢ ((φ \land x \in P) \land (x \in (A I C) \land x \in (B I B))) \to G \in 𝒢_{Tarski}$
12	6	ad2antrr	$⊢ ((φ \land x \in P) \land (x \in (A I C) \land x \in (B I B))) \to B \in P$
13		simplr	$⊢ ((φ \land x \in P) \land (x \in (A I C) \land x \in (B I B))) \to x \in P$
14		simprr	$⊢ ((φ \land x \in P) \land (x \in (A I C) \land x \in (B I B))) \to x \in (B I B)$
15	1 2 3 11 12 13 14	axtgbtwnid	$⊢ ((φ \land x \in P) \land (x \in (A I C) \land x \in (B I B))) \to B = x$
16		simprl	$⊢ ((φ \land x \in P) \land (x \in (A I C) \land x \in (B I B))) \to x \in (A I C)$
17	15 16	eqeltrd	$⊢ ((φ \land x \in P) \land (x \in (A I C) \land x \in (B I B))) \to B \in (A I C)$
18	1 2 3 4 6 7 8 5 6 9 10	axtgpasch	$⊢ φ \to \exists x \in P (x \in (A I C) \land x \in (B I B))$
19	17 18	r19.29a	$⊢ φ \to B \in (A I C)$