Description: Transfer a transitivity law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | caofref.1 | |
|
caofref.2 | |
||
caofcom.3 | |
||
caofass.4 | |
||
caoftrn.5 | |
||
Assertion | caoftrn | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | caofref.1 | |
|
2 | caofref.2 | |
|
3 | caofcom.3 | |
|
4 | caofass.4 | |
|
5 | caoftrn.5 | |
|
6 | 5 | ralrimivvva | |
7 | 6 | adantr | |
8 | 2 | ffvelrnda | |
9 | 3 | ffvelrnda | |
10 | 4 | ffvelrnda | |
11 | breq1 | |
|
12 | 11 | anbi1d | |
13 | breq1 | |
|
14 | 12 13 | imbi12d | |
15 | breq2 | |
|
16 | breq1 | |
|
17 | 15 16 | anbi12d | |
18 | 17 | imbi1d | |
19 | breq2 | |
|
20 | 19 | anbi2d | |
21 | breq2 | |
|
22 | 20 21 | imbi12d | |
23 | 14 18 22 | rspc3v | |
24 | 8 9 10 23 | syl3anc | |
25 | 7 24 | mpd | |
26 | 25 | ralimdva | |
27 | 2 | ffnd | |
28 | 3 | ffnd | |
29 | inidm | |
|
30 | eqidd | |
|
31 | eqidd | |
|
32 | 27 28 1 1 29 30 31 | ofrfval | |
33 | 4 | ffnd | |
34 | eqidd | |
|
35 | 28 33 1 1 29 31 34 | ofrfval | |
36 | 32 35 | anbi12d | |
37 | r19.26 | |
|
38 | 36 37 | bitr4di | |
39 | 27 33 1 1 29 30 34 | ofrfval | |
40 | 26 38 39 | 3imtr4d | |