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 ) )