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 FunTransportTo

Proof

Step Hyp Ref Expression
1 reeanv nmp𝔼n×𝔼nq𝔼n×𝔼n1stq2ndqx=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrpp𝔼m×𝔼mq𝔼m×𝔼m1stq2ndqy=ιr𝔼m|2ndqBtwn1stqr2ndqrCgrpnp𝔼n×𝔼nq𝔼n×𝔼n1stq2ndqx=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrpmp𝔼m×𝔼mq𝔼m×𝔼m1stq2ndqy=ιr𝔼m|2ndqBtwn1stqr2ndqrCgrp
2 simp1 p𝔼n×𝔼nq𝔼n×𝔼n1stq2ndqp𝔼n×𝔼n
3 simp1 p𝔼m×𝔼mq𝔼m×𝔼m1stq2ndqp𝔼m×𝔼m
4 2 3 anim12i p𝔼n×𝔼nq𝔼n×𝔼n1stq2ndqp𝔼m×𝔼mq𝔼m×𝔼m1stq2ndqp𝔼n×𝔼np𝔼m×𝔼m
5 4 anim1i p𝔼n×𝔼nq𝔼n×𝔼n1stq2ndqp𝔼m×𝔼mq𝔼m×𝔼m1stq2ndqx=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrpy=ιr𝔼m|2ndqBtwn1stqr2ndqrCgrpp𝔼n×𝔼np𝔼m×𝔼mx=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrpy=ιr𝔼m|2ndqBtwn1stqr2ndqrCgrp
6 5 an4s p𝔼n×𝔼nq𝔼n×𝔼n1stq2ndqx=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrpp𝔼m×𝔼mq𝔼m×𝔼m1stq2ndqy=ιr𝔼m|2ndqBtwn1stqr2ndqrCgrpp𝔼n×𝔼np𝔼m×𝔼mx=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrpy=ιr𝔼m|2ndqBtwn1stqr2ndqrCgrp
7 xp1st p𝔼n×𝔼n1stp𝔼n
8 xp1st p𝔼m×𝔼m1stp𝔼m
9 axdimuniq n1stp𝔼nm1stp𝔼mn=m
10 fveq2 n=m𝔼n=𝔼m
11 10 riotaeqdv n=mιr𝔼n|2ndqBtwn1stqr2ndqrCgrp=ιr𝔼m|2ndqBtwn1stqr2ndqrCgrp
12 11 eqeq2d n=my=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrpy=ιr𝔼m|2ndqBtwn1stqr2ndqrCgrp
13 12 anbi2d n=mx=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrpy=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrpx=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrpy=ιr𝔼m|2ndqBtwn1stqr2ndqrCgrp
14 eqtr3 x=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrpy=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrpx=y
15 13 14 syl6bir n=mx=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrpy=ιr𝔼m|2ndqBtwn1stqr2ndqrCgrpx=y
16 9 15 syl n1stp𝔼nm1stp𝔼mx=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrpy=ιr𝔼m|2ndqBtwn1stqr2ndqrCgrpx=y
17 16 an4s nm1stp𝔼n1stp𝔼mx=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrpy=ιr𝔼m|2ndqBtwn1stqr2ndqrCgrpx=y
18 17 ex nm1stp𝔼n1stp𝔼mx=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrpy=ιr𝔼m|2ndqBtwn1stqr2ndqrCgrpx=y
19 7 8 18 syl2ani nmp𝔼n×𝔼np𝔼m×𝔼mx=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrpy=ιr𝔼m|2ndqBtwn1stqr2ndqrCgrpx=y
20 19 impd nmp𝔼n×𝔼np𝔼m×𝔼mx=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrpy=ιr𝔼m|2ndqBtwn1stqr2ndqrCgrpx=y
21 6 20 syl5 nmp𝔼n×𝔼nq𝔼n×𝔼n1stq2ndqx=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrpp𝔼m×𝔼mq𝔼m×𝔼m1stq2ndqy=ιr𝔼m|2ndqBtwn1stqr2ndqrCgrpx=y
22 21 rexlimivv nmp𝔼n×𝔼nq𝔼n×𝔼n1stq2ndqx=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrpp𝔼m×𝔼mq𝔼m×𝔼m1stq2ndqy=ιr𝔼m|2ndqBtwn1stqr2ndqrCgrpx=y
23 1 22 sylbir np𝔼n×𝔼nq𝔼n×𝔼n1stq2ndqx=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrpmp𝔼m×𝔼mq𝔼m×𝔼m1stq2ndqy=ιr𝔼m|2ndqBtwn1stqr2ndqrCgrpx=y
24 23 gen2 xynp𝔼n×𝔼nq𝔼n×𝔼n1stq2ndqx=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrpmp𝔼m×𝔼mq𝔼m×𝔼m1stq2ndqy=ιr𝔼m|2ndqBtwn1stqr2ndqrCgrpx=y
25 eqeq1 x=yx=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrpy=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrp
26 25 anbi2d x=yp𝔼n×𝔼nq𝔼n×𝔼n1stq2ndqx=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrpp𝔼n×𝔼nq𝔼n×𝔼n1stq2ndqy=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrp
27 26 rexbidv x=ynp𝔼n×𝔼nq𝔼n×𝔼n1stq2ndqx=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrpnp𝔼n×𝔼nq𝔼n×𝔼n1stq2ndqy=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrp
28 10 sqxpeqd n=m𝔼n×𝔼n=𝔼m×𝔼m
29 28 eleq2d n=mp𝔼n×𝔼np𝔼m×𝔼m
30 28 eleq2d n=mq𝔼n×𝔼nq𝔼m×𝔼m
31 29 30 3anbi12d n=mp𝔼n×𝔼nq𝔼n×𝔼n1stq2ndqp𝔼m×𝔼mq𝔼m×𝔼m1stq2ndq
32 31 12 anbi12d n=mp𝔼n×𝔼nq𝔼n×𝔼n1stq2ndqy=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrpp𝔼m×𝔼mq𝔼m×𝔼m1stq2ndqy=ιr𝔼m|2ndqBtwn1stqr2ndqrCgrp
33 32 cbvrexvw np𝔼n×𝔼nq𝔼n×𝔼n1stq2ndqy=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrpmp𝔼m×𝔼mq𝔼m×𝔼m1stq2ndqy=ιr𝔼m|2ndqBtwn1stqr2ndqrCgrp
34 27 33 bitrdi x=ynp𝔼n×𝔼nq𝔼n×𝔼n1stq2ndqx=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrpmp𝔼m×𝔼mq𝔼m×𝔼m1stq2ndqy=ιr𝔼m|2ndqBtwn1stqr2ndqrCgrp
35 34 mo4 *xnp𝔼n×𝔼nq𝔼n×𝔼n1stq2ndqx=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrpxynp𝔼n×𝔼nq𝔼n×𝔼n1stq2ndqx=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrpmp𝔼m×𝔼mq𝔼m×𝔼m1stq2ndqy=ιr𝔼m|2ndqBtwn1stqr2ndqrCgrpx=y
36 24 35 mpbir *xnp𝔼n×𝔼nq𝔼n×𝔼n1stq2ndqx=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrp
37 36 funoprab Funpqx|np𝔼n×𝔼nq𝔼n×𝔼n1stq2ndqx=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrp
38 df-transport TransportTo=pqx|np𝔼n×𝔼nq𝔼n×𝔼n1stq2ndqx=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrp
39 38 funeqi FunTransportToFunpqx|np𝔼n×𝔼nq𝔼n×𝔼n1stq2ndqx=ιr𝔼n|2ndqBtwn1stqr2ndqrCgrp
40 37 39 mpbir FunTransportTo