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 φ A V
caofref.2 φ F : A S
caofcom.3 φ G : A S
caofass.4 φ H : A S
caoftrn.5 φ x S y S z S x R y y T z x U z
Assertion caoftrn φ F R f G G T f H F U f H

Proof

Step Hyp Ref Expression
1 caofref.1 φ A V
2 caofref.2 φ F : A S
3 caofcom.3 φ G : A S
4 caofass.4 φ H : A S
5 caoftrn.5 φ x S y S z S x R y y T z x U z
6 5 ralrimivvva φ x S y S z S x R y y T z x U z
7 6 adantr φ w A x S y S z S x R y y T z x U z
8 2 ffvelrnda φ w A F w S
9 3 ffvelrnda φ w A G w S
10 4 ffvelrnda φ w A H w S
11 breq1 x = F w x R y F w R y
12 11 anbi1d x = F w x R y y T z F w R y y T z
13 breq1 x = F w x U z F w U z
14 12 13 imbi12d x = F w x R y y T z x U z F w R y y T z F w U z
15 breq2 y = G w F w R y F w R G w
16 breq1 y = G w y T z G w T z
17 15 16 anbi12d y = G w F w R y y T z F w R G w G w T z
18 17 imbi1d y = G w F w R y y T z F w U z F w R G w G w T z F w U z
19 breq2 z = H w G w T z G w T H w
20 19 anbi2d z = H w F w R G w G w T z F w R G w G w T H w
21 breq2 z = H w F w U z F w U H w
22 20 21 imbi12d z = H w F w R G w G w T z F w U z F w R G w G w T H w F w U H w
23 14 18 22 rspc3v F w S G w S H w S x S y S z S x R y y T z x U z F w R G w G w T H w F w U H w
24 8 9 10 23 syl3anc φ w A x S y S z S x R y y T z x U z F w R G w G w T H w F w U H w
25 7 24 mpd φ w A F w R G w G w T H w F w U H w
26 25 ralimdva φ w A F w R G w G w T H w w A F w U H w
27 2 ffnd φ F Fn A
28 3 ffnd φ G Fn A
29 inidm A A = A
30 eqidd φ w A F w = F w
31 eqidd φ w A G w = G w
32 27 28 1 1 29 30 31 ofrfval φ F R f G w A F w R G w
33 4 ffnd φ H Fn A
34 eqidd φ w A H w = H w
35 28 33 1 1 29 31 34 ofrfval φ G T f H w A G w T H w
36 32 35 anbi12d φ F R f G G T f H w A F w R G w w A G w T H w
37 r19.26 w A F w R G w G w T H w w A F w R G w w A G w T H w
38 36 37 bitr4di φ F R f G G T f H w A F w R G w G w T H w
39 27 33 1 1 29 30 34 ofrfval φ F U f H w A F w U H w
40 26 38 39 3imtr4d φ F R f G G T f H F U f H