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 34997
Description: Define the segment transport function. See fvtransport 34999 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 34996 . 2 class TransportTo
2 vp . . . . . . . 8 setvar 𝑝
32cv 1540 . . . . . . 7 class 𝑝
4 vn . . . . . . . . . 10 setvar 𝑛
54cv 1540 . . . . . . . . 9 class 𝑛
6 cee 28143 . . . . . . . . 9 class 𝔼
75, 6cfv 6543 . . . . . . . 8 class (𝔼‘𝑛)
87, 7cxp 5674 . . . . . . 7 class ((𝔼‘𝑛) × (𝔼‘𝑛))
93, 8wcel 2106 . . . . . 6 wff 𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛))
10 vq . . . . . . . 8 setvar 𝑞
1110cv 1540 . . . . . . 7 class 𝑞
1211, 8wcel 2106 . . . . . 6 wff 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛))
13 c1st 7972 . . . . . . . 8 class 1st
1411, 13cfv 6543 . . . . . . 7 class (1st𝑞)
15 c2nd 7973 . . . . . . . 8 class 2nd
1611, 15cfv 6543 . . . . . . 7 class (2nd𝑞)
1714, 16wne 2940 . . . . . 6 wff (1st𝑞) ≠ (2nd𝑞)
189, 12, 17w3a 1087 . . . . 5 wff (𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ (1st𝑞) ≠ (2nd𝑞))
19 vx . . . . . . 7 setvar 𝑥
2019cv 1540 . . . . . 6 class 𝑥
21 vr . . . . . . . . . . 11 setvar 𝑟
2221cv 1540 . . . . . . . . . 10 class 𝑟
2314, 22cop 4634 . . . . . . . . 9 class ⟨(1st𝑞), 𝑟
24 cbtwn 28144 . . . . . . . . 9 class Btwn
2516, 23, 24wbr 5148 . . . . . . . 8 wff (2nd𝑞) Btwn ⟨(1st𝑞), 𝑟
2616, 22cop 4634 . . . . . . . . 9 class ⟨(2nd𝑞), 𝑟
27 ccgr 28145 . . . . . . . . 9 class Cgr
2826, 3, 27wbr 5148 . . . . . . . 8 wff ⟨(2nd𝑞), 𝑟⟩Cgr𝑝
2925, 28wa 396 . . . . . . 7 wff ((2nd𝑞) Btwn ⟨(1st𝑞), 𝑟⟩ ∧ ⟨(2nd𝑞), 𝑟⟩Cgr𝑝)
3029, 21, 7crio 7363 . . . . . 6 class (𝑟 ∈ (𝔼‘𝑛)((2nd𝑞) Btwn ⟨(1st𝑞), 𝑟⟩ ∧ ⟨(2nd𝑞), 𝑟⟩Cgr𝑝))
3120, 30wceq 1541 . . . . 5 wff 𝑥 = (𝑟 ∈ (𝔼‘𝑛)((2nd𝑞) Btwn ⟨(1st𝑞), 𝑟⟩ ∧ ⟨(2nd𝑞), 𝑟⟩Cgr𝑝))
3218, 31wa 396 . . . 4 wff ((𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ (1st𝑞) ≠ (2nd𝑞)) ∧ 𝑥 = (𝑟 ∈ (𝔼‘𝑛)((2nd𝑞) Btwn ⟨(1st𝑞), 𝑟⟩ ∧ ⟨(2nd𝑞), 𝑟⟩Cgr𝑝)))
33 cn 12211 . . . 4 class
3432, 4, 33wrex 3070 . . 3 wff 𝑛 ∈ ℕ ((𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ (1st𝑞) ≠ (2nd𝑞)) ∧ 𝑥 = (𝑟 ∈ (𝔼‘𝑛)((2nd𝑞) Btwn ⟨(1st𝑞), 𝑟⟩ ∧ ⟨(2nd𝑞), 𝑟⟩Cgr𝑝)))
3534, 2, 10, 19coprab 7409 . 2 class {⟨⟨𝑝, 𝑞⟩, 𝑥⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ (1st𝑞) ≠ (2nd𝑞)) ∧ 𝑥 = (𝑟 ∈ (𝔼‘𝑛)((2nd𝑞) Btwn ⟨(1st𝑞), 𝑟⟩ ∧ ⟨(2nd𝑞), 𝑟⟩Cgr𝑝)))}
361, 35wceq 1541 1 wff TransportTo = {⟨⟨𝑝, 𝑞⟩, 𝑥⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ (1st𝑞) ≠ (2nd𝑞)) ∧ 𝑥 = (𝑟 ∈ (𝔼‘𝑛)((2nd𝑞) Btwn ⟨(1st𝑞), 𝑟⟩ ∧ ⟨(2nd𝑞), 𝑟⟩Cgr𝑝)))}
Colors of variables: wff setvar class
This definition is referenced by:  funtransport  34998  fvtransport  34999
  Copyright terms: Public domain W3C validator