Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-transport Structured version   Visualization version   GIF version

Definition df-transport 32474
Description: Define the segment transport function. See fvtransport 32476 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
StepHypRef Expression
1 ctransport 32473 . 2 class TransportTo
2 vp . . . . . . . 8 setvar 𝑝
32cv 1630 . . . . . . 7 class 𝑝
4 vn . . . . . . . . . 10 setvar 𝑛
54cv 1630 . . . . . . . . 9 class 𝑛
6 cee 25989 . . . . . . . . 9 class 𝔼
75, 6cfv 6030 . . . . . . . 8 class (𝔼‘𝑛)
87, 7cxp 5248 . . . . . . 7 class ((𝔼‘𝑛) × (𝔼‘𝑛))
93, 8wcel 2145 . . . . . 6 wff 𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛))
10 vq . . . . . . . 8 setvar 𝑞
1110cv 1630 . . . . . . 7 class 𝑞
1211, 8wcel 2145 . . . . . 6 wff 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛))
13 c1st 7317 . . . . . . . 8 class 1st
1411, 13cfv 6030 . . . . . . 7 class (1st𝑞)
15 c2nd 7318 . . . . . . . 8 class 2nd
1611, 15cfv 6030 . . . . . . 7 class (2nd𝑞)
1714, 16wne 2943 . . . . . 6 wff (1st𝑞) ≠ (2nd𝑞)
189, 12, 17w3a 1071 . . . . 5 wff (𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ (1st𝑞) ≠ (2nd𝑞))
19 vx . . . . . . 7 setvar 𝑥
2019cv 1630 . . . . . 6 class 𝑥
21 vr . . . . . . . . . . 11 setvar 𝑟
2221cv 1630 . . . . . . . . . 10 class 𝑟
2314, 22cop 4323 . . . . . . . . 9 class ⟨(1st𝑞), 𝑟
24 cbtwn 25990 . . . . . . . . 9 class Btwn
2516, 23, 24wbr 4787 . . . . . . . 8 wff (2nd𝑞) Btwn ⟨(1st𝑞), 𝑟
2616, 22cop 4323 . . . . . . . . 9 class ⟨(2nd𝑞), 𝑟
27 ccgr 25991 . . . . . . . . 9 class Cgr
2826, 3, 27wbr 4787 . . . . . . . 8 wff ⟨(2nd𝑞), 𝑟⟩Cgr𝑝
2925, 28wa 382 . . . . . . 7 wff ((2nd𝑞) Btwn ⟨(1st𝑞), 𝑟⟩ ∧ ⟨(2nd𝑞), 𝑟⟩Cgr𝑝)
3029, 21, 7crio 6756 . . . . . 6 class (𝑟 ∈ (𝔼‘𝑛)((2nd𝑞) Btwn ⟨(1st𝑞), 𝑟⟩ ∧ ⟨(2nd𝑞), 𝑟⟩Cgr𝑝))
3120, 30wceq 1631 . . . . 5 wff 𝑥 = (𝑟 ∈ (𝔼‘𝑛)((2nd𝑞) Btwn ⟨(1st𝑞), 𝑟⟩ ∧ ⟨(2nd𝑞), 𝑟⟩Cgr𝑝))
3218, 31wa 382 . . . 4 wff ((𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ (1st𝑞) ≠ (2nd𝑞)) ∧ 𝑥 = (𝑟 ∈ (𝔼‘𝑛)((2nd𝑞) Btwn ⟨(1st𝑞), 𝑟⟩ ∧ ⟨(2nd𝑞), 𝑟⟩Cgr𝑝)))
33 cn 11226 . . . 4 class
3432, 4, 33wrex 3062 . . 3 wff 𝑛 ∈ ℕ ((𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ (1st𝑞) ≠ (2nd𝑞)) ∧ 𝑥 = (𝑟 ∈ (𝔼‘𝑛)((2nd𝑞) Btwn ⟨(1st𝑞), 𝑟⟩ ∧ ⟨(2nd𝑞), 𝑟⟩Cgr𝑝)))
3534, 2, 10, 19coprab 6797 . 2 class {⟨⟨𝑝, 𝑞⟩, 𝑥⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ (1st𝑞) ≠ (2nd𝑞)) ∧ 𝑥 = (𝑟 ∈ (𝔼‘𝑛)((2nd𝑞) Btwn ⟨(1st𝑞), 𝑟⟩ ∧ ⟨(2nd𝑞), 𝑟⟩Cgr𝑝)))}
361, 35wceq 1631 1 wff TransportTo = {⟨⟨𝑝, 𝑞⟩, 𝑥⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ (1st𝑞) ≠ (2nd𝑞)) ∧ 𝑥 = (𝑟 ∈ (𝔼‘𝑛)((2nd𝑞) Btwn ⟨(1st𝑞), 𝑟⟩ ∧ ⟨(2nd𝑞), 𝑟⟩Cgr𝑝)))}
Colors of variables: wff setvar class
This definition is referenced by:  funtransport  32475  fvtransport  32476
  Copyright terms: Public domain W3C validator