Metamath Proof Explorer

Theorem fcobij

Description: Composing functions with a bijection yields a bijection between sets of functions. (Contributed by Thierry Arnoux, 25-Aug-2017)

Ref Expression
Hypotheses fcobij.1 
|- ( ph -> G : S -1-1-onto-> T )
fcobij.2 
|- ( ph -> R e. U )
fcobij.3 
|- ( ph -> S e. V )
fcobij.4 
|- ( ph -> T e. W )
Assertion fcobij 
|- ( ph -> ( f e. ( S ^m R ) |-> ( G o. f ) ) : ( S ^m R ) -1-1-onto-> ( T ^m R ) )

Proof

Step Hyp Ref Expression
1 fcobij.1 
 |-  ( ph -> G : S -1-1-onto-> T )
2 fcobij.2 
 |-  ( ph -> R e. U )
3 fcobij.3 
 |-  ( ph -> S e. V )
4 fcobij.4 
 |-  ( ph -> T e. W )
5 eqid 
 |-  ( f e. ( S ^m R ) |-> ( G o. f ) ) = ( f e. ( S ^m R ) |-> ( G o. f ) )
6 f1of 
 |-  ( G : S -1-1-onto-> T -> G : S --> T )
7 1 6 syl 
 |-  ( ph -> G : S --> T )
8 7 adantr 
 |-  ( ( ph /\ f e. ( S ^m R ) ) -> G : S --> T )
9 3 2 elmapd 
 |-  ( ph -> ( f e. ( S ^m R ) <-> f : R --> S ) )
10 9 biimpa 
 |-  ( ( ph /\ f e. ( S ^m R ) ) -> f : R --> S )
11 fco 
 |-  ( ( G : S --> T /\ f : R --> S ) -> ( G o. f ) : R --> T )
12 8 10 11 syl2anc 
 |-  ( ( ph /\ f e. ( S ^m R ) ) -> ( G o. f ) : R --> T )
13 4 2 elmapd 
 |-  ( ph -> ( ( G o. f ) e. ( T ^m R ) <-> ( G o. f ) : R --> T ) )
14 13 adantr 
 |-  ( ( ph /\ f e. ( S ^m R ) ) -> ( ( G o. f ) e. ( T ^m R ) <-> ( G o. f ) : R --> T ) )
15 12 14 mpbird 
 |-  ( ( ph /\ f e. ( S ^m R ) ) -> ( G o. f ) e. ( T ^m R ) )
16 f1ocnv 
 |-  ( G : S -1-1-onto-> T -> `' G : T -1-1-onto-> S )
17 f1of 
 |-  ( `' G : T -1-1-onto-> S -> `' G : T --> S )
