Description: The transposition of the value of a function operation for two functions is the value of the function operation for the two functions transposed. (Contributed by Stefan O'Rear, 17-Jul-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | oftpos | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex | |
|
2 | 1 | adantr | |
3 | elex | |
|
4 | 3 | adantl | |
5 | funmpt | |
|
6 | 5 | a1i | |
7 | dftpos4 | |
|
8 | tposexg | |
|
9 | 8 | adantr | |
10 | 7 9 | eqeltrrid | |
11 | dftpos4 | |
|
12 | tposexg | |
|
13 | 12 | adantl | |
14 | 11 13 | eqeltrrid | |
15 | ofco2 | |
|
16 | 2 4 6 10 14 15 | syl23anc | |
17 | dftpos4 | |
|
18 | 7 11 | oveq12i | |
19 | 16 17 18 | 3eqtr4g | |