Description: The functionalization of the involution component of a structure. (Contributed by Mario Carneiro, 6-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | staffval.b | |
|
staffval.i | |
||
staffval.f | |
||
Assertion | staffval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | staffval.b | |
|
2 | staffval.i | |
|
3 | staffval.f | |
|
4 | fveq2 | |
|
5 | 4 1 | eqtr4di | |
6 | fveq2 | |
|
7 | 6 2 | eqtr4di | |
8 | 7 | fveq1d | |
9 | 5 8 | mpteq12dv | |
10 | df-staf | |
|
11 | eqid | |
|
12 | fvrn0 | |
|
13 | 12 | a1i | |
14 | 11 13 | fmpti | |
15 | 1 | fvexi | |
16 | 2 | fvexi | |
17 | 16 | rnex | |
18 | p0ex | |
|
19 | 17 18 | unex | |
20 | fex2 | |
|
21 | 14 15 19 20 | mp3an | |
22 | 9 10 21 | fvmpt | |
23 | fvprc | |
|
24 | mpt0 | |
|
25 | 23 24 | eqtr4di | |
26 | fvprc | |
|
27 | 1 26 | eqtrid | |
28 | 27 | mpteq1d | |
29 | 25 28 | eqtr4d | |
30 | 22 29 | pm2.61i | |
31 | 3 30 | eqtri | |