18 1 16 17 3syl 
 |-  ( ph -> `' G : T --> S )
19 18 adantr 
 |-  ( ( ph /\ h e. ( T ^m R ) ) -> `' G : T --> S )
20 4 2 elmapd 
 |-  ( ph -> ( h e. ( T ^m R ) <-> h : R --> T ) )
21 20 biimpa 
 |-  ( ( ph /\ h e. ( T ^m R ) ) -> h : R --> T )
22 fco 
 |-  ( ( `' G : T --> S /\ h : R --> T ) -> ( `' G o. h ) : R --> S )
23 19 21 22 syl2anc 
 |-  ( ( ph /\ h e. ( T ^m R ) ) -> ( `' G o. h ) : R --> S )
24 3 2 elmapd 
 |-  ( ph -> ( ( `' G o. h ) e. ( S ^m R ) <-> ( `' G o. h ) : R --> S ) )
25 24 adantr 
 |-  ( ( ph /\ h e. ( T ^m R ) ) -> ( ( `' G o. h ) e. ( S ^m R ) <-> ( `' G o. h ) : R --> S ) )
26 23 25 mpbird 
 |-  ( ( ph /\ h e. ( T ^m R ) ) -> ( `' G o. h ) e. ( S ^m R ) )
27 simpr 
 |-  ( ( ( ph /\ ( f e. ( S ^m R ) /\ h e. ( T ^m R ) ) ) /\ f = ( `' G o. h ) ) -> f = ( `' G o. h ) )
28 27 coeq2d 
 |-  ( ( ( ph /\ ( f e. ( S ^m R ) /\ h e. ( T ^m R ) ) ) /\ f = ( `' G o. h ) ) -> ( G o. f ) = ( G o. ( `' G o. h ) ) )
29 coass 
 |-  ( ( G o. `' G ) o. h ) = ( G o. ( `' G o. h ) )
30 28 29 eqtr4di 
 |-  ( ( ( ph /\ ( f e. ( S ^m R ) /\ h e. ( T ^m R ) ) ) /\ f = ( `' G o. h ) ) -> ( G o. f ) = ( ( G o. `' G ) o. h ) )
31 simpll 
 |-  ( ( ( ph /\ ( f e. ( S ^m R ) /\ h e. ( T ^m R ) ) ) /\ f = ( `' G o. h ) ) -> ph )
32 f1ococnv2 
 |-  ( G : S -1-1-onto-> T -> ( G o. `' G ) = ( _I |` T ) )
33 31 1 32 3syl 
 |-  ( ( ( ph /\ ( f e. ( S ^m R ) /\ h e. ( T ^m R ) ) ) /\ f = ( `' G o. h ) ) -> ( G o. `' G ) = ( _I |` T ) )
34 33 coeq1d 
 |-  ( ( ( ph /\ ( f e. ( S ^m R ) /\ h e. ( T ^m R ) ) ) /\ f = ( `' G o. h ) ) -> ( ( G o. `' G ) o. h ) = ( ( _I |` T ) o. h ) )
35 simplrr 
 |-  ( ( ( ph /\ ( f e. ( S ^m R ) /\ h e. ( T ^m R ) ) ) /\ f = ( `' G o. h ) ) -> h e. ( T ^m R ) )
36 31 35 21 syl2anc 
 |-  ( ( ( ph /\ ( f e. ( S ^m R ) /\ h e. ( T ^m R ) ) ) /\ f = ( `' G o. h ) ) -> h : R --> T )
37 fcoi2 
 |-  ( h : R --> T -> ( ( _I |` T ) o. h ) = h )
38 36 37 syl 
 |-  ( ( ( ph /\ ( f e. ( S ^m R ) /\ h e. ( T ^m R ) ) ) /\ f = ( `' G o. h ) ) -> ( ( _I |` T ) o. h ) = h )
39 30 34 38 3eqtrrd 
 |-  ( ( ( ph /\ ( f e. ( S ^m R ) /\ h e. ( T ^m R ) ) ) /\ f = ( `' G o. h ) ) -> h = ( G o. f ) )
40 simpr 
 |-  ( ( ( ph /\ ( f e. ( S ^m R ) /\ h e. ( T ^m R ) ) ) /\ h = ( G o. f ) ) -> h = ( G o. f ) )
41 40 coeq2d 
 |-  ( ( ( ph /\ ( f e. ( S ^m R ) /\ h e. ( T ^m R ) ) ) /\ h = ( G o. f ) ) -> ( `' G o. h ) = ( `' G o. ( G o. f ) ) )
42 coass 
 |-  ( ( `' G o. G ) o. f ) = ( `' G o. ( G o. f ) )
43 41 42 eqtr4di 
 |-  ( ( ( ph /\ ( f e. ( S ^m R ) /\ h e. ( T ^m R ) ) ) /\ h = ( G o. f ) ) -> ( `' G o. h ) = ( ( `' G o. G ) o. f ) )
44 simpll 
 |-  ( ( ( ph /\ ( f e. ( S ^m R ) /\ h e. ( T ^m R ) ) ) /\ h = ( G o. f ) ) -> ph )
45 f1ococnv1 
 |-  ( G : S -1-1-onto-> T -> ( `' G o. G ) = ( _I |` S ) )
46 44 1 45 3syl 
 |-  ( ( ( ph /\ ( f e. ( S ^m R ) /\ h e. ( T ^m R ) ) ) /\ h = ( G o. f ) ) -> ( `' G o. G ) = ( _I |` S ) )
47 46 coeq1d 
 |-  ( ( ( ph /\ ( f e. ( S ^m R ) /\ h e. ( T ^m R ) ) ) /\ h = ( G o. f ) ) -> ( ( `' G o. G ) o. f ) = ( ( _I |` S ) o. f ) )
48 simplrl 
 |-  ( ( ( ph /\ ( f e. ( S ^m R ) /\ h e. ( T ^m R ) ) ) /\ h = ( G o. f ) ) -> f e. ( S ^m R ) )
49 44 48 10 syl2anc 
 |-  ( ( ( ph /\ ( f e. ( S ^m R ) /\ h e. ( T ^m R ) ) ) /\ h = ( G o. f ) ) -> f : R --> S )
50 fcoi2 
 |-  ( f : R --> S -> ( ( _I |` S ) o. f ) = f )
51 49 50 syl 
 |-  ( ( ( ph /\ ( f e. ( S ^m R ) /\ h e. ( T ^m R ) ) ) /\ h = ( G o. f ) ) -> ( ( _I |` S ) o. f ) = f )
52 43 47 51 3eqtrrd 
 |-  ( ( ( ph /\ ( f e. ( S ^m R ) /\ h e. ( T ^m R ) ) ) /\ h = ( G o. f ) ) -> f = ( `' G o. h ) )
53 39 52 impbida 
 |-  ( ( ph /\ ( f e. ( S ^m R ) /\ h e. ( T ^m R ) ) ) -> ( f = ( `' G o. h ) <-> h = ( G o. f ) ) )
54 5 15 26 53 f1o2d 
 |-  ( ph -> ( f e. ( S ^m R ) |-> ( G o. f ) ) : ( S ^m R ) -1-1-onto-> ( T ^m R ) )