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 𝑅 ) )