Definition df-btwn 27549

Description: Define the Euclidean betweenness predicate. For details, see brbtwn 27556. (Contributed by Scott Fenton, 3-Jun-2013.)

Assertion

Ref	Expression
df-btwn	⊢ Btwn = ◡{⟨⟨𝑥, 𝑧⟩, 𝑦⟩ ∣ ∃𝑛 ∈ ℕ ((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑧‘𝑖))))}

Distinct variable group:   𝑥,𝑛,𝑦,𝑧,𝑡,𝑖

Detailed syntax breakdown of Definition df-btwn

Step	Hyp	Ref	Expression
1		cbtwn 27546	. 2 class Btwn
2		vx	. . . . . . . . 9 setvar 𝑥
3	2	cv 1539	. . . . . . . 8 class 𝑥
4		vn	. . . . . . . . . 10 setvar 𝑛
5	4	cv 1539	. . . . . . . . 9 class 𝑛
6		cee 27545	. . . . . . . . 9 class 𝔼
7	5, 6	cfv 6479	. . . . . . . 8 class (𝔼‘𝑛)
8	3, 7	wcel 2105	. . . . . . 7 wff 𝑥 ∈ (𝔼‘𝑛)
9		vz	. . . . . . . . 9 setvar 𝑧
10	9	cv 1539	. . . . . . . 8 class 𝑧
11	10, 7	wcel 2105	. . . . . . 7 wff 𝑧 ∈ (𝔼‘𝑛)
12		vy	. . . . . . . . 9 setvar 𝑦
13	12	cv 1539	. . . . . . . 8 class 𝑦
14	13, 7	wcel 2105	. . . . . . 7 wff 𝑦 ∈ (𝔼‘𝑛)
15	8, 11, 14	w3a 1086	. . . . . 6 wff (𝑥 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛))
16		vi	. . . . . . . . . . 11 setvar 𝑖
17	16	cv 1539	. . . . . . . . . 10 class 𝑖
18	17, 13	cfv 6479	. . . . . . . . 9 class (𝑦‘𝑖)
19		c1 10973	. . . . . . . . . . . 12 class 1
20		vt	. . . . . . . . . . . . 13 setvar 𝑡
21	20	cv 1539	. . . . . . . . . . . 12 class 𝑡
22		cmin 11306	. . . . . . . . . . . 12 class −
23	19, 21, 22	co 7337	. . . . . . . . . . 11 class (1 − 𝑡)
24	17, 3	cfv 6479	. . . . . . . . . . 11 class (𝑥‘𝑖)
25		cmul 10977	. . . . . . . . . . 11 class ·
26	23, 24, 25	co 7337	. . . . . . . . . 10 class ((1 − 𝑡) · (𝑥‘𝑖))
27	17, 10	cfv 6479	. . . . . . . . . . 11 class (𝑧‘𝑖)
28	21, 27, 25	co 7337	. . . . . . . . . 10 class (𝑡 · (𝑧‘𝑖))
29		caddc 10975	. . . . . . . . . 10 class +
30	26, 28, 29	co 7337	. . . . . . . . 9 class (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑧‘𝑖)))
31	18, 30	wceq 1540	. . . . . . . 8 wff (𝑦‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑧‘𝑖)))
32		cfz 13340	. . . . . . . . 9 class ...
33	19, 5, 32	co 7337	. . . . . . . 8 class (1...𝑛)
34	31, 16, 33	wral 3061	. . . . . . 7 wff ∀𝑖 ∈ (1...𝑛)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑧‘𝑖)))
35		cc0 10972	. . . . . . . 8 class 0
36		cicc 13183	. . . . . . . 8 class [,]
37	35, 19, 36	co 7337	. . . . . . 7 class (0[,]1)
38	34, 20, 37	wrex 3070	. . . . . 6 wff ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑧‘𝑖)))
39	15, 38	wa 396	. . . . 5 wff ((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑧‘𝑖))))
40		cn 12074	. . . . 5 class ℕ
41	39, 4, 40	wrex 3070	. . . 4 wff ∃𝑛 ∈ ℕ ((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑧‘𝑖))))
42	41, 2, 9, 12	coprab 7338	. . 3 class {⟨⟨𝑥, 𝑧⟩, 𝑦⟩ ∣ ∃𝑛 ∈ ℕ ((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑧‘𝑖))))}
43	42	ccnv 5619	. 2 class ◡{⟨⟨𝑥, 𝑧⟩, 𝑦⟩ ∣ ∃𝑛 ∈ ℕ ((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑧‘𝑖))))}
44	1, 43	wceq 1540	1 wff Btwn = ◡{⟨⟨𝑥, 𝑧⟩, 𝑦⟩ ∣ ∃𝑛 ∈ ℕ ((𝑥 ∈ (𝔼‘𝑛) ∧ 𝑧 ∈ (𝔼‘𝑛) ∧ 𝑦 ∈ (𝔼‘𝑛)) ∧ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑛)(𝑦‘𝑖) = (((1 − 𝑡) · (𝑥‘𝑖)) + (𝑡 · (𝑧‘𝑖))))}

This definition is referenced by:  brbtwn  27556