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

Definition df-transport 24653
Description: Define the segment transport function. See fvtransport 24655 for an explanation of the function. (Contributed by Scott Fenton, 18-Oct-2013.)
Assertion
Ref Expression
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 ) ) ) }
Distinct variable group:    n, p, q, r, x

Detailed syntax breakdown of Definition df-transport
StepHypRef Expression
1 ctransport 24652 . 2  class TransportTo
2 vp . . . . . . . 8  set  p
32cv 1622 . . . . . . 7  class  p
4 vn . . . . . . . . . 10  set  n
54cv 1622 . . . . . . . . 9  class  n
6 cee 24516 . . . . . . . . 9  class  EE
75, 6cfv 5255 . . . . . . . 8  class  ( EE
`  n )
87, 7cxp 4687 . . . . . . 7  class  ( ( EE `  n )  X.  ( EE `  n ) )
93, 8wcel 1684 . . . . . 6  wff  p  e.  ( ( EE `  n )  X.  ( EE `  n ) )
10 vq . . . . . . . 8  set  q
1110cv 1622 . . . . . . 7  class  q
1211, 8wcel 1684 . . . . . 6  wff  q  e.  ( ( EE `  n )  X.  ( EE `  n ) )
13 c1st 6120 . . . . . . . 8  class  1st
1411, 13cfv 5255 . . . . . . 7  class  ( 1st `  q )
15 c2nd 6121 . . . . . . . 8  class  2nd
1611, 15cfv 5255 . . . . . . 7  class  ( 2nd `  q )
1714, 16wne 2446 . . . . . 6  wff  ( 1st `  q )  =/=  ( 2nd `  q )
189, 12, 17w3a 934 . . . . 5  wff  ( p  e.  ( ( EE
`  n )  X.  ( EE `  n
) )  /\  q  e.  ( ( EE `  n )  X.  ( EE `  n ) )  /\  ( 1st `  q
)  =/=  ( 2nd `  q ) )
19 vx . . . . . . 7  set  x
2019cv 1622 . . . . . 6  class  x
21 vr . . . . . . . . . . 11  set  r
2221cv 1622 . . . . . . . . . 10  class  r
2314, 22cop 3643 . . . . . . . . 9  class  <. ( 1st `  q ) ,  r >.
24 cbtwn 24517 . . . . . . . . 9  class  Btwn
2516, 23, 24wbr 4023 . . . . . . . 8  wff  ( 2nd `  q )  Btwn  <. ( 1st `  q ) ,  r >.
2616, 22cop 3643 . . . . . . . . 9  class  <. ( 2nd `  q ) ,  r >.
27 ccgr 24518 . . . . . . . . 9  class Cgr
2826, 3, 27wbr 4023 . . . . . . . 8  wff  <. ( 2nd `  q ) ,  r >.Cgr p
2925, 28wa 358 . . . . . . 7  wff  ( ( 2nd `  q ) 
Btwn  <. ( 1st `  q
) ,  r >.  /\  <. ( 2nd `  q
) ,  r >.Cgr p )
3029, 21, 7crio 6297 . . . . . 6  class  ( iota_ r  e.  ( EE `  n ) ( ( 2nd `  q ) 
Btwn  <. ( 1st `  q
) ,  r >.  /\  <. ( 2nd `  q
) ,  r >.Cgr p ) )
3120, 30wceq 1623 . . . . 5  wff  x  =  ( iota_ r  e.  ( EE `  n ) ( ( 2nd `  q
)  Btwn  <. ( 1st `  q ) ,  r
>.  /\  <. ( 2nd `  q
) ,  r >.Cgr p ) )
3218, 31wa 358 . . . 4  wff  ( ( 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 cn 9746 . . . 4  class  NN
3432, 4, 33wrex 2544 . . 3  wff  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 ) ) )
3534, 2, 10, 19coprab 5859 . 2  class  { <. <.
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 ) ) ) }
361, 35wceq 1623 1  wff 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 ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  funtransport  24654  fvtransport  24655
  Copyright terms: Public domain W3C validator