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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reeanv | |
|
2 | simp1 | |
|
3 | simp1 | |
|
4 | 2 3 | anim12i | |
5 | 4 | anim1i | |
6 | 5 | an4s | |
7 | xp1st | |
|
8 | xp1st | |
|
9 | axdimuniq | |
|
10 | fveq2 | |
|
11 | 10 | riotaeqdv | |
12 | 11 | eqeq2d | |
13 | 12 | anbi2d | |
14 | eqtr3 | |
|
15 | 13 14 | syl6bir | |
16 | 9 15 | syl | |
17 | 16 | an4s | |
18 | 17 | ex | |
19 | 7 8 18 | syl2ani | |
20 | 19 | impd | |
21 | 6 20 | syl5 | |
22 | 21 | rexlimivv | |
23 | 1 22 | sylbir | |
24 | 23 | gen2 | |
25 | eqeq1 | |
|
26 | 25 | anbi2d | |
27 | 26 | rexbidv | |
28 | 10 | sqxpeqd | |
29 | 28 | eleq2d | |
30 | 28 | eleq2d | |
31 | 29 30 | 3anbi12d | |
32 | 31 12 | anbi12d | |
33 | 32 | cbvrexvw | |
34 | 27 33 | bitrdi | |
35 | 34 | mo4 | |
36 | 24 35 | mpbir | |
37 | 36 | funoprab | |
38 | df-transport | |
|
39 | 38 | funeqi | |
40 | 37 39 | mpbir | |