Definition df-transport 31307

Description: Define the segment transport function. See fvtransport 31309 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 31306	. 2 class TransportTo
2		vp	. . . . . . . 8 setvar 𝑝
3	2	cv 1474	. . . . . . 7 class 𝑝
4		vn	. . . . . . . . . 10 setvar 𝑛
5	4	cv 1474	. . . . . . . . 9 class 𝑛
6		cee 25568	. . . . . . . . 9 class 𝔼
7	5, 6	cfv 5804	. . . . . . . 8 class (𝔼‘𝑛)
8	7, 7	cxp 5036	. . . . . . 7 class ((𝔼‘𝑛) × (𝔼‘𝑛))
9	3, 8	wcel 1977	. . . . . 6 wff 𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛))
10		vq	. . . . . . . 8 setvar 𝑞
11	10	cv 1474	. . . . . . 7 class 𝑞
12	11, 8	wcel 1977	. . . . . 6 wff 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛))
13		c1st 7057	. . . . . . . 8 class 1st
14	11, 13	cfv 5804	. . . . . . 7 class (1st ‘𝑞)
15		c2nd 7058	. . . . . . . 8 class 2nd
16	11, 15	cfv 5804	. . . . . . 7 class (2nd ‘𝑞)
17	14, 16	wne 2780	. . . . . 6 wff (1st ‘𝑞) ≠ (2nd ‘𝑞)
18	9, 12, 17	w3a 1031	. . . . 5 wff (𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ (1st ‘𝑞) ≠ (2nd ‘𝑞))
19		vx	. . . . . . 7 setvar 𝑥
20	19	cv 1474	. . . . . 6 class 𝑥
21		vr	. . . . . . . . . . 11 setvar 𝑟
22	21	cv 1474	. . . . . . . . . 10 class 𝑟
23	14, 22	cop 4131	. . . . . . . . 9 class ⟨(1st ‘𝑞), 𝑟⟩
24		cbtwn 25569	. . . . . . . . 9 class Btwn
25	16, 23, 24	wbr 4583	. . . . . . . 8 wff (2nd ‘𝑞) Btwn ⟨(1st ‘𝑞), 𝑟⟩
26	16, 22	cop 4131	. . . . . . . . 9 class ⟨(2nd ‘𝑞), 𝑟⟩
27		ccgr 25570	. . . . . . . . 9 class Cgr
28	26, 3, 27	wbr 4583	. . . . . . . 8 wff ⟨(2nd ‘𝑞), 𝑟⟩Cgr𝑝
29	25, 28	wa 383	. . . . . . 7 wff ((2nd ‘𝑞) Btwn ⟨(1st ‘𝑞), 𝑟⟩ ∧ ⟨(2nd ‘𝑞), 𝑟⟩Cgr𝑝)
30	29, 21, 7	crio 6510	. . . . . 6 class (℩𝑟 ∈ (𝔼‘𝑛)((2nd ‘𝑞) Btwn ⟨(1st ‘𝑞), 𝑟⟩ ∧ ⟨(2nd ‘𝑞), 𝑟⟩Cgr𝑝))
31	20, 30	wceq 1475	. . . . 5 wff 𝑥 = (℩𝑟 ∈ (𝔼‘𝑛)((2nd ‘𝑞) Btwn ⟨(1st ‘𝑞), 𝑟⟩ ∧ ⟨(2nd ‘𝑞), 𝑟⟩Cgr𝑝))
32	18, 31	wa 383	. . . 4 wff ((𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ (1st ‘𝑞) ≠ (2nd ‘𝑞)) ∧ 𝑥 = (℩𝑟 ∈ (𝔼‘𝑛)((2nd ‘𝑞) Btwn ⟨(1st ‘𝑞), 𝑟⟩ ∧ ⟨(2nd ‘𝑞), 𝑟⟩Cgr𝑝)))
33		cn 10897	. . . 4 class ℕ
34	32, 4, 33	wrex 2897	. . 3 wff ∃𝑛 ∈ ℕ ((𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ (1st ‘𝑞) ≠ (2nd ‘𝑞)) ∧ 𝑥 = (℩𝑟 ∈ (𝔼‘𝑛)((2nd ‘𝑞) Btwn ⟨(1st ‘𝑞), 𝑟⟩ ∧ ⟨(2nd ‘𝑞), 𝑟⟩Cgr𝑝)))
35	34, 2, 10, 19	coprab 6550	. 2 class {⟨⟨𝑝, 𝑞⟩, 𝑥⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ (1st ‘𝑞) ≠ (2nd ‘𝑞)) ∧ 𝑥 = (℩𝑟 ∈ (𝔼‘𝑛)((2nd ‘𝑞) Btwn ⟨(1st ‘𝑞), 𝑟⟩ ∧ ⟨(2nd ‘𝑞), 𝑟⟩Cgr𝑝)))}
36	1, 35	wceq 1475	1 wff TransportTo = {⟨⟨𝑝, 𝑞⟩, 𝑥⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ (1st ‘𝑞) ≠ (2nd ‘𝑞)) ∧ 𝑥 = (℩𝑟 ∈ (𝔼‘𝑛)((2nd ‘𝑞) Btwn ⟨(1st ‘𝑞), 𝑟⟩ ∧ ⟨(2nd ‘𝑞), 𝑟⟩Cgr𝑝)))}

This definition is referenced by:  funtransport  31308  fvtransport  31309