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 >. | E. n e. NN ( ( p e. ( ( EE ` n ) X. ( EE ` n ) ) /\ q e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) /\ x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctransport 
 |-  TransportTo
1 vp 
 |-  p
2 vq 
 |-  q
3 vx 
 |-  x
4 vn 
 |-  n
5 cn 
 |-  NN
6 1 cv 
 |-  p
7 cee 
 |-  EE
8 4 cv 
 |-  n
9 8 7 cfv 
 |-  ( EE ` n )
10 9 9 cxp 
 |-  ( ( EE ` n ) X. ( EE ` n ) )
11 6 10 wcel 
 |-  p e. ( ( EE ` n ) X. ( EE ` n ) )
12 2 cv 
 |-  q
13 12 10 wcel 
 |-  q e. ( ( EE ` n ) X. ( EE ` n ) )
14 c1st 
 |-  1st
15 12 14 cfv 
 |-  ( 1st ` q )
16 c2nd 
 |-  2nd
17 12 16 cfv 
 |-  ( 2nd ` q )
18 15 17 wne 
 |-  ( 1st ` q ) =/= ( 2nd ` q )
19 11 13 18 w3a 
 |-  ( p e. ( ( EE ` n ) X. ( EE ` n ) ) /\ q e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) )
20 3 cv 
 |-  x
21 vr 
 |-  r
22 cbtwn 
 |-  Btwn
23 21 cv 
 |-  r
24 15 23 cop 
 |-  <. ( 1st ` q ) , r >.
25 17 24 22 wbr 
 |-  ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >.
26 17 23 cop 
 |-  <. ( 2nd ` q ) , r >.
27 ccgr 
 |-  Cgr
28 26 6 27 wbr 
 |-  <. ( 2nd ` q ) , r >. Cgr p
29 25 28 wa 
 |-  ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p )
30 29 21 9 crio 
 |-  ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) )
31 20 30 wceq 
 |-  x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) )
32 19 31 wa 
 |-  ( ( p e. ( ( EE ` n ) X. ( EE ` n ) ) /\ q e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) /\ x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) )
33 32 4 5 wrex 
 |-  E. n e. NN ( ( p e. ( ( EE ` n ) X. ( EE ` n ) ) /\ q e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) /\ x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) )
34 33 1 2 3 coprab 
 |-  { <. <. p , q >. , x >. | E. n e. NN ( ( p e. ( ( EE ` n ) X. ( EE ` n ) ) /\ q e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) /\ x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) }
35 0 34 wceq 
 |-  TransportTo = { <. <. p , q >. , x >. | E. n e. NN ( ( p e. ( ( EE ` n ) X. ( EE ` n ) ) /\ q e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) /\ x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) }