fmptco1f1o

Description: The action of composing (to the right) with a bijection is itself a bijection of functions. (Contributed by Thierry Arnoux, 3-Jan-2021)

	Ref	Expression
Hypotheses	fmptco1f1o.a	⊢ 𝐴 = ( 𝑅 ↑_m 𝐸 )
	fmptco1f1o.b	⊢ 𝐵 = ( 𝑅 ↑_m 𝐷 )
	fmptco1f1o.f	⊢ 𝐹 = ( 𝑓 ∈ 𝐴 ↦ ( 𝑓 ∘ 𝑇 ) )
	fmptco1f1o.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
	fmptco1f1o.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑊 )
	fmptco1f1o.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑋 )
	fmptco1f1o.t	⊢ ( 𝜑 → 𝑇 : 𝐷 –1-1-onto→ 𝐸 )
Assertion	fmptco1f1o	⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fmptco1f1o.a	⊢ 𝐴 = ( 𝑅 ↑_m 𝐸 )
2		fmptco1f1o.b	⊢ 𝐵 = ( 𝑅 ↑_m 𝐷 )
3		fmptco1f1o.f	⊢ 𝐹 = ( 𝑓 ∈ 𝐴 ↦ ( 𝑓 ∘ 𝑇 ) )
4		fmptco1f1o.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
5		fmptco1f1o.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑊 )
6		fmptco1f1o.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑋 )
7		fmptco1f1o.t	⊢ ( 𝜑 → 𝑇 : 𝐷 –1-1-onto→ 𝐸 )
8	3	a1i	⊢ ( 𝜑 → 𝐹 = ( 𝑓 ∈ 𝐴 ↦ ( 𝑓 ∘ 𝑇 ) ) )
9	6	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑅 ∈ 𝑋 )
10	4	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝐷 ∈ 𝑉 )
11		simpr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 ∈ 𝐴 )
12	11 1	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 ∈ ( 𝑅 ↑_m 𝐸 ) )
13		elmapi	⊢ ( 𝑓 ∈ ( 𝑅 ↑_m 𝐸 ) → 𝑓 : 𝐸 ⟶ 𝑅 )
14	12 13	syl	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝐸 ⟶ 𝑅 )
15		f1of	⊢ ( 𝑇 : 𝐷 –1-1-onto→ 𝐸 → 𝑇 : 𝐷 ⟶ 𝐸 )
16	7 15	syl	⊢ ( 𝜑 → 𝑇 : 𝐷 ⟶ 𝐸 )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑇 : 𝐷 ⟶ 𝐸 )
18		fco	⊢ ( ( 𝑓 : 𝐸 ⟶ 𝑅 ∧ 𝑇 : 𝐷 ⟶ 𝐸 ) → ( 𝑓 ∘ 𝑇 ) : 𝐷 ⟶ 𝑅 )
19	14 17 18	syl2anc	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → ( 𝑓 ∘ 𝑇 ) : 𝐷 ⟶ 𝑅 )
20		elmapg	⊢ ( ( 𝑅 ∈ 𝑋 ∧ 𝐷 ∈ 𝑉 ) → ( ( 𝑓 ∘ 𝑇 ) ∈ ( 𝑅 ↑_m 𝐷 ) ↔ ( 𝑓 ∘ 𝑇 ) : 𝐷 ⟶ 𝑅 ) )
21	20	biimpar	⊢ ( ( ( 𝑅 ∈ 𝑋 ∧ 𝐷 ∈ 𝑉 ) ∧ ( 𝑓 ∘ 𝑇 ) : 𝐷 ⟶ 𝑅 ) → ( 𝑓 ∘ 𝑇 ) ∈ ( 𝑅 ↑_m 𝐷 ) )
22	9 10 19 21	syl21anc	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → ( 𝑓 ∘ 𝑇 ) ∈ ( 𝑅 ↑_m 𝐷 ) )
23	22 2	eleqtrrdi	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → ( 𝑓 ∘ 𝑇 ) ∈ 𝐵 )
24	6	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) → 𝑅 ∈ 𝑋 )
25	5	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) → 𝐸 ∈ 𝑊 )
26		simpr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) → 𝑔 ∈ 𝐵 )
27	26 2	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) → 𝑔 ∈ ( 𝑅 ↑_m 𝐷 ) )
28		elmapi	⊢ ( 𝑔 ∈ ( 𝑅 ↑_m 𝐷 ) → 𝑔 : 𝐷 ⟶ 𝑅 )
29	27 28	syl	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) → 𝑔 : 𝐷 ⟶ 𝑅 )
30		f1ocnv	⊢ ( 𝑇 : 𝐷 –1-1-onto→ 𝐸 → ^◡ 𝑇 : 𝐸 –1-1-onto→ 𝐷 )
31		f1of	⊢ ( ^◡ 𝑇 : 𝐸 –1-1-onto→ 𝐷 → ^◡ 𝑇 : 𝐸 ⟶ 𝐷 )
32	7 30 31	3syl	⊢ ( 𝜑 → ^◡ 𝑇 : 𝐸 ⟶ 𝐷 )
33	32	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) → ^◡ 𝑇 : 𝐸 ⟶ 𝐷 )
34		fco	⊢ ( ( 𝑔 : 𝐷 ⟶ 𝑅 ∧ ^◡ 𝑇 : 𝐸 ⟶ 𝐷 ) → ( 𝑔 ∘ ^◡ 𝑇 ) : 𝐸 ⟶ 𝑅 )
35	29 33 34	syl2anc	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) → ( 𝑔 ∘ ^◡ 𝑇 ) : 𝐸 ⟶ 𝑅 )
36		elmapg	⊢ ( ( 𝑅 ∈ 𝑋 ∧ 𝐸 ∈ 𝑊 ) → ( ( 𝑔 ∘ ^◡ 𝑇 ) ∈ ( 𝑅 ↑_m 𝐸 ) ↔ ( 𝑔 ∘ ^◡ 𝑇 ) : 𝐸 ⟶ 𝑅 ) )
37	36	biimpar	⊢ ( ( ( 𝑅 ∈ 𝑋 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝑔 ∘ ^◡ 𝑇 ) : 𝐸 ⟶ 𝑅 ) → ( 𝑔 ∘ ^◡ 𝑇 ) ∈ ( 𝑅 ↑_m 𝐸 ) )
38	24 25 35 37	syl21anc	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) → ( 𝑔 ∘ ^◡ 𝑇 ) ∈ ( 𝑅 ↑_m 𝐸 ) )
39	38 1	eleqtrrdi	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) → ( 𝑔 ∘ ^◡ 𝑇 ) ∈ 𝐴 )
40		coass	⊢ ( ( 𝑔 ∘ ^◡ 𝑇 ) ∘ 𝑇 ) = ( 𝑔 ∘ ( ^◡ 𝑇 ∘ 𝑇 ) )
41	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → 𝑇 : 𝐷 –1-1-onto→ 𝐸 )
42		f1ococnv1	⊢ ( 𝑇 : 𝐷 –1-1-onto→ 𝐸 → ( ^◡ 𝑇 ∘ 𝑇 ) = ( I ↾ 𝐷 ) )
43	42	coeq2d	⊢ ( 𝑇 : 𝐷 –1-1-onto→ 𝐸 → ( 𝑔 ∘ ( ^◡ 𝑇 ∘ 𝑇 ) ) = ( 𝑔 ∘ ( I ↾ 𝐷 ) ) )
44	41 43	syl	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝑔 ∘ ( ^◡ 𝑇 ∘ 𝑇 ) ) = ( 𝑔 ∘ ( I ↾ 𝐷 ) ) )
45	29	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → 𝑔 : 𝐷 ⟶ 𝑅 )
46		fcoi1	⊢ ( 𝑔 : 𝐷 ⟶ 𝑅 → ( 𝑔 ∘ ( I ↾ 𝐷 ) ) = 𝑔 )
47	45 46	syl	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝑔 ∘ ( I ↾ 𝐷 ) ) = 𝑔 )
48	44 47	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝑔 ∘ ( ^◡ 𝑇 ∘ 𝑇 ) ) = 𝑔 )
49	40 48	eqtr2id	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → 𝑔 = ( ( 𝑔 ∘ ^◡ 𝑇 ) ∘ 𝑇 ) )
50	49	eqeq1d	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝑔 = ( 𝑓 ∘ 𝑇 ) ↔ ( ( 𝑔 ∘ ^◡ 𝑇 ) ∘ 𝑇 ) = ( 𝑓 ∘ 𝑇 ) ) )
51		eqcom	⊢ ( ( ( 𝑔 ∘ ^◡ 𝑇 ) ∘ 𝑇 ) = ( 𝑓 ∘ 𝑇 ) ↔ ( 𝑓 ∘ 𝑇 ) = ( ( 𝑔 ∘ ^◡ 𝑇 ) ∘ 𝑇 ) )
52	51	a1i	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ( ( ( 𝑔 ∘ ^◡ 𝑇 ) ∘ 𝑇 ) = ( 𝑓 ∘ 𝑇 ) ↔ ( 𝑓 ∘ 𝑇 ) = ( ( 𝑔 ∘ ^◡ 𝑇 ) ∘ 𝑇 ) ) )
53		f1ofo	⊢ ( 𝑇 : 𝐷 –1-1-onto→ 𝐸 → 𝑇 : 𝐷 –onto→ 𝐸 )
54	41 53	syl	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → 𝑇 : 𝐷 –onto→ 𝐸 )
55		simplr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → 𝑓 ∈ 𝐴 )
56	55 1	eleqtrdi	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → 𝑓 ∈ ( 𝑅 ↑_m 𝐸 ) )
57		elmapfn	⊢ ( 𝑓 ∈ ( 𝑅 ↑_m 𝐸 ) → 𝑓 Fn 𝐸 )
58	56 57	syl	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → 𝑓 Fn 𝐸 )
59		elmapfn	⊢ ( ( 𝑔 ∘ ^◡ 𝑇 ) ∈ ( 𝑅 ↑_m 𝐸 ) → ( 𝑔 ∘ ^◡ 𝑇 ) Fn 𝐸 )
60	38 59	syl	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) → ( 𝑔 ∘ ^◡ 𝑇 ) Fn 𝐸 )
61	60	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝑔 ∘ ^◡ 𝑇 ) Fn 𝐸 )
62		cocan2	⊢ ( ( 𝑇 : 𝐷 –onto→ 𝐸 ∧ 𝑓 Fn 𝐸 ∧ ( 𝑔 ∘ ^◡ 𝑇 ) Fn 𝐸 ) → ( ( 𝑓 ∘ 𝑇 ) = ( ( 𝑔 ∘ ^◡ 𝑇 ) ∘ 𝑇 ) ↔ 𝑓 = ( 𝑔 ∘ ^◡ 𝑇 ) ) )
63	54 58 61 62	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ( ( 𝑓 ∘ 𝑇 ) = ( ( 𝑔 ∘ ^◡ 𝑇 ) ∘ 𝑇 ) ↔ 𝑓 = ( 𝑔 ∘ ^◡ 𝑇 ) ) )
64	50 52 63	3bitrrd	⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ( 𝑓 = ( 𝑔 ∘ ^◡ 𝑇 ) ↔ 𝑔 = ( 𝑓 ∘ 𝑇 ) ) )
65	64	anasss	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐵 ) ) → ( 𝑓 = ( 𝑔 ∘ ^◡ 𝑇 ) ↔ 𝑔 = ( 𝑓 ∘ 𝑇 ) ) )
66	8 23 39 65	f1o3d	⊢ ( 𝜑 → ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ ^◡ 𝐹 = ( 𝑔 ∈ 𝐵 ↦ ( 𝑔 ∘ ^◡ 𝑇 ) ) ) )
67	66	simpld	⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )

Metamath Proof Explorer

Theorem fmptco1f1o

Proof