segconeq

Description: Two points that satisfy the conclusion of axsegcon are identical. Uniqueness portion of Theorem 2.12 of Schwabhauser p. 29. (Contributed by Scott Fenton, 12-Jun-2013)

		Ref	Expression
	Assertion	segconeq	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to ((Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩)) \to X = Y)$

Proof

Step	Hyp	Ref	Expression
1		simpr2l	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to A Btwn ⟨Q, X⟩$
2	1 1	jca	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to (A Btwn ⟨Q, X⟩ \land A Btwn ⟨Q, X⟩)$
3		simpl1	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to N \in ℕ$
4		simpl31	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to Q \in 𝔼 (N)$
5		simpl21	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to A \in 𝔼 (N)$
6	3 4 5	cgrrflxd	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to ⟨Q, A⟩ Cgr ⟨Q, A⟩$
7		simpl32	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to X \in 𝔼 (N)$
8	3 5 7	cgrrflxd	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to ⟨A, X⟩ Cgr ⟨A, X⟩$
9	6 8	jca	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to (⟨Q, A⟩ Cgr ⟨Q, A⟩ \land ⟨A, X⟩ Cgr ⟨A, X⟩)$
10		simpl33	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to Y \in 𝔼 (N)$
11	4 5 10	3jca	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to (Q \in 𝔼 (N) \land A \in 𝔼 (N) \land Y \in 𝔼 (N))$
12	4 5 7	3jca	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to (Q \in 𝔼 (N) \land A \in 𝔼 (N) \land X \in 𝔼 (N))$
13	3 11 12	3jca	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to (N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N) \land Y \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land A \in 𝔼 (N) \land X \in 𝔼 (N)))$
14		simpr3l	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to A Btwn ⟨Q, Y⟩$
15	14 1	jca	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to (A Btwn ⟨Q, Y⟩ \land A Btwn ⟨Q, X⟩)$
16		simpl22	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to B \in 𝔼 (N)$
17		simpl23	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to C \in 𝔼 (N)$
18		simpr3r	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to ⟨A, Y⟩ Cgr ⟨B, C⟩$
19		cgrcom	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land Y \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \to (⟨A, Y⟩ Cgr ⟨B, C⟩ \leftrightarrow ⟨B, C⟩ Cgr ⟨A, Y⟩)$
20	3 5 10 16 17 19	syl122anc	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to (⟨A, Y⟩ Cgr ⟨B, C⟩ \leftrightarrow ⟨B, C⟩ Cgr ⟨A, Y⟩)$
21	18 20	mpbid	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to ⟨B, C⟩ Cgr ⟨A, Y⟩$
22		simpr2r	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to ⟨A, X⟩ Cgr ⟨B, C⟩$
23		cgrcom	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land X \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \to (⟨A, X⟩ Cgr ⟨B, C⟩ \leftrightarrow ⟨B, C⟩ Cgr ⟨A, X⟩)$
24	3 5 7 16 17 23	syl122anc	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to (⟨A, X⟩ Cgr ⟨B, C⟩ \leftrightarrow ⟨B, C⟩ Cgr ⟨A, X⟩)$
25	22 24	mpbid	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to ⟨B, C⟩ Cgr ⟨A, X⟩$
26	3 16 17 5 10 5 7 21 25	cgrtr4d	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to ⟨A, Y⟩ Cgr ⟨A, X⟩$
27	15 6 26	jca32	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to ((A Btwn ⟨Q, Y⟩ \land A Btwn ⟨Q, X⟩) \land (⟨Q, A⟩ Cgr ⟨Q, A⟩ \land ⟨A, Y⟩ Cgr ⟨A, X⟩))$
28		cgrextend	$⊢ (N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N) \land Y \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land A \in 𝔼 (N) \land X \in 𝔼 (N))) \to (((A Btwn ⟨Q, Y⟩ \land A Btwn ⟨Q, X⟩) \land (⟨Q, A⟩ Cgr ⟨Q, A⟩ \land ⟨A, Y⟩ Cgr ⟨A, X⟩)) \to ⟨Q, Y⟩ Cgr ⟨Q, X⟩)$
29	13 27 28	sylc	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to ⟨Q, Y⟩ Cgr ⟨Q, X⟩$
30	29 26	jca	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to (⟨Q, Y⟩ Cgr ⟨Q, X⟩ \land ⟨A, Y⟩ Cgr ⟨A, X⟩)$
31	2 9 30	3jca	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \land (Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩))) \to ((A Btwn ⟨Q, X⟩ \land A Btwn ⟨Q, X⟩) \land (⟨Q, A⟩ Cgr ⟨Q, A⟩ \land ⟨A, X⟩ Cgr ⟨A, X⟩) \land (⟨Q, Y⟩ Cgr ⟨Q, X⟩ \land ⟨A, Y⟩ Cgr ⟨A, X⟩))$
32	31	ex	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to ((Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩)) \to ((A Btwn ⟨Q, X⟩ \land A Btwn ⟨Q, X⟩) \land (⟨Q, A⟩ Cgr ⟨Q, A⟩ \land ⟨A, X⟩ Cgr ⟨A, X⟩) \land (⟨Q, Y⟩ Cgr ⟨Q, X⟩ \land ⟨A, Y⟩ Cgr ⟨A, X⟩)))$
33		simp1	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to N \in ℕ$
34		simp31	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to Q \in 𝔼 (N)$
35		simp21	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to A \in 𝔼 (N)$
36		simp32	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to X \in 𝔼 (N)$
37		simp33	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to Y \in 𝔼 (N)$
38		brofs	$⊢ ((N \in ℕ \land Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (X \in 𝔼 (N) \land Y \in 𝔼 (N) \land Q \in 𝔼 (N)) \land (A \in 𝔼 (N) \land X \in 𝔼 (N) \land X \in 𝔼 (N))) \to (⟨⟨Q, A⟩, ⟨X, Y⟩⟩ OuterFiveSeg ⟨⟨Q, A⟩, ⟨X, X⟩⟩ \leftrightarrow ((A Btwn ⟨Q, X⟩ \land A Btwn ⟨Q, X⟩) \land (⟨Q, A⟩ Cgr ⟨Q, A⟩ \land ⟨A, X⟩ Cgr ⟨A, X⟩) \land (⟨Q, Y⟩ Cgr ⟨Q, X⟩ \land ⟨A, Y⟩ Cgr ⟨A, X⟩)))$
39	33 34 35 36 37 34 35 36 36 38	syl333anc	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to (⟨⟨Q, A⟩, ⟨X, Y⟩⟩ OuterFiveSeg ⟨⟨Q, A⟩, ⟨X, X⟩⟩ \leftrightarrow ((A Btwn ⟨Q, X⟩ \land A Btwn ⟨Q, X⟩) \land (⟨Q, A⟩ Cgr ⟨Q, A⟩ \land ⟨A, X⟩ Cgr ⟨A, X⟩) \land (⟨Q, Y⟩ Cgr ⟨Q, X⟩ \land ⟨A, Y⟩ Cgr ⟨A, X⟩)))$
40	32 39	sylibrd	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to ((Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩)) \to ⟨⟨Q, A⟩, ⟨X, Y⟩⟩ OuterFiveSeg ⟨⟨Q, A⟩, ⟨X, X⟩⟩)$
41		simp1	$⊢ (Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩)) \to Q \neq A$
42	41	a1i	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to ((Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩)) \to Q \neq A)$
43	40 42	jcad	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to ((Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩)) \to (⟨⟨Q, A⟩, ⟨X, Y⟩⟩ OuterFiveSeg ⟨⟨Q, A⟩, ⟨X, X⟩⟩ \land Q \neq A))$
44		5segofs	$⊢ ((N \in ℕ \land Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (X \in 𝔼 (N) \land Y \in 𝔼 (N) \land Q \in 𝔼 (N)) \land (A \in 𝔼 (N) \land X \in 𝔼 (N) \land X \in 𝔼 (N))) \to ((⟨⟨Q, A⟩, ⟨X, Y⟩⟩ OuterFiveSeg ⟨⟨Q, A⟩, ⟨X, X⟩⟩ \land Q \neq A) \to ⟨X, Y⟩ Cgr ⟨X, X⟩)$
45	33 34 35 36 37 34 35 36 36 44	syl333anc	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to ((⟨⟨Q, A⟩, ⟨X, Y⟩⟩ OuterFiveSeg ⟨⟨Q, A⟩, ⟨X, X⟩⟩ \land Q \neq A) \to ⟨X, Y⟩ Cgr ⟨X, X⟩)$
46		axcgrid	$⊢ (N \in ℕ \land (X \in 𝔼 (N) \land Y \in 𝔼 (N) \land X \in 𝔼 (N))) \to (⟨X, Y⟩ Cgr ⟨X, X⟩ \to X = Y)$
47	33 36 37 36 46	syl13anc	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to (⟨X, Y⟩ Cgr ⟨X, X⟩ \to X = Y)$
48	43 45 47	3syld	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (Q \in 𝔼 (N) \land X \in 𝔼 (N) \land Y \in 𝔼 (N))) \to ((Q \neq A \land (A Btwn ⟨Q, X⟩ \land ⟨A, X⟩ Cgr ⟨B, C⟩) \land (A Btwn ⟨Q, Y⟩ \land ⟨A, Y⟩ Cgr ⟨B, C⟩)) \to X = Y)$

Metamath Proof Explorer

Theorem segconeq

Proof