segletr

Description: Segment less than is transitive. Theorem 5.8 of Schwabhauser p. 42. (Contributed by Scott Fenton, 11-Oct-2013)

		Ref	Expression
	Assertion	segletr	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to ((⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩ \land ⟨C, D⟩ {Seg}_{\leq} ⟨E, F⟩) \to ⟨A, B⟩ {Seg}_{\leq} ⟨E, F⟩)$

Proof

Step	Hyp	Ref	Expression
1		simprll	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (z Btwn ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩))) \to y Btwn ⟨C, D⟩$
2		simprrr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (z Btwn ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩))) \to ⟨C, D⟩ Cgr ⟨E, z⟩$
3	1 2	jca	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (z Btwn ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩))) \to (y Btwn ⟨C, D⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩)$
4		simpl1	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \to N \in ℕ$
5		simpl23	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \to C \in 𝔼 (N)$
6		simprl	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \to y \in 𝔼 (N)$
7		simpl31	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \to D \in 𝔼 (N)$
8		simpl32	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \to E \in 𝔼 (N)$
9		simprr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \to z \in 𝔼 (N)$
10		cgrxfr	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land y \in 𝔼 (N) \land D \in 𝔼 (N)) \land (E \in 𝔼 (N) \land z \in 𝔼 (N))) \to ((y Btwn ⟨C, D⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩) \to \exists w \in 𝔼 (N) (w Btwn ⟨E, z⟩ \land ⟨C, ⟨y, D⟩⟩ Cgr3 ⟨E, ⟨w, z⟩⟩))$
11	4 5 6 7 8 9 10	syl132anc	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \to ((y Btwn ⟨C, D⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩) \to \exists w \in 𝔼 (N) (w Btwn ⟨E, z⟩ \land ⟨C, ⟨y, D⟩⟩ Cgr3 ⟨E, ⟨w, z⟩⟩))$
12	11	adantr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (z Btwn ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩))) \to ((y Btwn ⟨C, D⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩) \to \exists w \in 𝔼 (N) (w Btwn ⟨E, z⟩ \land ⟨C, ⟨y, D⟩⟩ Cgr3 ⟨E, ⟨w, z⟩⟩))$
13	3 12	mpd	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (z Btwn ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩))) \to \exists w \in 𝔼 (N) (w Btwn ⟨E, z⟩ \land ⟨C, ⟨y, D⟩⟩ Cgr3 ⟨E, ⟨w, z⟩⟩)$
14		anass	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \land w \in 𝔼 (N)) \leftrightarrow ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((y \in 𝔼 (N) \land z \in 𝔼 (N)) \land w \in 𝔼 (N)))$
15		df-3an	$⊢ (y \in 𝔼 (N) \land z \in 𝔼 (N) \land w \in 𝔼 (N)) \leftrightarrow ((y \in 𝔼 (N) \land z \in 𝔼 (N)) \land w \in 𝔼 (N))$
16	15	anbi2i	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N) \land w \in 𝔼 (N))) \leftrightarrow ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((y \in 𝔼 (N) \land z \in 𝔼 (N)) \land w \in 𝔼 (N)))$
17	14 16	bitr4i	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \land w \in 𝔼 (N)) \leftrightarrow ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N) \land w \in 𝔼 (N)))$
18		simpl1	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N) \land w \in 𝔼 (N))) \to N \in ℕ$
19		simpl23	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N) \land w \in 𝔼 (N))) \to C \in 𝔼 (N)$
20		simpr1	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N) \land w \in 𝔼 (N))) \to y \in 𝔼 (N)$
21		simpl31	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N) \land w \in 𝔼 (N))) \to D \in 𝔼 (N)$
22		simpl32	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N) \land w \in 𝔼 (N))) \to E \in 𝔼 (N)$
23		simpr3	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N) \land w \in 𝔼 (N))) \to w \in 𝔼 (N)$
24		simpr2	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N) \land w \in 𝔼 (N))) \to z \in 𝔼 (N)$
25		brcgr3	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land y \in 𝔼 (N) \land D \in 𝔼 (N)) \land (E \in 𝔼 (N) \land w \in 𝔼 (N) \land z \in 𝔼 (N))) \to (⟨C, ⟨y, D⟩⟩ Cgr3 ⟨E, ⟨w, z⟩⟩ \leftrightarrow (⟨C, y⟩ Cgr ⟨E, w⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩ \land ⟨y, D⟩ Cgr ⟨w, z⟩))$
26	18 19 20 21 22 23 24 25	syl133anc	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N) \land w \in 𝔼 (N))) \to (⟨C, ⟨y, D⟩⟩ Cgr3 ⟨E, ⟨w, z⟩⟩ \leftrightarrow (⟨C, y⟩ Cgr ⟨E, w⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩ \land ⟨y, D⟩ Cgr ⟨w, z⟩))$
27	26	anbi2d	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N) \land w \in 𝔼 (N))) \to ((w Btwn ⟨E, z⟩ \land ⟨C, ⟨y, D⟩⟩ Cgr3 ⟨E, ⟨w, z⟩⟩) \leftrightarrow (w Btwn ⟨E, z⟩ \land (⟨C, y⟩ Cgr ⟨E, w⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩ \land ⟨y, D⟩ Cgr ⟨w, z⟩)))$
28	27	adantr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N) \land w \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (z Btwn ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩))) \to ((w Btwn ⟨E, z⟩ \land ⟨C, ⟨y, D⟩⟩ Cgr3 ⟨E, ⟨w, z⟩⟩) \leftrightarrow (w Btwn ⟨E, z⟩ \land (⟨C, y⟩ Cgr ⟨E, w⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩ \land ⟨y, D⟩ Cgr ⟨w, z⟩)))$
29		df-3an	$⊢ ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (z Btwn ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩) \land (w Btwn ⟨E, z⟩ \land (⟨C, y⟩ Cgr ⟨E, w⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩ \land ⟨y, D⟩ Cgr ⟨w, z⟩))) \leftrightarrow (((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (z Btwn ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩)) \land (w Btwn ⟨E, z⟩ \land (⟨C, y⟩ Cgr ⟨E, w⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩ \land ⟨y, D⟩ Cgr ⟨w, z⟩)))$
30		simpl33	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N) \land w \in 𝔼 (N))) \to F \in 𝔼 (N)$
31		simpr3l	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N) \land w \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (z Btwn ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩) \land (w Btwn ⟨E, z⟩ \land (⟨C, y⟩ Cgr ⟨E, w⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩ \land ⟨y, D⟩ Cgr ⟨w, z⟩)))) \to w Btwn ⟨E, z⟩$
32		simpr2l	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N) \land w \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (z Btwn ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩) \land (w Btwn ⟨E, z⟩ \land (⟨C, y⟩ Cgr ⟨E, w⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩ \land ⟨y, D⟩ Cgr ⟨w, z⟩)))) \to z Btwn ⟨E, F⟩$
33	18 22 23 24 30 31 32	btwnexchand	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N) \land w \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (z Btwn ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩) \land (w Btwn ⟨E, z⟩ \land (⟨C, y⟩ Cgr ⟨E, w⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩ \land ⟨y, D⟩ Cgr ⟨w, z⟩)))) \to w Btwn ⟨E, F⟩$
34		simpl21	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N) \land w \in 𝔼 (N))) \to A \in 𝔼 (N)$
35		simpl22	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N) \land w \in 𝔼 (N))) \to B \in 𝔼 (N)$
36		simpr1r	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N) \land w \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (z Btwn ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩) \land (w Btwn ⟨E, z⟩ \land (⟨C, y⟩ Cgr ⟨E, w⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩ \land ⟨y, D⟩ Cgr ⟨w, z⟩)))) \to ⟨A, B⟩ Cgr ⟨C, y⟩$
37		simp3r1	$⊢ ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (z Btwn ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩) \land (w Btwn ⟨E, z⟩ \land (⟨C, y⟩ Cgr ⟨E, w⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩ \land ⟨y, D⟩ Cgr ⟨w, z⟩))) \to ⟨C, y⟩ Cgr ⟨E, w⟩$
38	37	adantl	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N) \land w \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (z Btwn ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩) \land (w Btwn ⟨E, z⟩ \land (⟨C, y⟩ Cgr ⟨E, w⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩ \land ⟨y, D⟩ Cgr ⟨w, z⟩)))) \to ⟨C, y⟩ Cgr ⟨E, w⟩$
39	18 34 35 19 20 22 23 36 38	cgrtrand	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N) \land w \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (z Btwn ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩) \land (w Btwn ⟨E, z⟩ \land (⟨C, y⟩ Cgr ⟨E, w⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩ \land ⟨y, D⟩ Cgr ⟨w, z⟩)))) \to ⟨A, B⟩ Cgr ⟨E, w⟩$
40	33 39	jca	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N) \land w \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (z Btwn ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩) \land (w Btwn ⟨E, z⟩ \land (⟨C, y⟩ Cgr ⟨E, w⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩ \land ⟨y, D⟩ Cgr ⟨w, z⟩)))) \to (w Btwn ⟨E, F⟩ \land ⟨A, B⟩ Cgr ⟨E, w⟩)$
41	29 40	sylan2br	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N) \land w \in 𝔼 (N))) \land (((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (z Btwn ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩)) \land (w Btwn ⟨E, z⟩ \land (⟨C, y⟩ Cgr ⟨E, w⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩ \land ⟨y, D⟩ Cgr ⟨w, z⟩)))) \to (w Btwn ⟨E, F⟩ \land ⟨A, B⟩ Cgr ⟨E, w⟩)$
42	41	expr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N) \land w \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (z Btwn ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩))) \to ((w Btwn ⟨E, z⟩ \land (⟨C, y⟩ Cgr ⟨E, w⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩ \land ⟨y, D⟩ Cgr ⟨w, z⟩)) \to (w Btwn ⟨E, F⟩ \land ⟨A, B⟩ Cgr ⟨E, w⟩))$
43	28 42	sylbid	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N) \land w \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (z Btwn ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩))) \to ((w Btwn ⟨E, z⟩ \land ⟨C, ⟨y, D⟩⟩ Cgr3 ⟨E, ⟨w, z⟩⟩) \to (w Btwn ⟨E, F⟩ \land ⟨A, B⟩ Cgr ⟨E, w⟩))$
44	17 43	sylanb	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \land w \in 𝔼 (N)) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (z Btwn ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩))) \to ((w Btwn ⟨E, z⟩ \land ⟨C, ⟨y, D⟩⟩ Cgr3 ⟨E, ⟨w, z⟩⟩) \to (w Btwn ⟨E, F⟩ \land ⟨A, B⟩ Cgr ⟨E, w⟩))$
45	44	an32s	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (z Btwn ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩))) \land w \in 𝔼 (N)) \to ((w Btwn ⟨E, z⟩ \land ⟨C, ⟨y, D⟩⟩ Cgr3 ⟨E, ⟨w, z⟩⟩) \to (w Btwn ⟨E, F⟩ \land ⟨A, B⟩ Cgr ⟨E, w⟩))$
46	45	reximdva	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (z Btwn ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩))) \to (\exists w \in 𝔼 (N) (w Btwn ⟨E, z⟩ \land ⟨C, ⟨y, D⟩⟩ Cgr3 ⟨E, ⟨w, z⟩⟩) \to \exists w \in 𝔼 (N) (w Btwn ⟨E, F⟩ \land ⟨A, B⟩ Cgr ⟨E, w⟩))$
47	13 46	mpd	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land (y \in 𝔼 (N) \land z \in 𝔼 (N))) \land ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (z Btwn ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩))) \to \exists w \in 𝔼 (N) (w Btwn ⟨E, F⟩ \land ⟨A, B⟩ Cgr ⟨E, w⟩)$
48	47	exp31	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to ((y \in 𝔼 (N) \land z \in 𝔼 (N)) \to (((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (z Btwn ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩)) \to \exists w \in 𝔼 (N) (w Btwn ⟨E, F⟩ \land ⟨A, B⟩ Cgr ⟨E, w⟩)))$
49	48	rexlimdvv	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to (\exists y \in 𝔼 (N) \exists z \in 𝔼 (N) ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (z Btwn ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩)) \to \exists w \in 𝔼 (N) (w Btwn ⟨E, F⟩ \land ⟨A, B⟩ Cgr ⟨E, w⟩))$
50		simp1	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to N \in ℕ$
51		simp21	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to A \in 𝔼 (N)$
52		simp22	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to B \in 𝔼 (N)$
53		simp23	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to C \in 𝔼 (N)$
54		simp31	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to D \in 𝔼 (N)$
55		brsegle	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩ \leftrightarrow \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))$
56	50 51 52 53 54 55	syl122anc	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to (⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩ \leftrightarrow \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))$
57		simp32	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to E \in 𝔼 (N)$
58		simp33	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to F \in 𝔼 (N)$
59		brsegle	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land (E \in 𝔼 (N) \land F \in 𝔼 (N))) \to (⟨C, D⟩ {Seg}_{\leq} ⟨E, F⟩ \leftrightarrow \exists z \in 𝔼 (N) (z Btwn ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩))$
60	50 53 54 57 58 59	syl122anc	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to (⟨C, D⟩ {Seg}_{\leq} ⟨E, F⟩ \leftrightarrow \exists z \in 𝔼 (N) (z Btwn ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩))$
61	56 60	anbi12d	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to ((⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩ \land ⟨C, D⟩ {Seg}_{\leq} ⟨E, F⟩) \leftrightarrow (\exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land \exists z \in 𝔼 (N) (z Btwn ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩)))$
62		reeanv	$⊢ \exists y \in 𝔼 (N) \exists z \in 𝔼 (N) ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (z Btwn ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩)) \leftrightarrow (\exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land \exists z \in 𝔼 (N) (z Btwn ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩))$
63	61 62	bitr4di	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to ((⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩ \land ⟨C, D⟩ {Seg}_{\leq} ⟨E, F⟩) \leftrightarrow \exists y \in 𝔼 (N) \exists z \in 𝔼 (N) ((y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \land (z Btwn ⟨E, F⟩ \land ⟨C, D⟩ Cgr ⟨E, z⟩)))$
64		brsegle	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (E \in 𝔼 (N) \land F \in 𝔼 (N))) \to (⟨A, B⟩ {Seg}_{\leq} ⟨E, F⟩ \leftrightarrow \exists w \in 𝔼 (N) (w Btwn ⟨E, F⟩ \land ⟨A, B⟩ Cgr ⟨E, w⟩))$
65	50 51 52 57 58 64	syl122anc	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to (⟨A, B⟩ {Seg}_{\leq} ⟨E, F⟩ \leftrightarrow \exists w \in 𝔼 (N) (w Btwn ⟨E, F⟩ \land ⟨A, B⟩ Cgr ⟨E, w⟩))$
66	49 63 65	3imtr4d	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to ((⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩ \land ⟨C, D⟩ {Seg}_{\leq} ⟨E, F⟩) \to ⟨A, B⟩ {Seg}_{\leq} ⟨E, F⟩)$

Metamath Proof Explorer

Theorem segletr

Proof