Metamath Proof Explorer

Theorem caofcan

Description: Transfer a cancellation law like mulcan to the function operation. (Contributed by Steve Rodriguez, 16-Nov-2015)

Ref Expression
Hypotheses caofcan.1 
|- ( ph -> A e. V )
caofcan.2 
|- ( ph -> F : A --> T )
caofcan.3 
|- ( ph -> G : A --> S )
caofcan.4 
|- ( ph -> H : A --> S )
caofcan.5 
|- ( ( ph /\ ( x e. T /\ y e. S /\ z e. S ) ) -> ( ( x R y ) = ( x R z ) <-> y = z ) )
Assertion caofcan 
|- ( ph -> ( ( F oF R G ) = ( F oF R H ) <-> G = H ) )

Proof

Step Hyp Ref Expression
1 caofcan.1 
 |-  ( ph -> A e. V )
2 caofcan.2 
 |-  ( ph -> F : A --> T )
3 caofcan.3 
 |-  ( ph -> G : A --> S )
4 caofcan.4 
 |-  ( ph -> H : A --> S )
5 caofcan.5 
 |-  ( ( ph /\ ( x e. T /\ y e. S /\ z e. S ) ) -> ( ( x R y ) = ( x R z ) <-> y = z ) )
6 2 ffnd 
 |-  ( ph -> F Fn A )
7 3 ffnd 
 |-  ( ph -> G Fn A )
8 inidm 
 |-  ( A i^i A ) = A
9 eqidd 
 |-  ( ( ph /\ w e. A ) -> ( F ` w ) = ( F ` w ) )
10 eqidd 
 |-  ( ( ph /\ w e. A ) -> ( G ` w ) = ( G ` w ) )
11 6 7 1 1 8 9 10 ofval 
 |-  ( ( ph /\ w e. A ) -> ( ( F oF R G ) ` w ) = ( ( F ` w ) R ( G ` w ) ) )
12 4 ffnd 
 |-  ( ph -> H Fn A )
13 eqidd 
 |-  ( ( ph /\ w e. A ) -> ( H ` w ) = ( H ` w ) )
14 6 12 1 1 8 9 13 ofval 
 |-  ( ( ph /\ w e. A ) -> ( ( F oF R H ) ` w ) = ( ( F ` w ) R ( H ` w ) ) )
15 11 14 eqeq12d 
 |-  ( ( ph /\ w e. A ) -> ( ( ( F oF R G ) ` w ) = ( ( F oF R H ) ` w ) <-> ( ( F ` w ) R ( G ` w ) ) = ( ( F ` w ) R ( H ` w ) ) ) )
16 simpl 
 |-  ( ( ph /\ w e. A ) -> ph )
17 2 ffvelrnda 
 |-  ( ( ph /\ w e. A ) -> ( F ` w ) e. T )
18 3 ffvelrnda 
 |-  ( ( ph /\ w e. A ) -> ( G ` w ) e. S )
19 4 ffvelrnda 
 |-  ( ( ph /\ w e. A ) -> ( H ` w ) e. S )
20 5 caovcang 
 |-  ( ( ph /\ ( ( F ` w ) e. T /\ ( G ` w ) e. S /\ ( H ` w ) e. S ) ) -> ( ( ( F ` w ) R ( G ` w ) ) = ( ( F ` w ) R ( H ` w ) ) <-> ( G ` w ) = ( H ` w ) ) )
21 16 17 18 19 20 syl13anc 
 |-  ( ( ph /\ w e. A ) -> ( ( ( F ` w ) R ( G ` w ) ) = ( ( F ` w ) R ( H ` w ) ) <-> ( G ` w ) = ( H ` w ) ) )
22 15 21 bitrd 
 |-  ( ( ph /\ w e. A ) -> ( ( ( F oF R G ) ` w ) = ( ( F oF R H ) ` w ) <-> ( G ` w ) = ( H ` w ) ) )
23 22 ralbidva 
 |-  ( ph -> ( A. w e. A ( ( F oF R G ) ` w ) = ( ( F oF R H ) ` w ) <-> A. w e. A ( G ` w ) = ( H ` w ) ) )
24 6 7 1 1 8 offn 
 |-  ( ph -> ( F oF R G ) Fn A )
25 6 12 1 1 8 offn 
 |-  ( ph -> ( F oF R H ) Fn A )
26 eqfnfv 
 |-  ( ( ( F oF R G ) Fn A /\ ( F oF R H ) Fn A ) -> ( ( F oF R G ) = ( F oF R H ) <-> A. w e. A ( ( F oF R G ) ` w ) = ( ( F oF R H ) ` w ) ) )
27 24 25 26 syl2anc 
 |-  ( ph -> ( ( F oF R G ) = ( F oF R H ) <-> A. w e. A ( ( F oF R G ) ` w ) = ( ( F oF R H ) ` w ) ) )
28 eqfnfv 
 |-  ( ( G Fn A /\ H Fn A ) -> ( G = H <-> A. w e. A ( G ` w ) = ( H ` w ) ) )
29 7 12 28 syl2anc 
 |-  ( ph -> ( G = H <-> A. w e. A ( G ` w ) = ( H ` w ) ) )
30 23 27 29 3bitr4d 
 |-  ( ph -> ( ( F oF R G ) = ( F oF R H ) <-> G = H ) )