Metamath Proof Explorer


Theorem invf1o

Description: The inverse relation is a bijection from isomorphisms to isomorphisms. This means that every isomorphism F e. ( X I Y ) has a unique inverse, denoted by ( ( InvC )F ) . Remark 3.12 of Adamek p. 28. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses invfval.b B = Base C
invfval.n N = Inv C
invfval.c φ C Cat
invfval.x φ X B
invfval.y φ Y B
isoval.n I = Iso C
Assertion invf1o φ X N Y : X I Y 1-1 onto Y I X

Proof

Step Hyp Ref Expression
1 invfval.b B = Base C
2 invfval.n N = Inv C
3 invfval.c φ C Cat
4 invfval.x φ X B
5 invfval.y φ Y B
6 isoval.n I = Iso C
7 1 2 3 4 5 6 invf φ X N Y : X I Y Y I X
8 7 ffnd φ X N Y Fn X I Y
9 1 2 3 5 4 6 invf φ Y N X : Y I X X I Y
10 9 ffnd φ Y N X Fn Y I X
11 1 2 3 4 5 invsym2 φ X N Y -1 = Y N X
12 11 fneq1d φ X N Y -1 Fn Y I X Y N X Fn Y I X
13 10 12 mpbird φ X N Y -1 Fn Y I X
14 dff1o4 X N Y : X I Y 1-1 onto Y I X X N Y Fn X I Y X N Y -1 Fn Y I X
15 8 13 14 sylanbrc φ X N Y : X I Y 1-1 onto Y I X