Step | Hyp | Ref
| Expression |
1 | | ctransport 34996 |
. 2
class
TransportTo |
2 | | vp |
. . . . . . . 8
setvar 𝑝 |
3 | 2 | cv 1540 |
. . . . . . 7
class 𝑝 |
4 | | vn |
. . . . . . . . . 10
setvar 𝑛 |
5 | 4 | cv 1540 |
. . . . . . . . 9
class 𝑛 |
6 | | cee 28143 |
. . . . . . . . 9
class
𝔼 |
7 | 5, 6 | cfv 6543 |
. . . . . . . 8
class
(𝔼‘𝑛) |
8 | 7, 7 | cxp 5674 |
. . . . . . 7
class
((𝔼‘𝑛)
× (𝔼‘𝑛)) |
9 | 3, 8 | wcel 2106 |
. . . . . 6
wff 𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) |
10 | | vq |
. . . . . . . 8
setvar 𝑞 |
11 | 10 | cv 1540 |
. . . . . . 7
class 𝑞 |
12 | 11, 8 | wcel 2106 |
. . . . . 6
wff 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) |
13 | | c1st 7972 |
. . . . . . . 8
class
1st |
14 | 11, 13 | cfv 6543 |
. . . . . . 7
class
(1st ‘𝑞) |
15 | | c2nd 7973 |
. . . . . . . 8
class
2nd |
16 | 11, 15 | cfv 6543 |
. . . . . . 7
class
(2nd ‘𝑞) |
17 | 14, 16 | wne 2940 |
. . . . . 6
wff
(1st ‘𝑞) ≠ (2nd ‘𝑞) |
18 | 9, 12, 17 | w3a 1087 |
. . . . 5
wff (𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ (1st ‘𝑞) ≠ (2nd
‘𝑞)) |
19 | | vx |
. . . . . . 7
setvar 𝑥 |
20 | 19 | cv 1540 |
. . . . . 6
class 𝑥 |
21 | | vr |
. . . . . . . . . . 11
setvar 𝑟 |
22 | 21 | cv 1540 |
. . . . . . . . . 10
class 𝑟 |
23 | 14, 22 | cop 4634 |
. . . . . . . . 9
class
⟨(1st ‘𝑞), 𝑟⟩ |
24 | | cbtwn 28144 |
. . . . . . . . 9
class
Btwn |
25 | 16, 23, 24 | wbr 5148 |
. . . . . . . 8
wff
(2nd ‘𝑞) Btwn ⟨(1st ‘𝑞), 𝑟⟩ |
26 | 16, 22 | cop 4634 |
. . . . . . . . 9
class
⟨(2nd ‘𝑞), 𝑟⟩ |
27 | | ccgr 28145 |
. . . . . . . . 9
class
Cgr |
28 | 26, 3, 27 | wbr 5148 |
. . . . . . . 8
wff
⟨(2nd ‘𝑞), 𝑟⟩Cgr𝑝 |
29 | 25, 28 | wa 396 |
. . . . . . 7
wff
((2nd ‘𝑞) Btwn ⟨(1st ‘𝑞), 𝑟⟩ ∧ ⟨(2nd
‘𝑞), 𝑟⟩Cgr𝑝) |
30 | 29, 21, 7 | crio 7363 |
. . . . . 6
class
(℩𝑟
∈ (𝔼‘𝑛)((2nd ‘𝑞) Btwn ⟨(1st ‘𝑞), 𝑟⟩ ∧ ⟨(2nd
‘𝑞), 𝑟⟩Cgr𝑝)) |
31 | 20, 30 | wceq 1541 |
. . . . 5
wff 𝑥 = (℩𝑟 ∈ (𝔼‘𝑛)((2nd ‘𝑞) Btwn ⟨(1st
‘𝑞), 𝑟⟩ ∧
⟨(2nd ‘𝑞), 𝑟⟩Cgr𝑝)) |
32 | 18, 31 | wa 396 |
. . . 4
wff ((𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ (1st ‘𝑞) ≠ (2nd
‘𝑞)) ∧ 𝑥 = (℩𝑟 ∈ (𝔼‘𝑛)((2nd ‘𝑞) Btwn ⟨(1st
‘𝑞), 𝑟⟩ ∧
⟨(2nd ‘𝑞), 𝑟⟩Cgr𝑝))) |
33 | | cn 12211 |
. . . 4
class
ℕ |
34 | 32, 4, 33 | wrex 3070 |
. . 3
wff
∃𝑛 ∈
ℕ ((𝑝 ∈
((𝔼‘𝑛) ×
(𝔼‘𝑛)) ∧
𝑞 ∈
((𝔼‘𝑛) ×
(𝔼‘𝑛)) ∧
(1st ‘𝑞)
≠ (2nd ‘𝑞)) ∧ 𝑥 = (℩𝑟 ∈ (𝔼‘𝑛)((2nd ‘𝑞) Btwn ⟨(1st ‘𝑞), 𝑟⟩ ∧ ⟨(2nd
‘𝑞), 𝑟⟩Cgr𝑝))) |
35 | 34, 2, 10, 19 | coprab 7409 |
. 2
class
{⟨⟨𝑝,
𝑞⟩, 𝑥⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ (1st ‘𝑞) ≠ (2nd
‘𝑞)) ∧ 𝑥 = (℩𝑟 ∈ (𝔼‘𝑛)((2nd ‘𝑞) Btwn ⟨(1st
‘𝑞), 𝑟⟩ ∧
⟨(2nd ‘𝑞), 𝑟⟩Cgr𝑝)))} |
36 | 1, 35 | wceq 1541 |
1
wff TransportTo
= {⟨⟨𝑝, 𝑞⟩, 𝑥⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ 𝑞 ∈ ((𝔼‘𝑛) × (𝔼‘𝑛)) ∧ (1st ‘𝑞) ≠ (2nd
‘𝑞)) ∧ 𝑥 = (℩𝑟 ∈ (𝔼‘𝑛)((2nd ‘𝑞) Btwn ⟨(1st
‘𝑞), 𝑟⟩ ∧
⟨(2nd ‘𝑞), 𝑟⟩Cgr𝑝)))} |