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
|- ( ph -> A e. V )
caofref.2
|- ( ph -> F : A --> S )
caofcom.3
|- ( ph -> G : A --> S )
caofass.4
|- ( ph -> H : A --> S )
caoftrn.5
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x R y /\ y T z ) -> x U z ) )
Assertion caoftrn
|- ( ph -> ( ( F oR R G /\ G oR T H ) -> F oR U H ) )

Proof

Step Hyp Ref Expression
1 caofref.1
 |-  ( ph -> A e. V )
2 caofref.2
 |-  ( ph -> F : A --> S )
3 caofcom.3
 |-  ( ph -> G : A --> S )
4 caofass.4
 |-  ( ph -> H : A --> S )
5 caoftrn.5
 |-  ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x R y /\ y T z ) -> x U z ) )
6 5 ralrimivvva
 |-  ( ph -> A. x e. S A. y e. S A. z e. S ( ( x R y /\ y T z ) -> x U z ) )
7 6 adantr
 |-  ( ( ph /\ w e. A ) -> A. x e. S A. y e. S A. z e. S ( ( x R y /\ y T z ) -> x U z ) )
8 2 ffvelrnda
 |-  ( ( ph /\ w e. A ) -> ( F ` w ) e. S )
9 3 ffvelrnda
 |-  ( ( ph /\ w e. A ) -> ( G ` w ) e. S )
10 4 ffvelrnda
 |-  ( ( ph /\ w e. A ) -> ( H ` w ) e. 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 ) e. S /\ ( G ` w ) e. S /\ ( H ` w ) e. S ) -> ( A. x e. S A. y e. S A. z e. 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
 |-  ( ( ph /\ w e. A ) -> ( A. x e. S A. y e. S A. z e. 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
 |-  ( ( ph /\ w e. A ) -> ( ( ( F ` w ) R ( G ` w ) /\ ( G ` w ) T ( H ` w ) ) -> ( F ` w ) U ( H ` w ) ) )
26 25 ralimdva
 |-  ( ph -> ( A. w e. A ( ( F ` w ) R ( G ` w ) /\ ( G ` w ) T ( H ` w ) ) -> A. w e. A ( F ` w ) U ( H ` w ) ) )
27 2 ffnd
 |-  ( ph -> F Fn A )
28 3 ffnd
 |-  ( ph -> G Fn A )
29 inidm
 |-  ( A i^i A ) = A
30 eqidd
 |-  ( ( ph /\ w e. A ) -> ( F ` w ) = ( F ` w ) )
31 eqidd
 |-  ( ( ph /\ w e. A ) -> ( G ` w ) = ( G ` w ) )
32 27 28 1 1 29 30 31 ofrfval
 |-  ( ph -> ( F oR R G <-> A. w e. A ( F ` w ) R ( G ` w ) ) )
33 4 ffnd
 |-  ( ph -> H Fn A )
34 eqidd
 |-  ( ( ph /\ w e. A ) -> ( H ` w ) = ( H ` w ) )
35 28 33 1 1 29 31 34 ofrfval
 |-  ( ph -> ( G oR T H <-> A. w e. A ( G ` w ) T ( H ` w ) ) )
36 32 35 anbi12d
 |-  ( ph -> ( ( F oR R G /\ G oR T H ) <-> ( A. w e. A ( F ` w ) R ( G ` w ) /\ A. w e. A ( G ` w ) T ( H ` w ) ) ) )
37 r19.26
 |-  ( A. w e. A ( ( F ` w ) R ( G ` w ) /\ ( G ` w ) T ( H ` w ) ) <-> ( A. w e. A ( F ` w ) R ( G ` w ) /\ A. w e. A ( G ` w ) T ( H ` w ) ) )
38 36 37 bitr4di
 |-  ( ph -> ( ( F oR R G /\ G oR T H ) <-> A. w e. A ( ( F ` w ) R ( G ` w ) /\ ( G ` w ) T ( H ` w ) ) ) )
39 27 33 1 1 29 30 34 ofrfval
 |-  ( ph -> ( F oR U H <-> A. w e. A ( F ` w ) U ( H ` w ) ) )
40 26 38 39 3imtr4d
 |-  ( ph -> ( ( F oR R G /\ G oR T H ) -> F oR U H ) )