Definition df-transport 34259

Description: Define the segment transport function. See fvtransport 34261 for an explanation of the function. (Contributed by Scott Fenton, 18-Oct-2013.)

Assertion

Ref	Expression
df-transport	⊢ TransportTo = {⟨⟨𝑝, 𝑞⟩, 𝑥⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ (1st ‘𝑞) ≠ (2nd ‘𝑞)) ∧ 𝑥 = (℩𝑟 ∈ (𝔼‘𝑛)((2nd ‘𝑞) Btwn ⟨(1st ‘𝑞), 𝑟⟩ ∧ ⟨(2nd ‘𝑞), 𝑟⟩Cgr𝑝)))}

Distinct variable group:   𝑛,𝑝,𝑞,𝑟,𝑥

Detailed syntax breakdown of Definition df-transport

Step	Hyp	Ref	Expression
1		ctransport 34258	. 2 class TransportTo
2		vp	. . . . . . . 8 setvar 𝑝
3	2	cv 1538	. . . . . . 7 class 𝑝
4		vn	. . . . . . . . . 10 setvar 𝑛
5	4	cv 1538	. . . . . . . . 9 class 𝑛
6		cee 27159	. . . . . . . . 9 class 𝔼
7	5, 6	cfv 6418	. . . . . . . 8 class (𝔼‘𝑛)
8	7, 7	cxp 5578	. . . . . . 7 class ((𝔼‘𝑛) × (𝔼‘𝑛))
9	3, 8	wcel 2108	. . . . . 6 wff 𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛))
10		vq	. . . . . . . 8 setvar 𝑞
11	10	cv 1538	. . . . . . 7 class 𝑞
12	11, 8	wcel 2108	. . . . . 6 wff 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛))
13		c1st 7802	. . . . . . . 8 class 1st
14	11, 13	cfv 6418	. . . . . . 7 class (1st ‘𝑞)
15		c2nd 7803	. . . . . . . 8 class 2nd
16	11, 15	cfv 6418	. . . . . . 7 class (2nd ‘𝑞)
17	14, 16	wne 2942	. . . . . 6 wff (1st ‘𝑞) ≠ (2nd ‘𝑞)
18	9, 12, 17	w3a 1085	. . . . 5 wff (𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ (1st ‘𝑞) ≠ (2nd ‘𝑞))
19		vx	. . . . . . 7 setvar 𝑥
20	19	cv 1538	. . . . . 6 class 𝑥
21		vr	. . . . . . . . . . 11 setvar 𝑟
22	21	cv 1538	. . . . . . . . . 10 class 𝑟
23	14, 22	cop 4564	. . . . . . . . 9 class ⟨(1st ‘𝑞), 𝑟⟩
24		cbtwn 27160	. . . . . . . . 9 class Btwn
25	16, 23, 24	wbr 5070	. . . . . . . 8 wff (2nd ‘𝑞) Btwn ⟨(1st ‘𝑞), 𝑟⟩
26	16, 22	cop 4564	. . . . . . . . 9 class ⟨(2nd ‘𝑞), 𝑟⟩
27		ccgr 27161	. . . . . . . . 9 class Cgr
28	26, 3, 27	wbr 5070	. . . . . . . 8 wff ⟨(2nd ‘𝑞), 𝑟⟩Cgr𝑝
29	25, 28	wa 395	. . . . . . 7 wff ((2nd ‘𝑞) Btwn ⟨(1st ‘𝑞), 𝑟⟩ ∧ ⟨(2nd ‘𝑞), 𝑟⟩Cgr𝑝)
30	29, 21, 7	crio 7211	. . . . . 6 class (℩𝑟 ∈ (𝔼‘𝑛)((2nd ‘𝑞) Btwn ⟨(1st ‘𝑞), 𝑟⟩ ∧ ⟨(2nd ‘𝑞), 𝑟⟩Cgr𝑝))
31	20, 30	wceq 1539	. . . . 5 wff 𝑥 = (℩𝑟 ∈ (𝔼‘𝑛)((2nd ‘𝑞) Btwn ⟨(1st ‘𝑞), 𝑟⟩ ∧ ⟨(2nd ‘𝑞), 𝑟⟩Cgr𝑝))
32	18, 31	wa 395	. . . 4 wff ((𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ (1st ‘𝑞) ≠ (2nd ‘𝑞)) ∧ 𝑥 = (℩𝑟 ∈ (𝔼‘𝑛)((2nd ‘𝑞) Btwn ⟨(1st ‘𝑞), 𝑟⟩ ∧ ⟨(2nd ‘𝑞), 𝑟⟩Cgr𝑝)))
33		cn 11903	. . . 4 class ℕ
34	32, 4, 33	wrex 3064	. . 3 wff ∃𝑛 ∈ ℕ ((𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ (1st ‘𝑞) ≠ (2nd ‘𝑞)) ∧ 𝑥 = (℩𝑟 ∈ (𝔼‘𝑛)((2nd ‘𝑞) Btwn ⟨(1st ‘𝑞), 𝑟⟩ ∧ ⟨(2nd ‘𝑞), 𝑟⟩Cgr𝑝)))
35	34, 2, 10, 19	coprab 7256	. 2 class {⟨⟨𝑝, 𝑞⟩, 𝑥⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ (1st ‘𝑞) ≠ (2nd ‘𝑞)) ∧ 𝑥 = (℩𝑟 ∈ (𝔼‘𝑛)((2nd ‘𝑞) Btwn ⟨(1st ‘𝑞), 𝑟⟩ ∧ ⟨(2nd ‘𝑞), 𝑟⟩Cgr𝑝)))}
36	1, 35	wceq 1539	1 wff TransportTo = {⟨⟨𝑝, 𝑞⟩, 𝑥⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ (1st ‘𝑞) ≠ (2nd ‘𝑞)) ∧ 𝑥 = (℩𝑟 ∈ (𝔼‘𝑛)((2nd ‘𝑞) Btwn ⟨(1st ‘𝑞), 𝑟⟩ ∧ ⟨(2nd ‘𝑞), 𝑟⟩Cgr𝑝)))}

This definition is referenced by:  funtransport  34260  fvtransport  34261