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 ffvelrnda
 |-  ( ( ph /\ w e. A ) -> ( F ` w ) e. S )
6 3 ffvelrnda
 |-  ( ( 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 ) )