brsegle

Description: Binary relation form of the segment comparison relationship. (Contributed by Scott Fenton, 11-Oct-2013)

		Ref	Expression
	Assertion	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⟩))$

Proof

Step	Hyp	Ref	Expression
1		opex	$⊢ ⟨A, B⟩ \in V$
2		opex	$⊢ ⟨C, D⟩ \in V$
3		eqeq1	$⊢ p = ⟨A, B⟩ \to (p = ⟨a, b⟩ \leftrightarrow ⟨A, B⟩ = ⟨a, b⟩)$
4		eqcom	$⊢ ⟨A, B⟩ = ⟨a, b⟩ \leftrightarrow ⟨a, b⟩ = ⟨A, B⟩$
5	3 4	bitrdi	$⊢ p = ⟨A, B⟩ \to (p = ⟨a, b⟩ \leftrightarrow ⟨a, b⟩ = ⟨A, B⟩)$
6	5	3anbi1d	$⊢ p = ⟨A, B⟩ \to ((p = ⟨a, b⟩ \land q = ⟨c, d⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)) \leftrightarrow (⟨a, b⟩ = ⟨A, B⟩ \land q = ⟨c, d⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)))$
7	6	rexbidv	$⊢ p = ⟨A, B⟩ \to (\exists d \in 𝔼 (n) (p = ⟨a, b⟩ \land q = ⟨c, d⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)) \leftrightarrow \exists d \in 𝔼 (n) (⟨a, b⟩ = ⟨A, B⟩ \land q = ⟨c, d⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)))$
8	7	2rexbidv	$⊢ p = ⟨A, B⟩ \to (\exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) (p = ⟨a, b⟩ \land q = ⟨c, d⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)) \leftrightarrow \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) (⟨a, b⟩ = ⟨A, B⟩ \land q = ⟨c, d⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)))$
9	8	2rexbidv	$⊢ p = ⟨A, B⟩ \to (\exists n \in ℕ \exists a \in 𝔼 (n) \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) (p = ⟨a, b⟩ \land q = ⟨c, d⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)) \leftrightarrow \exists n \in ℕ \exists a \in 𝔼 (n) \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) (⟨a, b⟩ = ⟨A, B⟩ \land q = ⟨c, d⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)))$
10		eqeq1	$⊢ q = ⟨C, D⟩ \to (q = ⟨c, d⟩ \leftrightarrow ⟨C, D⟩ = ⟨c, d⟩)$
11		eqcom	$⊢ ⟨C, D⟩ = ⟨c, d⟩ \leftrightarrow ⟨c, d⟩ = ⟨C, D⟩$
12	10 11	bitrdi	$⊢ q = ⟨C, D⟩ \to (q = ⟨c, d⟩ \leftrightarrow ⟨c, d⟩ = ⟨C, D⟩)$
13	12	3anbi2d	$⊢ q = ⟨C, D⟩ \to ((⟨a, b⟩ = ⟨A, B⟩ \land q = ⟨c, d⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)) \leftrightarrow (⟨a, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)))$
14	13	rexbidv	$⊢ q = ⟨C, D⟩ \to (\exists d \in 𝔼 (n) (⟨a, b⟩ = ⟨A, B⟩ \land q = ⟨c, d⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)) \leftrightarrow \exists d \in 𝔼 (n) (⟨a, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)))$
15	14	2rexbidv	$⊢ q = ⟨C, D⟩ \to (\exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) (⟨a, b⟩ = ⟨A, B⟩ \land q = ⟨c, d⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)) \leftrightarrow \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) (⟨a, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)))$
16	15	2rexbidv	$⊢ q = ⟨C, D⟩ \to (\exists n \in ℕ \exists a \in 𝔼 (n) \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) (⟨a, b⟩ = ⟨A, B⟩ \land q = ⟨c, d⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)) \leftrightarrow \exists n \in ℕ \exists a \in 𝔼 (n) \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) (⟨a, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)))$
17		df-segle	$⊢ {Seg}_{\leq} = \{⟨p, q⟩ \| \exists n \in ℕ \exists a \in 𝔼 (n) \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) (p = ⟨a, b⟩ \land q = ⟨c, d⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩))\}$
18	1 2 9 16 17	brab	$⊢ ⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩ \leftrightarrow \exists n \in ℕ \exists a \in 𝔼 (n) \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) (⟨a, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩))$
19		vex	$⊢ a \in V$
20		vex	$⊢ b \in V$
21	19 20	opth	$⊢ ⟨a, b⟩ = ⟨A, B⟩ \leftrightarrow (a = A \land b = B)$
22		vex	$⊢ c \in V$
23		vex	$⊢ d \in V$
24	22 23	opth	$⊢ ⟨c, d⟩ = ⟨C, D⟩ \leftrightarrow (c = C \land d = D)$
25		biid	$⊢ \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩) \leftrightarrow \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)$
26	21 24 25	3anbi123i	$⊢ (⟨a, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)) \leftrightarrow ((a = A \land b = B) \land (c = C \land d = D) \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩))$
27	26	2rexbii	$⊢ \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) (⟨a, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)) \leftrightarrow \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) ((a = A \land b = B) \land (c = C \land d = D) \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩))$
28	27	2rexbii	$⊢ \exists a \in 𝔼 (n) \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) (⟨a, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)) \leftrightarrow \exists a \in 𝔼 (n) \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) ((a = A \land b = B) \land (c = C \land d = D) \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩))$
29	28	rexbii	$⊢ \exists n \in ℕ \exists a \in 𝔼 (n) \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) (⟨a, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)) \leftrightarrow \exists n \in ℕ \exists a \in 𝔼 (n) \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) ((a = A \land b = B) \land (c = C \land d = D) \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩))$
30		simpl2l	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land n \in ℕ) \to A \in 𝔼 (N)$
31	30	ad2antrl	$⊢ ((a = A \land (b = B \land (c = C \land d = D))) \land (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land n \in ℕ) \land ((A \in 𝔼 (n) \land B \in 𝔼 (n)) \land (C \in 𝔼 (n) \land D \in 𝔼 (n))))) \to A \in 𝔼 (N)$
32		eleenn	$⊢ A \in 𝔼 (N) \to N \in ℕ$
33	31 32	syl	$⊢ ((a = A \land (b = B \land (c = C \land d = D))) \land (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land n \in ℕ) \land ((A \in 𝔼 (n) \land B \in 𝔼 (n)) \land (C \in 𝔼 (n) \land D \in 𝔼 (n))))) \to N \in ℕ$
34		simprlr	$⊢ ((a = A \land (b = B \land (c = C \land d = D))) \land (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land n \in ℕ) \land ((A \in 𝔼 (n) \land B \in 𝔼 (n)) \land (C \in 𝔼 (n) \land D \in 𝔼 (n))))) \to n \in ℕ$
35		simprll	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land n \in ℕ) \land ((A \in 𝔼 (n) \land B \in 𝔼 (n)) \land (C \in 𝔼 (n) \land D \in 𝔼 (n)))) \to A \in 𝔼 (n)$
36	35	adantl	$⊢ ((a = A \land (b = B \land (c = C \land d = D))) \land (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land n \in ℕ) \land ((A \in 𝔼 (n) \land B \in 𝔼 (n)) \land (C \in 𝔼 (n) \land D \in 𝔼 (n))))) \to A \in 𝔼 (n)$
37		axdimuniq	$⊢ ((N \in ℕ \land A \in 𝔼 (N)) \land (n \in ℕ \land A \in 𝔼 (n))) \to N = n$
38	33 31 34 36 37	syl22anc	$⊢ ((a = A \land (b = B \land (c = C \land d = D))) \land (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land n \in ℕ) \land ((A \in 𝔼 (n) \land B \in 𝔼 (n)) \land (C \in 𝔼 (n) \land D \in 𝔼 (n))))) \to N = n$
39	38	fveq2d	$⊢ ((a = A \land (b = B \land (c = C \land d = D))) \land (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land n \in ℕ) \land ((A \in 𝔼 (n) \land B \in 𝔼 (n)) \land (C \in 𝔼 (n) \land D \in 𝔼 (n))))) \to 𝔼 (N) = 𝔼 (n)$
40	39	rexeqdv	$⊢ ((a = A \land (b = B \land (c = C \land d = D))) \land (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land n \in ℕ) \land ((A \in 𝔼 (n) \land B \in 𝔼 (n)) \land (C \in 𝔼 (n) \land D \in 𝔼 (n))))) \to (\exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \leftrightarrow \exists y \in 𝔼 (n) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))$
41	40	exbiri	$⊢ (a = A \land (b = B \land (c = C \land d = D))) \to ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land n \in ℕ) \land ((A \in 𝔼 (n) \land B \in 𝔼 (n)) \land (C \in 𝔼 (n) \land D \in 𝔼 (n)))) \to (\exists y \in 𝔼 (n) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \to \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)))$
42	41	anassrs	$⊢ ((a = A \land b = B) \land (c = C \land d = D)) \to ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land n \in ℕ) \land ((A \in 𝔼 (n) \land B \in 𝔼 (n)) \land (C \in 𝔼 (n) \land D \in 𝔼 (n)))) \to (\exists y \in 𝔼 (n) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \to \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)))$
43		eleq1	$⊢ a = A \to (a \in 𝔼 (n) \leftrightarrow A \in 𝔼 (n))$
44		eleq1	$⊢ b = B \to (b \in 𝔼 (n) \leftrightarrow B \in 𝔼 (n))$
45	43 44	bi2anan9	$⊢ (a = A \land b = B) \to ((a \in 𝔼 (n) \land b \in 𝔼 (n)) \leftrightarrow (A \in 𝔼 (n) \land B \in 𝔼 (n)))$
46		eleq1	$⊢ c = C \to (c \in 𝔼 (n) \leftrightarrow C \in 𝔼 (n))$
47		eleq1	$⊢ d = D \to (d \in 𝔼 (n) \leftrightarrow D \in 𝔼 (n))$
48	46 47	bi2anan9	$⊢ (c = C \land d = D) \to ((c \in 𝔼 (n) \land d \in 𝔼 (n)) \leftrightarrow (C \in 𝔼 (n) \land D \in 𝔼 (n)))$
49	45 48	bi2anan9	$⊢ ((a = A \land b = B) \land (c = C \land d = D)) \to (((a \in 𝔼 (n) \land b \in 𝔼 (n)) \land (c \in 𝔼 (n) \land d \in 𝔼 (n))) \leftrightarrow ((A \in 𝔼 (n) \land B \in 𝔼 (n)) \land (C \in 𝔼 (n) \land D \in 𝔼 (n))))$
50	49	anbi2d	$⊢ ((a = A \land b = B) \land (c = C \land d = D)) \to ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land n \in ℕ) \land ((a \in 𝔼 (n) \land b \in 𝔼 (n)) \land (c \in 𝔼 (n) \land d \in 𝔼 (n)))) \leftrightarrow (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land n \in ℕ) \land ((A \in 𝔼 (n) \land B \in 𝔼 (n)) \land (C \in 𝔼 (n) \land D \in 𝔼 (n)))))$
51		opeq12	$⊢ (a = A \land b = B) \to ⟨a, b⟩ = ⟨A, B⟩$
52	51	breq1d	$⊢ (a = A \land b = B) \to (⟨a, b⟩ Cgr ⟨c, y⟩ \leftrightarrow ⟨A, B⟩ Cgr ⟨c, y⟩)$
53	52	anbi2d	$⊢ (a = A \land b = B) \to ((y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩) \leftrightarrow (y Btwn ⟨c, d⟩ \land ⟨A, B⟩ Cgr ⟨c, y⟩))$
54		opeq12	$⊢ (c = C \land d = D) \to ⟨c, d⟩ = ⟨C, D⟩$
55	54	breq2d	$⊢ (c = C \land d = D) \to (y Btwn ⟨c, d⟩ \leftrightarrow y Btwn ⟨C, D⟩)$
56		opeq1	$⊢ c = C \to ⟨c, y⟩ = ⟨C, y⟩$
57	56	breq2d	$⊢ c = C \to (⟨A, B⟩ Cgr ⟨c, y⟩ \leftrightarrow ⟨A, B⟩ Cgr ⟨C, y⟩)$
58	57	adantr	$⊢ (c = C \land d = D) \to (⟨A, B⟩ Cgr ⟨c, y⟩ \leftrightarrow ⟨A, B⟩ Cgr ⟨C, y⟩)$
59	55 58	anbi12d	$⊢ (c = C \land d = D) \to ((y Btwn ⟨c, d⟩ \land ⟨A, B⟩ Cgr ⟨c, y⟩) \leftrightarrow (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))$
60	53 59	sylan9bb	$⊢ ((a = A \land b = B) \land (c = C \land d = D)) \to ((y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩) \leftrightarrow (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))$
61	60	rexbidv	$⊢ ((a = A \land b = B) \land (c = C \land d = D)) \to (\exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩) \leftrightarrow \exists y \in 𝔼 (n) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))$
62	61	imbi1d	$⊢ ((a = A \land b = B) \land (c = C \land d = D)) \to ((\exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩) \to \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)) \leftrightarrow (\exists y \in 𝔼 (n) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \to \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)))$
63	42 50 62	3imtr4d	$⊢ ((a = A \land b = B) \land (c = C \land d = D)) \to ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land n \in ℕ) \land ((a \in 𝔼 (n) \land b \in 𝔼 (n)) \land (c \in 𝔼 (n) \land d \in 𝔼 (n)))) \to (\exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩) \to \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)))$
64	63	com12	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land n \in ℕ) \land ((a \in 𝔼 (n) \land b \in 𝔼 (n)) \land (c \in 𝔼 (n) \land d \in 𝔼 (n)))) \to (((a = A \land b = B) \land (c = C \land d = D)) \to (\exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩) \to \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)))$
65	64	expd	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land n \in ℕ) \land ((a \in 𝔼 (n) \land b \in 𝔼 (n)) \land (c \in 𝔼 (n) \land d \in 𝔼 (n)))) \to ((a = A \land b = B) \to ((c = C \land d = D) \to (\exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩) \to \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))))$
66	65	3impd	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land n \in ℕ) \land ((a \in 𝔼 (n) \land b \in 𝔼 (n)) \land (c \in 𝔼 (n) \land d \in 𝔼 (n)))) \to (((a = A \land b = B) \land (c = C \land d = D) \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)) \to \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))$
67	66	expr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land n \in ℕ) \land (a \in 𝔼 (n) \land b \in 𝔼 (n))) \to ((c \in 𝔼 (n) \land d \in 𝔼 (n)) \to (((a = A \land b = B) \land (c = C \land d = D) \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)) \to \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)))$
68	67	rexlimdvv	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land n \in ℕ) \land (a \in 𝔼 (n) \land b \in 𝔼 (n))) \to (\exists c \in 𝔼 (n) \exists d \in 𝔼 (n) ((a = A \land b = B) \land (c = C \land d = D) \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)) \to \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))$
69	68	rexlimdvva	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land n \in ℕ) \to (\exists a \in 𝔼 (n) \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) ((a = A \land b = B) \land (c = C \land d = D) \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)) \to \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))$
70	69	rexlimdva	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (\exists n \in ℕ \exists a \in 𝔼 (n) \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) ((a = A \land b = B) \land (c = C \land d = D) \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)) \to \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))$
71	29 70	syl5bi	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (\exists n \in ℕ \exists a \in 𝔼 (n) \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) (⟨a, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)) \to \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))$
72		simpl1	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)) \to N \in ℕ$
73		simpl2l	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)) \to A \in 𝔼 (N)$
74		simpl2r	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)) \to B \in 𝔼 (N)$
75		simpl3l	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)) \to C \in 𝔼 (N)$
76		simpl3r	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)) \to D \in 𝔼 (N)$
77		eqidd	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)) \to ⟨A, B⟩ = ⟨A, B⟩$
78		eqidd	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)) \to ⟨C, D⟩ = ⟨C, D⟩$
79		simpr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)) \to \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)$
80		opeq1	$⊢ c = C \to ⟨c, d⟩ = ⟨C, d⟩$
81	80	eqeq1d	$⊢ c = C \to (⟨c, d⟩ = ⟨C, D⟩ \leftrightarrow ⟨C, d⟩ = ⟨C, D⟩)$
82	80	breq2d	$⊢ c = C \to (y Btwn ⟨c, d⟩ \leftrightarrow y Btwn ⟨C, d⟩)$
83	82 57	anbi12d	$⊢ c = C \to ((y Btwn ⟨c, d⟩ \land ⟨A, B⟩ Cgr ⟨c, y⟩) \leftrightarrow (y Btwn ⟨C, d⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))$
84	83	rexbidv	$⊢ c = C \to (\exists y \in 𝔼 (N) (y Btwn ⟨c, d⟩ \land ⟨A, B⟩ Cgr ⟨c, y⟩) \leftrightarrow \exists y \in 𝔼 (N) (y Btwn ⟨C, d⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))$
85	81 84	3anbi23d	$⊢ c = C \to ((⟨A, B⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (N) (y Btwn ⟨c, d⟩ \land ⟨A, B⟩ Cgr ⟨c, y⟩)) \leftrightarrow (⟨A, B⟩ = ⟨A, B⟩ \land ⟨C, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (N) (y Btwn ⟨C, d⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)))$
86		opeq2	$⊢ d = D \to ⟨C, d⟩ = ⟨C, D⟩$
87	86	eqeq1d	$⊢ d = D \to (⟨C, d⟩ = ⟨C, D⟩ \leftrightarrow ⟨C, D⟩ = ⟨C, D⟩)$
88	86	breq2d	$⊢ d = D \to (y Btwn ⟨C, d⟩ \leftrightarrow y Btwn ⟨C, D⟩)$
89	88	anbi1d	$⊢ d = D \to ((y Btwn ⟨C, d⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \leftrightarrow (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))$
90	89	rexbidv	$⊢ d = D \to (\exists y \in 𝔼 (N) (y Btwn ⟨C, d⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \leftrightarrow \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))$
91	87 90	3anbi23d	$⊢ d = D \to ((⟨A, B⟩ = ⟨A, B⟩ \land ⟨C, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (N) (y Btwn ⟨C, d⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)) \leftrightarrow (⟨A, B⟩ = ⟨A, B⟩ \land ⟨C, D⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)))$
92	85 91	rspc2ev	$⊢ (C \in 𝔼 (N) \land D \in 𝔼 (N) \land (⟨A, B⟩ = ⟨A, B⟩ \land ⟨C, D⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))) \to \exists c \in 𝔼 (N) \exists d \in 𝔼 (N) (⟨A, B⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (N) (y Btwn ⟨c, d⟩ \land ⟨A, B⟩ Cgr ⟨c, y⟩))$
93	75 76 77 78 79 92	syl113anc	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)) \to \exists c \in 𝔼 (N) \exists d \in 𝔼 (N) (⟨A, B⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (N) (y Btwn ⟨c, d⟩ \land ⟨A, B⟩ Cgr ⟨c, y⟩))$
94		opeq1	$⊢ a = A \to ⟨a, b⟩ = ⟨A, b⟩$
95	94	eqeq1d	$⊢ a = A \to (⟨a, b⟩ = ⟨A, B⟩ \leftrightarrow ⟨A, b⟩ = ⟨A, B⟩)$
96	94	breq1d	$⊢ a = A \to (⟨a, b⟩ Cgr ⟨c, y⟩ \leftrightarrow ⟨A, b⟩ Cgr ⟨c, y⟩)$
97	96	anbi2d	$⊢ a = A \to ((y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩) \leftrightarrow (y Btwn ⟨c, d⟩ \land ⟨A, b⟩ Cgr ⟨c, y⟩))$
98	97	rexbidv	$⊢ a = A \to (\exists y \in 𝔼 (N) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩) \leftrightarrow \exists y \in 𝔼 (N) (y Btwn ⟨c, d⟩ \land ⟨A, b⟩ Cgr ⟨c, y⟩))$
99	95 98	3anbi13d	$⊢ a = A \to ((⟨a, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (N) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)) \leftrightarrow (⟨A, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (N) (y Btwn ⟨c, d⟩ \land ⟨A, b⟩ Cgr ⟨c, y⟩)))$
100	99	2rexbidv	$⊢ a = A \to (\exists c \in 𝔼 (N) \exists d \in 𝔼 (N) (⟨a, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (N) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)) \leftrightarrow \exists c \in 𝔼 (N) \exists d \in 𝔼 (N) (⟨A, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (N) (y Btwn ⟨c, d⟩ \land ⟨A, b⟩ Cgr ⟨c, y⟩)))$
101		opeq2	$⊢ b = B \to ⟨A, b⟩ = ⟨A, B⟩$
102	101	eqeq1d	$⊢ b = B \to (⟨A, b⟩ = ⟨A, B⟩ \leftrightarrow ⟨A, B⟩ = ⟨A, B⟩)$
103	101	breq1d	$⊢ b = B \to (⟨A, b⟩ Cgr ⟨c, y⟩ \leftrightarrow ⟨A, B⟩ Cgr ⟨c, y⟩)$
104	103	anbi2d	$⊢ b = B \to ((y Btwn ⟨c, d⟩ \land ⟨A, b⟩ Cgr ⟨c, y⟩) \leftrightarrow (y Btwn ⟨c, d⟩ \land ⟨A, B⟩ Cgr ⟨c, y⟩))$
105	104	rexbidv	$⊢ b = B \to (\exists y \in 𝔼 (N) (y Btwn ⟨c, d⟩ \land ⟨A, b⟩ Cgr ⟨c, y⟩) \leftrightarrow \exists y \in 𝔼 (N) (y Btwn ⟨c, d⟩ \land ⟨A, B⟩ Cgr ⟨c, y⟩))$
106	102 105	3anbi13d	$⊢ b = B \to ((⟨A, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (N) (y Btwn ⟨c, d⟩ \land ⟨A, b⟩ Cgr ⟨c, y⟩)) \leftrightarrow (⟨A, B⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (N) (y Btwn ⟨c, d⟩ \land ⟨A, B⟩ Cgr ⟨c, y⟩)))$
107	106	2rexbidv	$⊢ b = B \to (\exists c \in 𝔼 (N) \exists d \in 𝔼 (N) (⟨A, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (N) (y Btwn ⟨c, d⟩ \land ⟨A, b⟩ Cgr ⟨c, y⟩)) \leftrightarrow \exists c \in 𝔼 (N) \exists d \in 𝔼 (N) (⟨A, B⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (N) (y Btwn ⟨c, d⟩ \land ⟨A, B⟩ Cgr ⟨c, y⟩)))$
108	100 107	rspc2ev	$⊢ (A \in 𝔼 (N) \land B \in 𝔼 (N) \land \exists c \in 𝔼 (N) \exists d \in 𝔼 (N) (⟨A, B⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (N) (y Btwn ⟨c, d⟩ \land ⟨A, B⟩ Cgr ⟨c, y⟩))) \to \exists a \in 𝔼 (N) \exists b \in 𝔼 (N) \exists c \in 𝔼 (N) \exists d \in 𝔼 (N) (⟨a, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (N) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩))$
109	73 74 93 108	syl3anc	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)) \to \exists a \in 𝔼 (N) \exists b \in 𝔼 (N) \exists c \in 𝔼 (N) \exists d \in 𝔼 (N) (⟨a, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (N) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩))$
110		fveq2	$⊢ n = N \to 𝔼 (n) = 𝔼 (N)$
111	110	rexeqdv	$⊢ n = N \to (\exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩) \leftrightarrow \exists y \in 𝔼 (N) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩))$
112	111	3anbi3d	$⊢ n = N \to ((⟨a, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)) \leftrightarrow (⟨a, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (N) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)))$
113	110 112	rexeqbidv	$⊢ n = N \to (\exists d \in 𝔼 (n) (⟨a, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)) \leftrightarrow \exists d \in 𝔼 (N) (⟨a, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (N) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)))$
114	110 113	rexeqbidv	$⊢ n = N \to (\exists c \in 𝔼 (n) \exists d \in 𝔼 (n) (⟨a, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)) \leftrightarrow \exists c \in 𝔼 (N) \exists d \in 𝔼 (N) (⟨a, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (N) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)))$
115	110 114	rexeqbidv	$⊢ n = N \to (\exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) (⟨a, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)) \leftrightarrow \exists b \in 𝔼 (N) \exists c \in 𝔼 (N) \exists d \in 𝔼 (N) (⟨a, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (N) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)))$
116	110 115	rexeqbidv	$⊢ n = N \to (\exists a \in 𝔼 (n) \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) (⟨a, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)) \leftrightarrow \exists a \in 𝔼 (N) \exists b \in 𝔼 (N) \exists c \in 𝔼 (N) \exists d \in 𝔼 (N) (⟨a, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (N) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)))$
117	116	rspcev	$⊢ (N \in ℕ \land \exists a \in 𝔼 (N) \exists b \in 𝔼 (N) \exists c \in 𝔼 (N) \exists d \in 𝔼 (N) (⟨a, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (N) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩))) \to \exists n \in ℕ \exists a \in 𝔼 (n) \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) (⟨a, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩))$
118	72 109 117	syl2anc	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩)) \to \exists n \in ℕ \exists a \in 𝔼 (n) \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) (⟨a, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩))$
119	118	ex	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (\exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩) \to \exists n \in ℕ \exists a \in 𝔼 (n) \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) (⟨a, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)))$
120	71 119	impbid	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (\exists n \in ℕ \exists a \in 𝔼 (n) \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) (⟨a, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩ \land \exists y \in 𝔼 (n) (y Btwn ⟨c, d⟩ \land ⟨a, b⟩ Cgr ⟨c, y⟩)) \leftrightarrow \exists y \in 𝔼 (N) (y Btwn ⟨C, D⟩ \land ⟨A, B⟩ Cgr ⟨C, y⟩))$
121	18 120	syl5bb	$⊢ (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⟩))$

Metamath Proof Explorer

Theorem brsegle

Proof