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

Metamath Proof Explorer

Theorem caofrss

Description: Transfer a relation subset 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 )
caofrss.4 
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x R y -> x T y ) )
Assertion caofrss 
|- ( ph -> ( F oR R G -> F oR T G ) )

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 caofrss.4 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x R y -> x T y ) )
5 2 ffvelcdmda 
 |-  ( ( ph /\ w e. A ) -> ( F ` w ) e. S )
6 3 ffvelcdmda 
 |-  ( ( ph /\ w e. A ) -> ( G ` w ) e. S )
7 4 ralrimivva 
 |-  ( ph -> A. x e. S A. y e. S ( x R y -> x T y ) )
8 7 adantr 
 |-  ( ( ph /\ w e. A ) -> A. x e. S A. y e. S ( x R y -> x T y ) )
9 breq1 
 |-  ( x = ( F ` w ) -> ( x R y <-> ( F ` w ) R y ) )
10 breq1 
 |-  ( x = ( F ` w ) -> ( x T y <-> ( F ` w ) T y ) )
11 9 10 imbi12d 
 |-  ( x = ( F ` w ) -> ( ( x R y -> x T y ) <-> ( ( F ` w ) R y -> ( F ` w ) T y ) ) )
12 breq2 
 |-  ( y = ( G ` w ) -> ( ( F ` w ) R y <-> ( F ` w ) R ( G ` w ) ) )
13 breq2 
 |-  ( y = ( G ` w ) -> ( ( F ` w ) T y <-> ( F ` w ) T ( G ` w ) ) )
14 12 13 imbi12d 
 |-  ( y = ( G ` w ) -> ( ( ( F ` w ) R y -> ( F ` w ) T y ) <-> ( ( F ` w ) R ( G ` w ) -> ( F ` w ) T ( G ` w ) ) ) )
15 11 14 rspc2va 
 |-  ( ( ( ( F ` w ) e. S /\ ( G ` w ) e. S ) /\ A. x e. S A. y e. S ( x R y -> x T y ) ) -> ( ( F ` w ) R ( G ` w ) -> ( F ` w ) T ( G ` w ) ) )
16 5 6 8 15 syl21anc 
 |-  ( ( ph /\ w e. A ) -> ( ( F ` w ) R ( G ` w ) -> ( F ` w ) T ( G ` w ) ) )
17 16 ralimdva 
 |-  ( ph -> ( A. w e. A ( F ` w ) R ( G ` w ) -> A. w e. A ( F ` w ) T ( G ` w ) ) )
18 2 ffnd 
 |-  ( ph -> F Fn A )
19 3 ffnd 
 |-  ( ph -> G Fn A )
20 inidm 
 |-  ( A i^i A ) = A
21 eqidd 
 |-  ( ( ph /\ w e. A ) -> ( F ` w ) = ( F ` w ) )
22 eqidd 
 |-  ( ( ph /\ w e. A ) -> ( G ` w ) = ( G ` w ) )
23 18 19 1 1 20 21 22 ofrfval 
 |-  ( ph -> ( F oR R G <-> A. w e. A ( F ` w ) R ( G ` w ) ) )
24 18 19 1 1 20 21 22 ofrfval 
 |-  ( ph -> ( F oR T G <-> A. w e. A ( F ` w ) T ( G ` w ) ) )
25 17 23 24 3imtr4d 
 |-  ( ph -> ( F oR R G -> F oR T G ) )