Metamath Proof Explorer


Theorem caoftrn

Description: Transfer a transitivity law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014)

Ref Expression
Hypotheses caofref.1 φAV
caofref.2 φF:AS
caofcom.3 φG:AS
caofass.4 φH:AS
caoftrn.5 φxSySzSxRyyTzxUz
Assertion caoftrn φFRfGGTfHFUfH

Proof

Step Hyp Ref Expression
1 caofref.1 φAV
2 caofref.2 φF:AS
3 caofcom.3 φG:AS
4 caofass.4 φH:AS
5 caoftrn.5 φxSySzSxRyyTzxUz
6 5 ralrimivvva φxSySzSxRyyTzxUz
7 6 adantr φwAxSySzSxRyyTzxUz
8 2 ffvelrnda φwAFwS
9 3 ffvelrnda φwAGwS
10 4 ffvelrnda φwAHwS
11 breq1 x=FwxRyFwRy
12 11 anbi1d x=FwxRyyTzFwRyyTz
13 breq1 x=FwxUzFwUz
14 12 13 imbi12d x=FwxRyyTzxUzFwRyyTzFwUz
15 breq2 y=GwFwRyFwRGw
16 breq1 y=GwyTzGwTz
17 15 16 anbi12d y=GwFwRyyTzFwRGwGwTz
18 17 imbi1d y=GwFwRyyTzFwUzFwRGwGwTzFwUz
19 breq2 z=HwGwTzGwTHw
20 19 anbi2d z=HwFwRGwGwTzFwRGwGwTHw
21 breq2 z=HwFwUzFwUHw
22 20 21 imbi12d z=HwFwRGwGwTzFwUzFwRGwGwTHwFwUHw
23 14 18 22 rspc3v FwSGwSHwSxSySzSxRyyTzxUzFwRGwGwTHwFwUHw
24 8 9 10 23 syl3anc φwAxSySzSxRyyTzxUzFwRGwGwTHwFwUHw
25 7 24 mpd φwAFwRGwGwTHwFwUHw
26 25 ralimdva φwAFwRGwGwTHwwAFwUHw
27 2 ffnd φFFnA
28 3 ffnd φGFnA
29 inidm AA=A
30 eqidd φwAFw=Fw
31 eqidd φwAGw=Gw
32 27 28 1 1 29 30 31 ofrfval φFRfGwAFwRGw
33 4 ffnd φHFnA
34 eqidd φwAHw=Hw
35 28 33 1 1 29 31 34 ofrfval φGTfHwAGwTHw
36 32 35 anbi12d φFRfGGTfHwAFwRGwwAGwTHw
37 r19.26 wAFwRGwGwTHwwAFwRGwwAGwTHw
38 36 37 bitr4di φFRfGGTfHwAFwRGwGwTHw
39 27 33 1 1 29 30 34 ofrfval φFUfHwAFwUHw
40 26 38 39 3imtr4d φFRfGGTfHFUfH