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 ( 𝜑𝐺 : 𝑆1-1-onto𝑇 )
fcobij.2 ( 𝜑𝑅𝑈 )
fcobij.3 ( 𝜑𝑆𝑉 )
fcobij.4 ( 𝜑𝑇𝑊 )
Assertion fcobij ( 𝜑 → ( 𝑓 ∈ ( 𝑆m 𝑅 ) ↦ ( 𝐺𝑓 ) ) : ( 𝑆m 𝑅 ) –1-1-onto→ ( 𝑇m 𝑅 ) )

Proof

Step Hyp Ref Expression
1 fcobij.1 ( 𝜑𝐺 : 𝑆1-1-onto𝑇 )
2 fcobij.2 ( 𝜑𝑅𝑈 )
3 fcobij.3 ( 𝜑𝑆𝑉 )
4 fcobij.4 ( 𝜑𝑇𝑊 )
5 eqid ( 𝑓 ∈ ( 𝑆m 𝑅 ) ↦ ( 𝐺𝑓 ) ) = ( 𝑓 ∈ ( 𝑆m 𝑅 ) ↦ ( 𝐺𝑓 ) )
6 f1of ( 𝐺 : 𝑆1-1-onto𝑇𝐺 : 𝑆𝑇 )
7 1 6 syl ( 𝜑𝐺 : 𝑆𝑇 )
8 7 adantr ( ( 𝜑𝑓 ∈ ( 𝑆m 𝑅 ) ) → 𝐺 : 𝑆𝑇 )
9 3 2 elmapd ( 𝜑 → ( 𝑓 ∈ ( 𝑆m 𝑅 ) ↔ 𝑓 : 𝑅𝑆 ) )
10 9 biimpa ( ( 𝜑𝑓 ∈ ( 𝑆m 𝑅 ) ) → 𝑓 : 𝑅𝑆 )
11 fco ( ( 𝐺 : 𝑆𝑇𝑓 : 𝑅𝑆 ) → ( 𝐺𝑓 ) : 𝑅𝑇 )
12 8 10 11 syl2anc ( ( 𝜑𝑓 ∈ ( 𝑆m 𝑅 ) ) → ( 𝐺𝑓 ) : 𝑅𝑇 )
13 4 2 elmapd ( 𝜑 → ( ( 𝐺𝑓 ) ∈ ( 𝑇m 𝑅 ) ↔ ( 𝐺𝑓 ) : 𝑅𝑇 ) )
14 13 adantr ( ( 𝜑𝑓 ∈ ( 𝑆m 𝑅 ) ) → ( ( 𝐺𝑓 ) ∈ ( 𝑇m 𝑅 ) ↔ ( 𝐺𝑓 ) : 𝑅𝑇 ) )
15 12 14 mpbird ( ( 𝜑𝑓 ∈ ( 𝑆m 𝑅 ) ) → ( 𝐺𝑓 ) ∈ ( 𝑇m 𝑅 ) )
16 f1ocnv ( 𝐺 : 𝑆1-1-onto𝑇 𝐺 : 𝑇1-1-onto𝑆 )
17 f1of ( 𝐺 : 𝑇1-1-onto𝑆 𝐺 : 𝑇𝑆 )
18 1 16 17 3syl ( 𝜑 𝐺 : 𝑇𝑆 )
19 18 adantr ( ( 𝜑 ∈ ( 𝑇m 𝑅 ) ) → 𝐺 : 𝑇𝑆 )
20 4 2 elmapd ( 𝜑 → ( ∈ ( 𝑇m 𝑅 ) ↔ : 𝑅𝑇 ) )
21 20 biimpa ( ( 𝜑 ∈ ( 𝑇m 𝑅 ) ) → : 𝑅𝑇 )
22 fco ( ( 𝐺 : 𝑇𝑆 : 𝑅𝑇 ) → ( 𝐺 ) : 𝑅𝑆 )
23 19 21 22 syl2anc ( ( 𝜑 ∈ ( 𝑇m 𝑅 ) ) → ( 𝐺 ) : 𝑅𝑆 )
24 3 2 elmapd ( 𝜑 → ( ( 𝐺 ) ∈ ( 𝑆m 𝑅 ) ↔ ( 𝐺 ) : 𝑅𝑆 ) )
25 24 adantr ( ( 𝜑 ∈ ( 𝑇m 𝑅 ) ) → ( ( 𝐺 ) ∈ ( 𝑆m 𝑅 ) ↔ ( 𝐺 ) : 𝑅𝑆 ) )
26 23 25 mpbird ( ( 𝜑 ∈ ( 𝑇m 𝑅 ) ) → ( 𝐺 ) ∈ ( 𝑆m 𝑅 ) )
27 simpr ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆m 𝑅 ) ∧ ∈ ( 𝑇m 𝑅 ) ) ) ∧ 𝑓 = ( 𝐺 ) ) → 𝑓 = ( 𝐺 ) )
28 27 coeq2d ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆m 𝑅 ) ∧ ∈ ( 𝑇m 𝑅 ) ) ) ∧ 𝑓 = ( 𝐺 ) ) → ( 𝐺𝑓 ) = ( 𝐺 ∘ ( 𝐺 ) ) )
29 coass ( ( 𝐺 𝐺 ) ∘ ) = ( 𝐺 ∘ ( 𝐺 ) )
30 28 29 eqtr4di ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆m 𝑅 ) ∧ ∈ ( 𝑇m 𝑅 ) ) ) ∧ 𝑓 = ( 𝐺 ) ) → ( 𝐺𝑓 ) = ( ( 𝐺 𝐺 ) ∘ ) )
31 simpll ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆m 𝑅 ) ∧ ∈ ( 𝑇m 𝑅 ) ) ) ∧ 𝑓 = ( 𝐺 ) ) → 𝜑 )
32 f1ococnv2 ( 𝐺 : 𝑆1-1-onto𝑇 → ( 𝐺 𝐺 ) = ( I ↾ 𝑇 ) )
33 31 1 32 3syl ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆m 𝑅 ) ∧ ∈ ( 𝑇m 𝑅 ) ) ) ∧ 𝑓 = ( 𝐺 ) ) → ( 𝐺 𝐺 ) = ( I ↾ 𝑇 ) )
34 33 coeq1d ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆m 𝑅 ) ∧ ∈ ( 𝑇m 𝑅 ) ) ) ∧ 𝑓 = ( 𝐺 ) ) → ( ( 𝐺 𝐺 ) ∘ ) = ( ( I ↾ 𝑇 ) ∘ ) )
35 simplrr ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆m 𝑅 ) ∧ ∈ ( 𝑇m 𝑅 ) ) ) ∧ 𝑓 = ( 𝐺 ) ) → ∈ ( 𝑇m 𝑅 ) )
36 31 35 21 syl2anc ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆m 𝑅 ) ∧ ∈ ( 𝑇m 𝑅 ) ) ) ∧ 𝑓 = ( 𝐺 ) ) → : 𝑅𝑇 )
37 fcoi2 ( : 𝑅𝑇 → ( ( I ↾ 𝑇 ) ∘ ) = )
38 36 37 syl ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆m 𝑅 ) ∧ ∈ ( 𝑇m 𝑅 ) ) ) ∧ 𝑓 = ( 𝐺 ) ) → ( ( I ↾ 𝑇 ) ∘ ) = )
39 30 34 38 3eqtrrd ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆m 𝑅 ) ∧ ∈ ( 𝑇m 𝑅 ) ) ) ∧ 𝑓 = ( 𝐺 ) ) → = ( 𝐺𝑓 ) )
40 simpr ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆m 𝑅 ) ∧ ∈ ( 𝑇m 𝑅 ) ) ) ∧ = ( 𝐺𝑓 ) ) → = ( 𝐺𝑓 ) )
41 40 coeq2d ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆m 𝑅 ) ∧ ∈ ( 𝑇m 𝑅 ) ) ) ∧ = ( 𝐺𝑓 ) ) → ( 𝐺 ) = ( 𝐺 ∘ ( 𝐺𝑓 ) ) )
42 coass ( ( 𝐺𝐺 ) ∘ 𝑓 ) = ( 𝐺 ∘ ( 𝐺𝑓 ) )
43 41 42 eqtr4di ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆m 𝑅 ) ∧ ∈ ( 𝑇m 𝑅 ) ) ) ∧ = ( 𝐺𝑓 ) ) → ( 𝐺 ) = ( ( 𝐺𝐺 ) ∘ 𝑓 ) )
44 simpll ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆m 𝑅 ) ∧ ∈ ( 𝑇m 𝑅 ) ) ) ∧ = ( 𝐺𝑓 ) ) → 𝜑 )
45 f1ococnv1 ( 𝐺 : 𝑆1-1-onto𝑇 → ( 𝐺𝐺 ) = ( I ↾ 𝑆 ) )
46 44 1 45 3syl ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆m 𝑅 ) ∧ ∈ ( 𝑇m 𝑅 ) ) ) ∧ = ( 𝐺𝑓 ) ) → ( 𝐺𝐺 ) = ( I ↾ 𝑆 ) )
47 46 coeq1d ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆m 𝑅 ) ∧ ∈ ( 𝑇m 𝑅 ) ) ) ∧ = ( 𝐺𝑓 ) ) → ( ( 𝐺𝐺 ) ∘ 𝑓 ) = ( ( I ↾ 𝑆 ) ∘ 𝑓 ) )
48 simplrl ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆m 𝑅 ) ∧ ∈ ( 𝑇m 𝑅 ) ) ) ∧ = ( 𝐺𝑓 ) ) → 𝑓 ∈ ( 𝑆m 𝑅 ) )
49 44 48 10 syl2anc ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆m 𝑅 ) ∧ ∈ ( 𝑇m 𝑅 ) ) ) ∧ = ( 𝐺𝑓 ) ) → 𝑓 : 𝑅𝑆 )
50 fcoi2 ( 𝑓 : 𝑅𝑆 → ( ( I ↾ 𝑆 ) ∘ 𝑓 ) = 𝑓 )
51 49 50 syl ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆m 𝑅 ) ∧ ∈ ( 𝑇m 𝑅 ) ) ) ∧ = ( 𝐺𝑓 ) ) → ( ( I ↾ 𝑆 ) ∘ 𝑓 ) = 𝑓 )
52 43 47 51 3eqtrrd ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆m 𝑅 ) ∧ ∈ ( 𝑇m 𝑅 ) ) ) ∧ = ( 𝐺𝑓 ) ) → 𝑓 = ( 𝐺 ) )
53 39 52 impbida ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆m 𝑅 ) ∧ ∈ ( 𝑇m 𝑅 ) ) ) → ( 𝑓 = ( 𝐺 ) ↔ = ( 𝐺𝑓 ) ) )
54 5 15 26 53 f1o2d ( 𝜑 → ( 𝑓 ∈ ( 𝑆m 𝑅 ) ↦ ( 𝐺𝑓 ) ) : ( 𝑆m 𝑅 ) –1-1-onto→ ( 𝑇m 𝑅 ) )