Metamath Proof Explorer

Definition df-transport

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

Ref Expression
Assertion df-transport ⊢ TransportTo = p q x | ∃ n ∈ ℕ p ∈ 𝔼 ⁡ n × 𝔼 ⁡ n ∧ q ∈ 𝔼 ⁡ n × 𝔼 ⁡ n ∧ 1 st ⁡ q ≠ 2 nd ⁡ q ∧ x = ι r ∈ 𝔼 ⁡ n | 2 nd ⁡ q Btwn 1 st ⁡ q r ∧ 2 nd ⁡ q r Cgr p

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctransport class TransportTo
1 vp setvar p
2 vq setvar q
3 vx setvar x
4 vn setvar n
5 cn class ℕ
6 1 cv setvar p
7 cee class 𝔼
8 4 cv setvar n
9 8 7 cfv class 𝔼 ⁡ n
10 9 9 cxp class 𝔼 ⁡ n × 𝔼 ⁡ n
11 6 10 wcel wff p ∈ 𝔼 ⁡ n × 𝔼 ⁡ n
12 2 cv setvar q
13 12 10 wcel wff q ∈ 𝔼 ⁡ n × 𝔼 ⁡ n
14 c1st class 1 st
15 12 14 cfv class 1 st ⁡ q
16 c2nd class 2 nd
17 12 16 cfv class 2 nd ⁡ q
18 15 17 wne wff 1 st ⁡ q ≠ 2 nd ⁡ q
19 11 13 18 w3a wff p ∈ 𝔼 ⁡ n × 𝔼 ⁡ n ∧ q ∈ 𝔼 ⁡ n × 𝔼 ⁡ n ∧ 1 st ⁡ q ≠ 2 nd ⁡ q
20 3 cv setvar x
21 vr setvar r
22 cbtwn class Btwn
23 21 cv setvar r
24 15 23 cop class 1 st ⁡ q r
25 17 24 22 wbr wff 2 nd ⁡ q Btwn 1 st ⁡ q r
26 17 23 cop class 2 nd ⁡ q r
27 ccgr class Cgr
28 26 6 27 wbr wff 2 nd ⁡ q r Cgr p
29 25 28 wa wff 2 nd ⁡ q Btwn 1 st ⁡ q r ∧ 2 nd ⁡ q r Cgr p
30 29 21 9 crio class ι r ∈ 𝔼 ⁡ n | 2 nd ⁡ q Btwn 1 st ⁡ q r ∧ 2 nd ⁡ q r Cgr p
31 20 30 wceq wff x = ι r ∈ 𝔼 ⁡ n | 2 nd ⁡ q Btwn 1 st ⁡ q r ∧ 2 nd ⁡ q r Cgr p
32 19 31 wa wff p ∈ 𝔼 ⁡ n × 𝔼 ⁡ n ∧ q ∈ 𝔼 ⁡ n × 𝔼 ⁡ n ∧ 1 st ⁡ q ≠ 2 nd ⁡ q ∧ x = ι r ∈ 𝔼 ⁡ n | 2 nd ⁡ q Btwn 1 st ⁡ q r ∧ 2 nd ⁡ q r Cgr p
33 32 4 5 wrex wff ∃ n ∈ ℕ p ∈ 𝔼 ⁡ n × 𝔼 ⁡ n ∧ q ∈ 𝔼 ⁡ n × 𝔼 ⁡ n ∧ 1 st ⁡ q ≠ 2 nd ⁡ q ∧ x = ι r ∈ 𝔼 ⁡ n | 2 nd ⁡ q Btwn 1 st ⁡ q r ∧ 2 nd ⁡ q r Cgr p
34 33 1 2 3 coprab class p q x | ∃ n ∈ ℕ p ∈ 𝔼 ⁡ n × 𝔼 ⁡ n ∧ q ∈ 𝔼 ⁡ n × 𝔼 ⁡ n ∧ 1 st ⁡ q ≠ 2 nd ⁡ q ∧ x = ι r ∈ 𝔼 ⁡ n | 2 nd ⁡ q Btwn 1 st ⁡ q r ∧ 2 nd ⁡ q r Cgr p
35 0 34 wceq wff TransportTo = p q x | ∃ n ∈ ℕ p ∈ 𝔼 ⁡ n × 𝔼 ⁡ n ∧ q ∈ 𝔼 ⁡ n × 𝔼 ⁡ n ∧ 1 st ⁡ q ≠ 2 nd ⁡ q ∧ x = ι r ∈ 𝔼 ⁡ n | 2 nd ⁡ q Btwn 1 st ⁡ q r ∧ 2 nd ⁡ q r Cgr p