Definition df-transport 32137

Description: Define the segment transport function. See fvtransport 32139 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

Step	Hyp	Ref	Expression
1		ctransport 32136	. 2 class TransportTo
2		vp	. . . . . . . 8 setvar p
3	2	cv 1482	. . . . . . 7 class p
4		vn	. . . . . . . . . 10 setvar n
5	4	cv 1482	. . . . . . . . 9 class n
6		cee 25768	. . . . . . . . 9 class EE
7	5, 6	cfv 5888	. . . . . . . 8 class ( EE ` n )
8	7, 7	cxp 5112	. . . . . . 7 class ( ( EE ` n ) X. ( EE ` n ) )
9	3, 8	wcel 1990	. . . . . 6 wff p e. ( ( EE ` n ) X. ( EE ` n ) )
10		vq	. . . . . . . 8 setvar q
11	10	cv 1482	. . . . . . 7 class q
12	11, 8	wcel 1990	. . . . . 6 wff q e. ( ( EE ` n ) X. ( EE ` n ) )
13		c1st 7166	. . . . . . . 8 class 1st
14	11, 13	cfv 5888	. . . . . . 7 class ( 1st ` q )
15		c2nd 7167	. . . . . . . 8 class 2nd
16	11, 15	cfv 5888	. . . . . . 7 class ( 2nd ` q )
17	14, 16	wne 2794	. . . . . 6 wff ( 1st ` q ) =/= ( 2nd ` q )
18	9, 12, 17	w3a 1037	. . . . 5 wff ( p e. ( ( EE ` n ) X. ( EE ` n ) ) /\ q e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) )
19		vx	. . . . . . 7 setvar x
20	19	cv 1482	. . . . . 6 class x
21		vr	. . . . . . . . . . 11 setvar r
22	21	cv 1482	. . . . . . . . . 10 class r
23	14, 22	cop 4183	. . . . . . . . 9 class <. ( 1st ` q ) , r >.
24		cbtwn 25769	. . . . . . . . 9 class Btwn
25	16, 23, 24	wbr 4653	. . . . . . . 8 wff ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >.
26	16, 22	cop 4183	. . . . . . . . 9 class <. ( 2nd ` q ) , r >.
27		ccgr 25770	. . . . . . . . 9 class Cgr
28	26, 3, 27	wbr 4653	. . . . . . . 8 wff <. ( 2nd ` q ) , r >.Cgr p
29	25, 28	wa 384	. . . . . . 7 wff ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >.Cgr p )
30	29, 21, 7	crio 6610	. . . . . 6 class ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >.Cgr p ) )
31	20, 30	wceq 1483	. . . . 5 wff x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >.Cgr p ) )
32	18, 31	wa 384	. . . 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 11020	. . . 4 class NN
34	32, 4, 33	wrex 2913	. . 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 ) ) )
35	34, 2, 10, 19	coprab 6651	. 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 ) ) ) }
36	1, 35	wceq 1483	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 ) ) ) }

This definition is referenced by:  funtransport  32138  fvtransport  32139