btwnouttr2

Description: Outer transitivity law for betweenness. Left-hand side of Theorem 3.1 of Schwabhauser p. 30. (Contributed by Scott Fenton, 12-Jun-2013)

		Ref	Expression
	Assertion	btwnouttr2	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to ((B \neq C \land B Btwn ⟨A, C⟩ \land C Btwn ⟨B, D⟩) \to C Btwn ⟨A, D⟩)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to N \in ℕ$
2		simp2l	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to A \in 𝔼 (N)$
3		simp3l	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to C \in 𝔼 (N)$
4		simp3r	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to D \in 𝔼 (N)$
5		axsegcon	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land C \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to \exists x \in 𝔼 (N) (C Btwn ⟨A, x⟩ \land ⟨C, x⟩ Cgr ⟨C, D⟩)$
6	1 2 3 3 4 5	syl122anc	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to \exists x \in 𝔼 (N) (C Btwn ⟨A, x⟩ \land ⟨C, x⟩ Cgr ⟨C, D⟩)$
7	6	adantr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (B \neq C \land B Btwn ⟨A, C⟩ \land C Btwn ⟨B, D⟩)) \to \exists x \in 𝔼 (N) (C Btwn ⟨A, x⟩ \land ⟨C, x⟩ Cgr ⟨C, D⟩)$
8		simprrl	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land ((B \neq C \land B Btwn ⟨A, C⟩ \land C Btwn ⟨B, D⟩) \land (C Btwn ⟨A, x⟩ \land ⟨C, x⟩ Cgr ⟨C, D⟩))) \to C Btwn ⟨A, x⟩$
9		simprl1	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land ((B \neq C \land B Btwn ⟨A, C⟩ \land C Btwn ⟨B, D⟩) \land (C Btwn ⟨A, x⟩ \land ⟨C, x⟩ Cgr ⟨C, D⟩))) \to B \neq C$
10		simpl2	$⊢ ((B \neq C \land B Btwn ⟨A, C⟩ \land C Btwn ⟨B, D⟩) \land (C Btwn ⟨A, x⟩ \land ⟨C, x⟩ Cgr ⟨C, D⟩)) \to B Btwn ⟨A, C⟩$
11		simprl	$⊢ ((B \neq C \land B Btwn ⟨A, C⟩ \land C Btwn ⟨B, D⟩) \land (C Btwn ⟨A, x⟩ \land ⟨C, x⟩ Cgr ⟨C, D⟩)) \to C Btwn ⟨A, x⟩$
12	10 11	jca	$⊢ ((B \neq C \land B Btwn ⟨A, C⟩ \land C Btwn ⟨B, D⟩) \land (C Btwn ⟨A, x⟩ \land ⟨C, x⟩ Cgr ⟨C, D⟩)) \to (B Btwn ⟨A, C⟩ \land C Btwn ⟨A, x⟩)$
13	12	adantl	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land ((B \neq C \land B Btwn ⟨A, C⟩ \land C Btwn ⟨B, D⟩) \land (C Btwn ⟨A, x⟩ \land ⟨C, x⟩ Cgr ⟨C, D⟩))) \to (B Btwn ⟨A, C⟩ \land C Btwn ⟨A, x⟩)$
14		simpl1	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to N \in ℕ$
15		simpl2l	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to A \in 𝔼 (N)$
16		simpl2r	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to B \in 𝔼 (N)$
17		simpl3l	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to C \in 𝔼 (N)$
18		simpr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to x \in 𝔼 (N)$
19		btwnexch3	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land x \in 𝔼 (N))) \to ((B Btwn ⟨A, C⟩ \land C Btwn ⟨A, x⟩) \to C Btwn ⟨B, x⟩)$
20	14 15 16 17 18 19	syl122anc	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to ((B Btwn ⟨A, C⟩ \land C Btwn ⟨A, x⟩) \to C Btwn ⟨B, x⟩)$
21	20	adantr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land ((B \neq C \land B Btwn ⟨A, C⟩ \land C Btwn ⟨B, D⟩) \land (C Btwn ⟨A, x⟩ \land ⟨C, x⟩ Cgr ⟨C, D⟩))) \to ((B Btwn ⟨A, C⟩ \land C Btwn ⟨A, x⟩) \to C Btwn ⟨B, x⟩)$
22	13 21	mpd	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land ((B \neq C \land B Btwn ⟨A, C⟩ \land C Btwn ⟨B, D⟩) \land (C Btwn ⟨A, x⟩ \land ⟨C, x⟩ Cgr ⟨C, D⟩))) \to C Btwn ⟨B, x⟩$
23		simprrr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land ((B \neq C \land B Btwn ⟨A, C⟩ \land C Btwn ⟨B, D⟩) \land (C Btwn ⟨A, x⟩ \land ⟨C, x⟩ Cgr ⟨C, D⟩))) \to ⟨C, x⟩ Cgr ⟨C, D⟩$
24	22 23	jca	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land ((B \neq C \land B Btwn ⟨A, C⟩ \land C Btwn ⟨B, D⟩) \land (C Btwn ⟨A, x⟩ \land ⟨C, x⟩ Cgr ⟨C, D⟩))) \to (C Btwn ⟨B, x⟩ \land ⟨C, x⟩ Cgr ⟨C, D⟩)$
25		simprl3	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land ((B \neq C \land B Btwn ⟨A, C⟩ \land C Btwn ⟨B, D⟩) \land (C Btwn ⟨A, x⟩ \land ⟨C, x⟩ Cgr ⟨C, D⟩))) \to C Btwn ⟨B, D⟩$
26		simpl3r	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to D \in 𝔼 (N)$
27	14 17 26	cgrrflxd	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to ⟨C, D⟩ Cgr ⟨C, D⟩$
28	27	adantr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land ((B \neq C \land B Btwn ⟨A, C⟩ \land C Btwn ⟨B, D⟩) \land (C Btwn ⟨A, x⟩ \land ⟨C, x⟩ Cgr ⟨C, D⟩))) \to ⟨C, D⟩ Cgr ⟨C, D⟩$
29	25 28	jca	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land ((B \neq C \land B Btwn ⟨A, C⟩ \land C Btwn ⟨B, D⟩) \land (C Btwn ⟨A, x⟩ \land ⟨C, x⟩ Cgr ⟨C, D⟩))) \to (C Btwn ⟨B, D⟩ \land ⟨C, D⟩ Cgr ⟨C, D⟩)$
30		segconeq	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land C \in 𝔼 (N) \land D \in 𝔼 (N)) \land (B \in 𝔼 (N) \land x \in 𝔼 (N) \land D \in 𝔼 (N))) \to ((B \neq C \land (C Btwn ⟨B, x⟩ \land ⟨C, x⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨B, D⟩ \land ⟨C, D⟩ Cgr ⟨C, D⟩)) \to x = D)$
31	14 17 17 26 16 18 26 30	syl133anc	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to ((B \neq C \land (C Btwn ⟨B, x⟩ \land ⟨C, x⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨B, D⟩ \land ⟨C, D⟩ Cgr ⟨C, D⟩)) \to x = D)$
32	31	adantr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land ((B \neq C \land B Btwn ⟨A, C⟩ \land C Btwn ⟨B, D⟩) \land (C Btwn ⟨A, x⟩ \land ⟨C, x⟩ Cgr ⟨C, D⟩))) \to ((B \neq C \land (C Btwn ⟨B, x⟩ \land ⟨C, x⟩ Cgr ⟨C, D⟩) \land (C Btwn ⟨B, D⟩ \land ⟨C, D⟩ Cgr ⟨C, D⟩)) \to x = D)$
33	9 24 29 32	mp3and	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land ((B \neq C \land B Btwn ⟨A, C⟩ \land C Btwn ⟨B, D⟩) \land (C Btwn ⟨A, x⟩ \land ⟨C, x⟩ Cgr ⟨C, D⟩))) \to x = D$
34	33	opeq2d	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land ((B \neq C \land B Btwn ⟨A, C⟩ \land C Btwn ⟨B, D⟩) \land (C Btwn ⟨A, x⟩ \land ⟨C, x⟩ Cgr ⟨C, D⟩))) \to ⟨A, x⟩ = ⟨A, D⟩$
35	8 34	breqtrd	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land ((B \neq C \land B Btwn ⟨A, C⟩ \land C Btwn ⟨B, D⟩) \land (C Btwn ⟨A, x⟩ \land ⟨C, x⟩ Cgr ⟨C, D⟩))) \to C Btwn ⟨A, D⟩$
36	35	expr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \land (B \neq C \land B Btwn ⟨A, C⟩ \land C Btwn ⟨B, D⟩)) \to ((C Btwn ⟨A, x⟩ \land ⟨C, x⟩ Cgr ⟨C, D⟩) \to C Btwn ⟨A, D⟩)$
37	36	an32s	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (B \neq C \land B Btwn ⟨A, C⟩ \land C Btwn ⟨B, D⟩)) \land x \in 𝔼 (N)) \to ((C Btwn ⟨A, x⟩ \land ⟨C, x⟩ Cgr ⟨C, D⟩) \to C Btwn ⟨A, D⟩)$
38	37	rexlimdva	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (B \neq C \land B Btwn ⟨A, C⟩ \land C Btwn ⟨B, D⟩)) \to (\exists x \in 𝔼 (N) (C Btwn ⟨A, x⟩ \land ⟨C, x⟩ Cgr ⟨C, D⟩) \to C Btwn ⟨A, D⟩)$
39	7 38	mpd	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land (B \neq C \land B Btwn ⟨A, C⟩ \land C Btwn ⟨B, D⟩)) \to C Btwn ⟨A, D⟩$
40	39	ex	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to ((B \neq C \land B Btwn ⟨A, C⟩ \land C Btwn ⟨B, D⟩) \to C Btwn ⟨A, D⟩)$

Metamath Proof Explorer

Theorem btwnouttr2

Proof