This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ofrco

Description: Function relation between function compositions. (Contributed by Thierry Arnoux, 15-Jan-2026)

Ref Expression
Hypotheses ofrco.1 
|- ( ph -> F Fn A )
ofrco.2 
|- ( ph -> G Fn A )
ofrco.3 
|- ( ph -> H : C --> A )
ofrco.4 
|- ( ph -> A e. V )
ofrco.5 
|- ( ph -> C e. W )
ofrco.6 
|- ( ph -> F oR R G )
Assertion ofrco 
|- ( ph -> ( F o. H ) oR R ( G o. H ) )

Proof

Step Hyp Ref Expression
1 ofrco.1 
 |-  ( ph -> F Fn A )
2 ofrco.2 
 |-  ( ph -> G Fn A )
3 ofrco.3 
 |-  ( ph -> H : C --> A )
4 ofrco.4 
 |-  ( ph -> A e. V )
5 ofrco.5 
 |-  ( ph -> C e. W )
6 ofrco.6 
 |-  ( ph -> F oR R G )
7 fveq2 
 |-  ( y = ( H ` x ) -> ( F ` y ) = ( F ` ( H ` x ) ) )
8 fveq2 
 |-  ( y = ( H ` x ) -> ( G ` y ) = ( G ` ( H ` x ) ) )
9 7 8 breq12d 
 |-  ( y = ( H ` x ) -> ( ( F ` y ) R ( G ` y ) <-> ( F ` ( H ` x ) ) R ( G ` ( H ` x ) ) ) )
10 inidm 
 |-  ( A i^i A ) = A
11 eqidd 
 |-  ( ( ph /\ y e. A ) -> ( F ` y ) = ( F ` y ) )
12 eqidd 
 |-  ( ( ph /\ y e. A ) -> ( G ` y ) = ( G ` y ) )
13 1 2 4 4 10 11 12 ofrfval 
 |-  ( ph -> ( F oR R G <-> A. y e. A ( F ` y ) R ( G ` y ) ) )
14 6 13 mpbid 
 |-  ( ph -> A. y e. A ( F ` y ) R ( G ` y ) )
15 14 adantr 
 |-  ( ( ph /\ x e. C ) -> A. y e. A ( F ` y ) R ( G ` y ) )
16 3 ffvelcdmda 
 |-  ( ( ph /\ x e. C ) -> ( H ` x ) e. A )
17 9 15 16 rspcdva 
 |-  ( ( ph /\ x e. C ) -> ( F ` ( H ` x ) ) R ( G ` ( H ` x ) ) )
18 17 ralrimiva 
 |-  ( ph -> A. x e. C ( F ` ( H ` x ) ) R ( G ` ( H ` x ) ) )
19 fnfco 
 |-  ( ( F Fn A /\ H : C --> A ) -> ( F o. H ) Fn C )
20 1 3 19 syl2anc 
 |-  ( ph -> ( F o. H ) Fn C )
21 fnfco 
 |-  ( ( G Fn A /\ H : C --> A ) -> ( G o. H ) Fn C )
22 2 3 21 syl2anc 
 |-  ( ph -> ( G o. H ) Fn C )
23 inidm 
 |-  ( C i^i C ) = C
24 3 adantr 
 |-  ( ( ph /\ x e. C ) -> H : C --> A )
25 simpr 
 |-  ( ( ph /\ x e. C ) -> x e. C )
26 24 25 fvco3d 
 |-  ( ( ph /\ x e. C ) -> ( ( F o. H ) ` x ) = ( F ` ( H ` x ) ) )
27 24 25 fvco3d 
 |-  ( ( ph /\ x e. C ) -> ( ( G o. H ) ` x ) = ( G ` ( H ` x ) ) )
28 20 22 5 5 23 26 27 ofrfval 
 |-  ( ph -> ( ( F o. H ) oR R ( G o. H ) <-> A. x e. C ( F ` ( H ` x ) ) R ( G ` ( H ` x ) ) ) )
29 18 28 mpbird 
 |-  ( ph -> ( F o. H ) oR R ( G o. H ) )