segconeu

Description: Existential uniqueness version of segconeq . (Contributed by Scott Fenton, 19-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	segconeu	$⊢ (N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D)) \to \exists! r \in 𝔼 (N) (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D)) \to N \in ℕ$
2		simpr2	$⊢ (N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D)) \to (C \in 𝔼 (N) \land D \in 𝔼 (N))$
3		simpr1	$⊢ (N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D)) \to (A \in 𝔼 (N) \land B \in 𝔼 (N))$
4		axsegcon	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land (A \in 𝔼 (N) \land B \in 𝔼 (N))) \to \exists r \in 𝔼 (N) (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)$
5	1 2 3 4	syl3anc	$⊢ (N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D)) \to \exists r \in 𝔼 (N) (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)$
6		simpl23	$⊢ ((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D) \land (r \in 𝔼 (N) \land s \in 𝔼 (N))) \land ((D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩) \land (D Btwn ⟨C, s⟩ \land ⟨D, s⟩ Cgr ⟨A, B⟩))) \to C \neq D$
7		simprl	$⊢ ((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D) \land (r \in 𝔼 (N) \land s \in 𝔼 (N))) \land ((D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩) \land (D Btwn ⟨C, s⟩ \land ⟨D, s⟩ Cgr ⟨A, B⟩))) \to (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)$
8		simprr	$⊢ ((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D) \land (r \in 𝔼 (N) \land s \in 𝔼 (N))) \land ((D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩) \land (D Btwn ⟨C, s⟩ \land ⟨D, s⟩ Cgr ⟨A, B⟩))) \to (D Btwn ⟨C, s⟩ \land ⟨D, s⟩ Cgr ⟨A, B⟩)$
9	6 7 8	3jca	$⊢ ((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D) \land (r \in 𝔼 (N) \land s \in 𝔼 (N))) \land ((D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩) \land (D Btwn ⟨C, s⟩ \land ⟨D, s⟩ Cgr ⟨A, B⟩))) \to (C \neq D \land (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩) \land (D Btwn ⟨C, s⟩ \land ⟨D, s⟩ Cgr ⟨A, B⟩))$
10	9	ex	$⊢ (N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D) \land (r \in 𝔼 (N) \land s \in 𝔼 (N))) \to (((D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩) \land (D Btwn ⟨C, s⟩ \land ⟨D, s⟩ Cgr ⟨A, B⟩)) \to (C \neq D \land (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩) \land (D Btwn ⟨C, s⟩ \land ⟨D, s⟩ Cgr ⟨A, B⟩)))$
11		simp1	$⊢ (N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D) \land (r \in 𝔼 (N) \land s \in 𝔼 (N))) \to N \in ℕ$
12		simp22r	$⊢ (N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D) \land (r \in 𝔼 (N) \land s \in 𝔼 (N))) \to D \in 𝔼 (N)$
13		simp21l	$⊢ (N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D) \land (r \in 𝔼 (N) \land s \in 𝔼 (N))) \to A \in 𝔼 (N)$
14		simp21r	$⊢ (N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D) \land (r \in 𝔼 (N) \land s \in 𝔼 (N))) \to B \in 𝔼 (N)$
15		simp22l	$⊢ (N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D) \land (r \in 𝔼 (N) \land s \in 𝔼 (N))) \to C \in 𝔼 (N)$
16		simp3l	$⊢ (N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D) \land (r \in 𝔼 (N) \land s \in 𝔼 (N))) \to r \in 𝔼 (N)$
17		simp3r	$⊢ (N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D) \land (r \in 𝔼 (N) \land s \in 𝔼 (N))) \to s \in 𝔼 (N)$
18		segconeq	$⊢ (N \in ℕ \land (D \in 𝔼 (N) \land A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land r \in 𝔼 (N) \land s \in 𝔼 (N))) \to ((C \neq D \land (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩) \land (D Btwn ⟨C, s⟩ \land ⟨D, s⟩ Cgr ⟨A, B⟩)) \to r = s)$
19	11 12 13 14 15 16 17 18	syl133anc	$⊢ (N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D) \land (r \in 𝔼 (N) \land s \in 𝔼 (N))) \to ((C \neq D \land (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩) \land (D Btwn ⟨C, s⟩ \land ⟨D, s⟩ Cgr ⟨A, B⟩)) \to r = s)$
20	10 19	syld	$⊢ (N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D) \land (r \in 𝔼 (N) \land s \in 𝔼 (N))) \to (((D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩) \land (D Btwn ⟨C, s⟩ \land ⟨D, s⟩ Cgr ⟨A, B⟩)) \to r = s)$
21	20	3expa	$⊢ ((N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D)) \land (r \in 𝔼 (N) \land s \in 𝔼 (N))) \to (((D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩) \land (D Btwn ⟨C, s⟩ \land ⟨D, s⟩ Cgr ⟨A, B⟩)) \to r = s)$
22	21	ralrimivva	$⊢ (N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D)) \to \forall r \in 𝔼 (N) \forall s \in 𝔼 (N) (((D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩) \land (D Btwn ⟨C, s⟩ \land ⟨D, s⟩ Cgr ⟨A, B⟩)) \to r = s)$
23		opeq2	$⊢ r = s \to ⟨C, r⟩ = ⟨C, s⟩$
24	23	breq2d	$⊢ r = s \to (D Btwn ⟨C, r⟩ \leftrightarrow D Btwn ⟨C, s⟩)$
25		opeq2	$⊢ r = s \to ⟨D, r⟩ = ⟨D, s⟩$
26	25	breq1d	$⊢ r = s \to (⟨D, r⟩ Cgr ⟨A, B⟩ \leftrightarrow ⟨D, s⟩ Cgr ⟨A, B⟩)$
27	24 26	anbi12d	$⊢ r = s \to ((D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩) \leftrightarrow (D Btwn ⟨C, s⟩ \land ⟨D, s⟩ Cgr ⟨A, B⟩))$
28	27	reu4	$⊢ \exists! r \in 𝔼 (N) (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩) \leftrightarrow (\exists r \in 𝔼 (N) (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩) \land \forall r \in 𝔼 (N) \forall s \in 𝔼 (N) (((D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩) \land (D Btwn ⟨C, s⟩ \land ⟨D, s⟩ Cgr ⟨A, B⟩)) \to r = s))$
29	5 22 28	sylanbrc	$⊢ (N \in ℕ \land ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land C \neq D)) \to \exists! r \in 𝔼 (N) (D Btwn ⟨C, r⟩ \land ⟨D, r⟩ Cgr ⟨A, B⟩)$

Metamath Proof Explorer

Theorem segconeu

Proof