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

Definition df-transport 24725
Description: Define the segment transport function. See fvtransport 24727 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 24724 . 2  class TransportTo
2 vp . . . . . . . 8  set  p
32cv 1631 . . . . . . 7  class  p
4 vn . . . . . . . . . 10  set  n
54cv 1631 . . . . . . . . 9  class  n
6 cee 24588 . . . . . . . . 9  class  EE
75, 6cfv 5271 . . . . . . . 8  class  ( EE
`  n )
87, 7cxp 4703 . . . . . . 7  class  ( ( EE `  n )  X.  ( EE `  n ) )
93, 8wcel 1696 . . . . . 6  wff  p  e.  ( ( EE `  n )  X.  ( EE `  n ) )
10 vq . . . . . . . 8  set  q
1110cv 1631 . . . . . . 7  class  q
1211, 8wcel 1696 . . . . . 6  wff  q  e.  ( ( EE `  n )  X.  ( EE `  n ) )
13 c1st 6136 . . . . . . . 8  class  1st
1411, 13cfv 5271 . . . . . . 7  class  ( 1st `  q )
15 c2nd 6137 . . . . . . . 8  class  2nd
1611, 15cfv 5271 . . . . . . 7  class  ( 2nd `  q )
1714, 16wne 2459 . . . . . 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 1631 . . . . . 6  class  x
21 vr . . . . . . . . . . 11  set  r
2221cv 1631 . . . . . . . . . 10  class  r
2314, 22cop 3656 . . . . . . . . 9  class  <. ( 1st `  q ) ,  r >.
24 cbtwn 24589 . . . . . . . . 9  class  Btwn
2516, 23, 24wbr 4039 . . . . . . . 8  wff  ( 2nd `  q )  Btwn  <. ( 1st `  q ) ,  r >.
2616, 22cop 3656 . . . . . . . . 9  class  <. ( 2nd `  q ) ,  r >.
27 ccgr 24590 . . . . . . . . 9  class Cgr
2826, 3, 27wbr 4039 . . . . . . . 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 6313 . . . . . 6  class  ( iota_ r  e.  ( EE `  n ) ( ( 2nd `  q ) 
Btwn  <. ( 1st `  q
) ,  r >.  /\  <. ( 2nd `  q
) ,  r >.Cgr p ) )
3120, 30wceq 1632 . . . . 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 9762 . . . 4  class  NN
3432, 4, 33wrex 2557 . . 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 5875 . 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 1632 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  24726  fvtransport  24727
  Copyright terms: Public domain W3C validator