Metamath Proof Explorer


Theorem 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 A = R E
fmptco1f1o.b B = R D
fmptco1f1o.f F = f A f T
fmptco1f1o.d φ D V
fmptco1f1o.e φ E W
fmptco1f1o.r φ R X
fmptco1f1o.t φ T : D 1-1 onto E
Assertion fmptco1f1o φ F : A 1-1 onto B

Proof

Step Hyp Ref Expression
1 fmptco1f1o.a A = R E
2 fmptco1f1o.b B = R D
3 fmptco1f1o.f F = f A f T
4 fmptco1f1o.d φ D V
5 fmptco1f1o.e φ E W
6 fmptco1f1o.r φ R X
7 fmptco1f1o.t φ T : D 1-1 onto E
8 3 a1i φ F = f A f T
9 6 adantr φ f A R X
10 4 adantr φ f A D V
11 simpr φ f A f A
12 11 1 eleqtrdi φ f A f R E
13 elmapi f R E f : E R
14 12 13 syl φ f A f : E R
15 f1of T : D 1-1 onto E T : D E
16 7 15 syl φ T : D E
17 16 adantr φ f A T : D E
18 fco f : E R T : D E f T : D R
19 14 17 18 syl2anc φ f A f T : D R
20 elmapg R X D V f T R D f T : D R
21 20 biimpar R X D V f T : D R f T R D
22 9 10 19 21 syl21anc φ f A f T R D
23 22 2 eleqtrrdi φ f A f T B
24 6 adantr φ g B R X
25 5 adantr φ g B E W
26 simpr φ g B g B
27 26 2 eleqtrdi φ g B g R D
28 elmapi g R D g : D R
29 27 28 syl φ g B g : D R
30 f1ocnv T : D 1-1 onto E T -1 : E 1-1 onto D
31 f1of T -1 : E 1-1 onto D T -1 : E D
32 7 30 31 3syl φ T -1 : E D
33 32 adantr φ g B T -1 : E D
34 fco g : D R T -1 : E D g T -1 : E R
35 29 33 34 syl2anc φ g B g T -1 : E R
36 elmapg R X E W g T -1 R E g T -1 : E R
37 36 biimpar R X E W g T -1 : E R g T -1 R E
38 24 25 35 37 syl21anc φ g B g T -1 R E
39 38 1 eleqtrrdi φ g B g T -1 A
40 coass g T -1 T = g T -1 T
41 7 ad2antrr φ f A g B T : D 1-1 onto E
42 f1ococnv1 T : D 1-1 onto E T -1 T = I D
43 42 coeq2d T : D 1-1 onto E g T -1 T = g I D
44 41 43 syl φ f A g B g T -1 T = g I D
45 29 adantlr φ f A g B g : D R
46 fcoi1 g : D R g I D = g
47 45 46 syl φ f A g B g I D = g
48 44 47 eqtrd φ f A g B g T -1 T = g
49 40 48 eqtr2id φ f A g B g = g T -1 T
50 49 eqeq1d φ f A g B g = f T g T -1 T = f T
51 eqcom g T -1 T = f T f T = g T -1 T
52 51 a1i φ f A g B g T -1 T = f T f T = g T -1 T
53 f1ofo T : D 1-1 onto E T : D onto E
54 41 53 syl φ f A g B T : D onto E
55 simplr φ f A g B f A
56 55 1 eleqtrdi φ f A g B f R E
57 elmapfn f R E f Fn E
58 56 57 syl φ f A g B f Fn E
59 elmapfn g T -1 R E g T -1 Fn E
60 38 59 syl φ g B g T -1 Fn E
61 60 adantlr φ f A g B g T -1 Fn E
62 cocan2 T : D onto E f Fn E g T -1 Fn E f T = g T -1 T f = g T -1
63 54 58 61 62 syl3anc φ f A g B f T = g T -1 T f = g T -1
64 50 52 63 3bitrrd φ f A g B f = g T -1 g = f T
65 64 anasss φ f A g B f = g T -1 g = f T
66 8 23 39 65 f1o3d φ F : A 1-1 onto B F -1 = g B g T -1
67 66 simpld φ F : A 1-1 onto B