outsideofeq

Description: Uniqueness law for OutsideOf . Analogue of segconeq . (Contributed by Scott Fenton, 24-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	outsideofeq	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to (((A OutsideOf ⟨X, R⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A OutsideOf ⟨Y, R⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩)) \to X = Y)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to N \in ℕ$
2		simp21	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to A \in 𝔼 (N)$
3		simp32	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to X \in 𝔼 (N)$
4		simp22	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to R \in 𝔼 (N)$
5		broutsideof2	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land X \in 𝔼 (N) \land R \in 𝔼 (N))) \to (A OutsideOf ⟨X, R⟩ \leftrightarrow (X \neq A \land R \neq A \land (X Btwn ⟨A, R⟩ \lor R Btwn ⟨A, X⟩)))$
6	1 2 3 4 5	syl13anc	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to (A OutsideOf ⟨X, R⟩ \leftrightarrow (X \neq A \land R \neq A \land (X Btwn ⟨A, R⟩ \lor R Btwn ⟨A, X⟩)))$
7	6	anbi1d	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to ((A OutsideOf ⟨X, R⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \leftrightarrow ((X \neq A \land R \neq A \land (X Btwn ⟨A, R⟩ \lor R Btwn ⟨A, X⟩)) \land ⟨A, X⟩ Cgr ⟨B, C⟩))$
8		simp33	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to Y \in 𝔼 (N)$
9		broutsideof2	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land Y \in 𝔼 (N) \land R \in 𝔼 (N))) \to (A OutsideOf ⟨Y, R⟩ \leftrightarrow (Y \neq A \land R \neq A \land (Y Btwn ⟨A, R⟩ \lor R Btwn ⟨A, Y⟩)))$
10	1 2 8 4 9	syl13anc	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to (A OutsideOf ⟨Y, R⟩ \leftrightarrow (Y \neq A \land R \neq A \land (Y Btwn ⟨A, R⟩ \lor R Btwn ⟨A, Y⟩)))$
11	10	anbi1d	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to ((A OutsideOf ⟨Y, R⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩) \leftrightarrow ((Y \neq A \land R \neq A \land (Y Btwn ⟨A, R⟩ \lor R Btwn ⟨A, Y⟩)) \land ⟨A, Y⟩ Cgr ⟨B, C⟩))$
12	7 11	anbi12d	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to (((A OutsideOf ⟨X, R⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A OutsideOf ⟨Y, R⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩)) \leftrightarrow (((X \neq A \land R \neq A \land (X Btwn ⟨A, R⟩ \lor R Btwn ⟨A, X⟩)) \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land ((Y \neq A \land R \neq A \land (Y Btwn ⟨A, R⟩ \lor R Btwn ⟨A, Y⟩)) \land ⟨A, Y⟩ Cgr ⟨B, C⟩)))$
13		simpll3	$⊢ (((X \neq A \land R \neq A \land (X Btwn ⟨A, R⟩ \lor R Btwn ⟨A, X⟩)) \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land ((Y \neq A \land R \neq A \land (Y Btwn ⟨A, R⟩ \lor R Btwn ⟨A, Y⟩)) \land ⟨A, Y⟩ Cgr ⟨B, C⟩)) \to (X Btwn ⟨A, R⟩ \lor R Btwn ⟨A, X⟩)$
14		simprl3	$⊢ (((X \neq A \land R \neq A \land (X Btwn ⟨A, R⟩ \lor R Btwn ⟨A, X⟩)) \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land ((Y \neq A \land R \neq A \land (Y Btwn ⟨A, R⟩ \lor R Btwn ⟨A, Y⟩)) \land ⟨A, Y⟩ Cgr ⟨B, C⟩)) \to (Y Btwn ⟨A, R⟩ \lor R Btwn ⟨A, Y⟩)$
15	13 14	jca	$⊢ (((X \neq A \land R \neq A \land (X Btwn ⟨A, R⟩ \lor R Btwn ⟨A, X⟩)) \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land ((Y \neq A \land R \neq A \land (Y Btwn ⟨A, R⟩ \lor R Btwn ⟨A, Y⟩)) \land ⟨A, Y⟩ Cgr ⟨B, C⟩)) \to ((X Btwn ⟨A, R⟩ \lor R Btwn ⟨A, X⟩) \land (Y Btwn ⟨A, R⟩ \lor R Btwn ⟨A, Y⟩))$
16	15	adantl	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (((X \neq A \land R \neq A \land (X Btwn ⟨A, R⟩ \lor R Btwn ⟨A, X⟩)) \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land ((Y \neq A \land R \neq A \land (Y Btwn ⟨A, R⟩ \lor R Btwn ⟨A, Y⟩)) \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to ((X Btwn ⟨A, R⟩ \lor R Btwn ⟨A, X⟩) \land (Y Btwn ⟨A, R⟩ \lor R Btwn ⟨A, Y⟩))$
17		simpll2	$⊢ (((X \neq A \land R \neq A \land (X Btwn ⟨A, R⟩ \lor R Btwn ⟨A, X⟩)) \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land ((Y \neq A \land R \neq A \land (Y Btwn ⟨A, R⟩ \lor R Btwn ⟨A, Y⟩)) \land ⟨A, Y⟩ Cgr ⟨B, C⟩)) \to R \neq A$
18	17	adantl	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (((X \neq A \land R \neq A \land (X Btwn ⟨A, R⟩ \lor R Btwn ⟨A, X⟩)) \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land ((Y \neq A \land R \neq A \land (Y Btwn ⟨A, R⟩ \lor R Btwn ⟨A, Y⟩)) \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to R \neq A$
19		simp23	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to B \in 𝔼 (N)$
20		simp31	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to C \in 𝔼 (N)$
21		simprlr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (((X \neq A \land R \neq A \land (X Btwn ⟨A, R⟩ \lor R Btwn ⟨A, X⟩)) \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land ((Y \neq A \land R \neq A \land (Y Btwn ⟨A, R⟩ \lor R Btwn ⟨A, Y⟩)) \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to ⟨A, X⟩ Cgr ⟨B, C⟩$
22		simprrr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (((X \neq A \land R \neq A \land (X Btwn ⟨A, R⟩ \lor R Btwn ⟨A, X⟩)) \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land ((Y \neq A \land R \neq A \land (Y Btwn ⟨A, R⟩ \lor R Btwn ⟨A, Y⟩)) \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to ⟨A, Y⟩ Cgr ⟨B, C⟩$
23	1 2 3 2 8 19 20 21 22	cgrtr3and	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (((X \neq A \land R \neq A \land (X Btwn ⟨A, R⟩ \lor R Btwn ⟨A, X⟩)) \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land ((Y \neq A \land R \neq A \land (Y Btwn ⟨A, R⟩ \lor R Btwn ⟨A, Y⟩)) \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to ⟨A, X⟩ Cgr ⟨A, Y⟩$
24	16 18 23	jca32	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (((X \neq A \land R \neq A \land (X Btwn ⟨A, R⟩ \lor R Btwn ⟨A, X⟩)) \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land ((Y \neq A \land R \neq A \land (Y Btwn ⟨A, R⟩ \lor R Btwn ⟨A, Y⟩)) \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to (((X Btwn ⟨A, R⟩ \lor R Btwn ⟨A, X⟩) \land (Y Btwn ⟨A, R⟩ \lor R Btwn ⟨A, Y⟩)) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩))$
25		simprll	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land ((X Btwn ⟨A, R⟩ \land Y Btwn ⟨A, R⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩))) \to X Btwn ⟨A, R⟩$
26		simprlr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land ((X Btwn ⟨A, R⟩ \land Y Btwn ⟨A, R⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩))) \to Y Btwn ⟨A, R⟩$
27		simprrr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land ((X Btwn ⟨A, R⟩ \land Y Btwn ⟨A, R⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩))) \to ⟨A, X⟩ Cgr ⟨A, Y⟩$
28		midofsegid	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to ((X Btwn ⟨A, R⟩ \land Y Btwn ⟨A, R⟩ \land ⟨A, X⟩ Cgr ⟨A, Y⟩) \to X = Y)$
29	1 2 4 3 8 28	syl122anc	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to ((X Btwn ⟨A, R⟩ \land Y Btwn ⟨A, R⟩ \land ⟨A, X⟩ Cgr ⟨A, Y⟩) \to X = Y)$
30	29	adantr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land ((X Btwn ⟨A, R⟩ \land Y Btwn ⟨A, R⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩))) \to ((X Btwn ⟨A, R⟩ \land Y Btwn ⟨A, R⟩ \land ⟨A, X⟩ Cgr ⟨A, Y⟩) \to X = Y)$
31	25 26 27 30	mp3and	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land ((X Btwn ⟨A, R⟩ \land Y Btwn ⟨A, R⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩))) \to X = Y$
32	31	exp32	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to ((X Btwn ⟨A, R⟩ \land Y Btwn ⟨A, R⟩) \to ((R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩) \to X = Y))$
33		simprlr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land ((R Btwn ⟨A, X⟩ \land Y Btwn ⟨A, R⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩))) \to Y Btwn ⟨A, R⟩$
34		simprll	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land ((R Btwn ⟨A, X⟩ \land Y Btwn ⟨A, R⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩))) \to R Btwn ⟨A, X⟩$
35	1 2 8 4 3 33 34	btwnexchand	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land ((R Btwn ⟨A, X⟩ \land Y Btwn ⟨A, R⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩))) \to Y Btwn ⟨A, X⟩$
36		simprrr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land ((R Btwn ⟨A, X⟩ \land Y Btwn ⟨A, R⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩))) \to ⟨A, X⟩ Cgr ⟨A, Y⟩$
37	1 2 3 8 35 36	endofsegidand	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land ((R Btwn ⟨A, X⟩ \land Y Btwn ⟨A, R⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩))) \to X = Y$
38	37	exp32	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to ((R Btwn ⟨A, X⟩ \land Y Btwn ⟨A, R⟩) \to ((R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩) \to X = Y))$
39		simprll	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land ((X Btwn ⟨A, R⟩ \land R Btwn ⟨A, Y⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩))) \to X Btwn ⟨A, R⟩$
40		simprlr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land ((X Btwn ⟨A, R⟩ \land R Btwn ⟨A, Y⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩))) \to R Btwn ⟨A, Y⟩$
41	1 2 3 4 8 39 40	btwnexchand	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land ((X Btwn ⟨A, R⟩ \land R Btwn ⟨A, Y⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩))) \to X Btwn ⟨A, Y⟩$
42		simprrr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land ((X Btwn ⟨A, R⟩ \land R Btwn ⟨A, Y⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩))) \to ⟨A, X⟩ Cgr ⟨A, Y⟩$
43	1 2 3 2 8 42	cgrcomand	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land ((X Btwn ⟨A, R⟩ \land R Btwn ⟨A, Y⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩))) \to ⟨A, Y⟩ Cgr ⟨A, X⟩$
44	1 2 8 3 41 43	endofsegidand	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land ((X Btwn ⟨A, R⟩ \land R Btwn ⟨A, Y⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩))) \to Y = X$
45	44	eqcomd	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land ((X Btwn ⟨A, R⟩ \land R Btwn ⟨A, Y⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩))) \to X = Y$
46	45	exp32	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to ((X Btwn ⟨A, R⟩ \land R Btwn ⟨A, Y⟩) \to ((R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩) \to X = Y))$
47		simprr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (((R Btwn ⟨A, X⟩ \land R Btwn ⟨A, Y⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩)) \land X Btwn ⟨A, Y⟩)) \to X Btwn ⟨A, Y⟩$
48		simplrr	$⊢ (((R Btwn ⟨A, X⟩ \land R Btwn ⟨A, Y⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩)) \land X Btwn ⟨A, Y⟩) \to ⟨A, X⟩ Cgr ⟨A, Y⟩$
49	48	adantl	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (((R Btwn ⟨A, X⟩ \land R Btwn ⟨A, Y⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩)) \land X Btwn ⟨A, Y⟩)) \to ⟨A, X⟩ Cgr ⟨A, Y⟩$
50	1 2 3 2 8 49	cgrcomand	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (((R Btwn ⟨A, X⟩ \land R Btwn ⟨A, Y⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩)) \land X Btwn ⟨A, Y⟩)) \to ⟨A, Y⟩ Cgr ⟨A, X⟩$
51	1 2 8 3 47 50	endofsegidand	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (((R Btwn ⟨A, X⟩ \land R Btwn ⟨A, Y⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩)) \land X Btwn ⟨A, Y⟩)) \to Y = X$
52	51	eqcomd	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (((R Btwn ⟨A, X⟩ \land R Btwn ⟨A, Y⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩)) \land X Btwn ⟨A, Y⟩)) \to X = Y$
53	52	expr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land ((R Btwn ⟨A, X⟩ \land R Btwn ⟨A, Y⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩))) \to (X Btwn ⟨A, Y⟩ \to X = Y)$
54		simprr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (((R Btwn ⟨A, X⟩ \land R Btwn ⟨A, Y⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩)) \land Y Btwn ⟨A, X⟩)) \to Y Btwn ⟨A, X⟩$
55		simplrr	$⊢ (((R Btwn ⟨A, X⟩ \land R Btwn ⟨A, Y⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩)) \land Y Btwn ⟨A, X⟩) \to ⟨A, X⟩ Cgr ⟨A, Y⟩$
56	55	adantl	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (((R Btwn ⟨A, X⟩ \land R Btwn ⟨A, Y⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩)) \land Y Btwn ⟨A, X⟩)) \to ⟨A, X⟩ Cgr ⟨A, Y⟩$
57	1 2 3 8 54 56	endofsegidand	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (((R Btwn ⟨A, X⟩ \land R Btwn ⟨A, Y⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩)) \land Y Btwn ⟨A, X⟩)) \to X = Y$
58	57	expr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land ((R Btwn ⟨A, X⟩ \land R Btwn ⟨A, Y⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩))) \to (Y Btwn ⟨A, X⟩ \to X = Y)$
59		simprrl	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land ((R Btwn ⟨A, X⟩ \land R Btwn ⟨A, Y⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩))) \to R \neq A$
60	59	necomd	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land ((R Btwn ⟨A, X⟩ \land R Btwn ⟨A, Y⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩))) \to A \neq R$
61		simprll	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land ((R Btwn ⟨A, X⟩ \land R Btwn ⟨A, Y⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩))) \to R Btwn ⟨A, X⟩$
62		simprlr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land ((R Btwn ⟨A, X⟩ \land R Btwn ⟨A, Y⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩))) \to R Btwn ⟨A, Y⟩$
63		btwnconn1	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to ((A \neq R \land R Btwn ⟨A, X⟩ \land R Btwn ⟨A, Y⟩) \to (X Btwn ⟨A, Y⟩ \lor Y Btwn ⟨A, X⟩))$
64	1 2 4 3 8 63	syl122anc	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to ((A \neq R \land R Btwn ⟨A, X⟩ \land R Btwn ⟨A, Y⟩) \to (X Btwn ⟨A, Y⟩ \lor Y Btwn ⟨A, X⟩))$
65	64	adantr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land ((R Btwn ⟨A, X⟩ \land R Btwn ⟨A, Y⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩))) \to ((A \neq R \land R Btwn ⟨A, X⟩ \land R Btwn ⟨A, Y⟩) \to (X Btwn ⟨A, Y⟩ \lor Y Btwn ⟨A, X⟩))$
66	60 61 62 65	mp3and	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land ((R Btwn ⟨A, X⟩ \land R Btwn ⟨A, Y⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩))) \to (X Btwn ⟨A, Y⟩ \lor Y Btwn ⟨A, X⟩)$
67	53 58 66	mpjaod	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land ((R Btwn ⟨A, X⟩ \land R Btwn ⟨A, Y⟩) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩))) \to X = Y$
68	67	exp32	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to ((R Btwn ⟨A, X⟩ \land R Btwn ⟨A, Y⟩) \to ((R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩) \to X = Y))$
69	32 38 46 68	ccased	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to (((X Btwn ⟨A, R⟩ \lor R Btwn ⟨A, X⟩) \land (Y Btwn ⟨A, R⟩ \lor R Btwn ⟨A, Y⟩)) \to ((R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩) \to X = Y))$
70	69	imp32	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (((X Btwn ⟨A, R⟩ \lor R Btwn ⟨A, X⟩) \land (Y Btwn ⟨A, R⟩ \lor R Btwn ⟨A, Y⟩)) \land (R \neq A \land ⟨A, X⟩ Cgr ⟨A, Y⟩))) \to X = Y$
71	24 70	syldan	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (((X \neq A \land R \neq A \land (X Btwn ⟨A, R⟩ \lor R Btwn ⟨A, X⟩)) \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land ((Y \neq A \land R \neq A \land (Y Btwn ⟨A, R⟩ \lor R Btwn ⟨A, Y⟩)) \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to X = Y$
72	71	ex	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to ((((X \neq A \land R \neq A \land (X Btwn ⟨A, R⟩ \lor R Btwn ⟨A, X⟩)) \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land ((Y \neq A \land R \neq A \land (Y Btwn ⟨A, R⟩ \lor R Btwn ⟨A, Y⟩)) \land ⟨A, Y⟩ Cgr ⟨B, C⟩)) \to X = Y)$
73	12 72	sylbid	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to (((A OutsideOf ⟨X, R⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A OutsideOf ⟨Y, R⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩)) \to X = Y)$

Metamath Proof Explorer

Theorem outsideofeq

Proof