Metamath Proof Explorer

Theorem funtransport

Description: The TransportTo relationship is a function. (Contributed by Scott Fenton, 18-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion funtransport 
|- Fun TransportTo

Proof

Step Hyp Ref Expression
1 reeanv 
 |-  ( E. n e. NN E. m 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 ) ) ) /\ ( ( p e. ( ( EE ` m ) X. ( EE ` m ) ) /\ q e. ( ( EE ` m ) X. ( EE ` m ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) /\ y = ( iota_ r e. ( EE ` m ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) ) <-> ( 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 ) ) ) /\ E. m e. NN ( ( p e. ( ( EE ` m ) X. ( EE ` m ) ) /\ q e. ( ( EE ` m ) X. ( EE ` m ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) /\ y = ( iota_ r e. ( EE ` m ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) ) )
2 simp1 
 |-  ( ( p e. ( ( EE ` n ) X. ( EE ` n ) ) /\ q e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) -> p e. ( ( EE ` n ) X. ( EE ` n ) ) )
3 simp1 
 |-  ( ( p e. ( ( EE ` m ) X. ( EE ` m ) ) /\ q e. ( ( EE ` m ) X. ( EE ` m ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) -> p e. ( ( EE ` m ) X. ( EE ` m ) ) )
4 2 3 anim12i 
 |-  ( ( ( p e. ( ( EE ` n ) X. ( EE ` n ) ) /\ q e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) /\ ( p e. ( ( EE ` m ) X. ( EE ` m ) ) /\ q e. ( ( EE ` m ) X. ( EE ` m ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) ) -> ( p e. ( ( EE ` n ) X. ( EE ` n ) ) /\ p e. ( ( EE ` m ) X. ( EE ` m ) ) ) )
5 4 anim1i 
 |-  ( ( ( ( p e. ( ( EE ` n ) X. ( EE ` n ) ) /\ q e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) /\ ( p e. ( ( EE ` m ) X. ( EE ` m ) ) /\ q e. ( ( EE ` m ) X. ( EE ` m ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) ) /\ ( x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) /\ y = ( iota_ r e. ( EE ` m ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) ) -> ( ( p e. ( ( EE ` n ) X. ( EE ` n ) ) /\ p e. ( ( EE ` m ) X. ( EE ` m ) ) ) /\ ( x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) /\ y = ( iota_ r e. ( EE ` m ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) ) )
6 5 an4s 
 |-  ( ( ( ( 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 ) ) ) /\ ( ( p e. ( ( EE ` m ) X. ( EE ` m ) ) /\ q e. ( ( EE ` m ) X. ( EE ` m ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) /\ y = ( iota_ r e. ( EE ` m ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) ) -> ( ( p e. ( ( EE ` n ) X. ( EE ` n ) ) /\ p e. ( ( EE ` m ) X. ( EE ` m ) ) ) /\ ( x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) /\ y = ( iota_ r e. ( EE ` m ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) ) )
7 xp1st 
 |-  ( p e. ( ( EE ` n ) X. ( EE ` n ) ) -> ( 1st ` p ) e. ( EE ` n ) )
8 xp1st 
 |-  ( p e. ( ( EE ` m ) X. ( EE ` m ) ) -> ( 1st ` p ) e. ( EE ` m ) )
9 axdimuniq 
 |-  ( ( ( n e. NN /\ ( 1st ` p ) e. ( EE ` n ) ) /\ ( m e. NN /\ ( 1st ` p ) e. ( EE ` m ) ) ) -> n = m )
10 fveq2 
 |-  ( n = m -> ( EE ` n ) = ( EE ` m ) )
11 10 riotaeqdv 
 |-  ( n = m -> ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) = ( iota_ r e. ( EE ` m ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) )
12 11 eqeq2d 
 |-  ( n = m -> ( y = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) <-> y = ( iota_ r e. ( EE ` m ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) )
13 12 anbi2d 
 |-  ( n = m -> ( ( x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) /\ y = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) <-> ( x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) /\ y = ( iota_ r e. ( EE ` m ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) ) )
14 eqtr3 
 |-  ( ( x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) /\ y = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) -> x = y )
15 13 14 syl6bir 
 |-  ( n = m -> ( ( x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) /\ y = ( iota_ r e. ( EE ` m ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) -> x = y ) )
16 9 15 syl 
 |-  ( ( ( n e. NN /\ ( 1st ` p ) e. ( EE ` n ) ) /\ ( m e. NN /\ ( 1st ` p ) e. ( EE ` m ) ) ) -> ( ( x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) /\ y = ( iota_ r e. ( EE ` m ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) -> x = y ) )
17 16 an4s 
 |-  ( ( ( n e. NN /\ m e. NN ) /\ ( ( 1st ` p ) e. ( EE ` n ) /\ ( 1st ` p ) e. ( EE ` m ) ) ) -> ( ( x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) /\ y = ( iota_ r e. ( EE ` m ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) -> x = y ) )
18 17 ex 
 |-  ( ( n e. NN /\ m e. NN ) -> ( ( ( 1st ` p ) e. ( EE ` n ) /\ ( 1st ` p ) e. ( EE ` m ) ) -> ( ( x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) /\ y = ( iota_ r e. ( EE ` m ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) -> x = y ) ) )
19 7 8 18 syl2ani 
 |-  ( ( n e. NN /\ m e. NN ) -> ( ( p e. ( ( EE ` n ) X. ( EE ` n ) ) /\ p e. ( ( EE ` m ) X. ( EE ` m ) ) ) -> ( ( x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) /\ y = ( iota_ r e. ( EE ` m ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) -> x = y ) ) )
20 19 impd 
 |-  ( ( n e. NN /\ m e. NN ) -> ( ( ( p e. ( ( EE ` n ) X. ( EE ` n ) ) /\ p e. ( ( EE ` m ) X. ( EE ` m ) ) ) /\ ( x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) /\ y = ( iota_ r e. ( EE ` m ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) ) -> x = y ) )
21 6 20 syl5 
 |-  ( ( n e. NN /\ m 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 ) ) ) /\ ( ( p e. ( ( EE ` m ) X. ( EE ` m ) ) /\ q e. ( ( EE ` m ) X. ( EE ` m ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) /\ y = ( iota_ r e. ( EE ` m ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) ) -> x = y ) )
22 21 rexlimivv 
 |-  ( E. n e. NN E. m 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 ) ) ) /\ ( ( p e. ( ( EE ` m ) X. ( EE ` m ) ) /\ q e. ( ( EE ` m ) X. ( EE ` m ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) /\ y = ( iota_ r e. ( EE ` m ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) ) -> x = y )
23 1 22 sylbir 
 |-  ( ( 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 ) ) ) /\ E. m e. NN ( ( p e. ( ( EE ` m ) X. ( EE ` m ) ) /\ q e. ( ( EE ` m ) X. ( EE ` m ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) /\ y = ( iota_ r e. ( EE ` m ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) ) -> x = y )
24 23 gen2 
 |-  A. x A. y ( ( 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 ) ) ) /\ E. m e. NN ( ( p e. ( ( EE ` m ) X. ( EE ` m ) ) /\ q e. ( ( EE ` m ) X. ( EE ` m ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) /\ y = ( iota_ r e. ( EE ` m ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) ) -> x = y )
25 eqeq1 
 |-  ( x = y -> ( x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) <-> y = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) )
26 25 anbi2d 
 |-  ( x = y -> ( ( ( 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 ) ) ) <-> ( ( p e. ( ( EE ` n ) X. ( EE ` n ) ) /\ q e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) /\ y = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) ) )
27 26 rexbidv 
 |-  ( x = y -> ( 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 ) ) ) <-> E. n e. NN ( ( p e. ( ( EE ` n ) X. ( EE ` n ) ) /\ q e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) /\ y = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) ) )
28 10 sqxpeqd 
 |-  ( n = m -> ( ( EE ` n ) X. ( EE ` n ) ) = ( ( EE ` m ) X. ( EE ` m ) ) )
29 28 eleq2d 
 |-  ( n = m -> ( p e. ( ( EE ` n ) X. ( EE ` n ) ) <-> p e. ( ( EE ` m ) X. ( EE ` m ) ) ) )
30 28 eleq2d 
 |-  ( n = m -> ( q e. ( ( EE ` n ) X. ( EE ` n ) ) <-> q e. ( ( EE ` m ) X. ( EE ` m ) ) ) )
31 29 30 3anbi12d 
 |-  ( n = m -> ( ( p e. ( ( EE ` n ) X. ( EE ` n ) ) /\ q e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) <-> ( p e. ( ( EE ` m ) X. ( EE ` m ) ) /\ q e. ( ( EE ` m ) X. ( EE ` m ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) ) )
32 31 12 anbi12d 
 |-  ( n = m -> ( ( ( p e. ( ( EE ` n ) X. ( EE ` n ) ) /\ q e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) /\ y = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) <-> ( ( p e. ( ( EE ` m ) X. ( EE ` m ) ) /\ q e. ( ( EE ` m ) X. ( EE ` m ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) /\ y = ( iota_ r e. ( EE ` m ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) ) )
33 32 cbvrexvw 
 |-  ( E. n e. NN ( ( p e. ( ( EE ` n ) X. ( EE ` n ) ) /\ q e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) /\ y = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) <-> E. m e. NN ( ( p e. ( ( EE ` m ) X. ( EE ` m ) ) /\ q e. ( ( EE ` m ) X. ( EE ` m ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) /\ y = ( iota_ r e. ( EE ` m ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) )
34 27 33 bitrdi 
 |-  ( x = y -> ( 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 ) ) ) <-> E. m e. NN ( ( p e. ( ( EE ` m ) X. ( EE ` m ) ) /\ q e. ( ( EE ` m ) X. ( EE ` m ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) /\ y = ( iota_ r e. ( EE ` m ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) ) )
35 34 mo4 
 |-  ( E* 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 ) ) ) <-> A. x A. y ( ( 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 ) ) ) /\ E. m e. NN ( ( p e. ( ( EE ` m ) X. ( EE ` m ) ) /\ q e. ( ( EE ` m ) X. ( EE ` m ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) /\ y = ( iota_ r e. ( EE ` m ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) ) -> x = y ) )
36 24 35 mpbir 
 |-  E* 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 ) ) )
37 36 funoprab 
 |-  Fun { <. <. 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 ) ) ) }
38 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 ) ) ) }
39 38 funeqi 
 |-  ( Fun TransportTo <-> Fun { <. <. 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 ) ) ) } )
40 37 39 mpbir 
 |-  Fun TransportTo