Metamath Proof Explorer


Theorem rngciso

Description: An isomorphism in the category of non-unital rings is a bijection. (Contributed by AV, 28-Feb-2020)

Ref Expression
Hypotheses rngcsect.c
|- C = ( RngCat ` U )
rngcsect.b
|- B = ( Base ` C )
rngcsect.u
|- ( ph -> U e. V )
rngcsect.x
|- ( ph -> X e. B )
rngcsect.y
|- ( ph -> Y e. B )
rngciso.n
|- I = ( Iso ` C )
Assertion rngciso
|- ( ph -> ( F e. ( X I Y ) <-> F e. ( X RngIsom Y ) ) )

Proof

Step Hyp Ref Expression
1 rngcsect.c
 |-  C = ( RngCat ` U )
2 rngcsect.b
 |-  B = ( Base ` C )
3 rngcsect.u
 |-  ( ph -> U e. V )
4 rngcsect.x
 |-  ( ph -> X e. B )
5 rngcsect.y
 |-  ( ph -> Y e. B )
6 rngciso.n
 |-  I = ( Iso ` C )
7 eqid
 |-  ( Inv ` C ) = ( Inv ` C )
8 1 rngccat
 |-  ( U e. V -> C e. Cat )
9 3 8 syl
 |-  ( ph -> C e. Cat )
10 2 7 9 4 5 6 isoval
 |-  ( ph -> ( X I Y ) = dom ( X ( Inv ` C ) Y ) )
11 10 eleq2d
 |-  ( ph -> ( F e. ( X I Y ) <-> F e. dom ( X ( Inv ` C ) Y ) ) )
12 2 7 9 4 5 invfun
 |-  ( ph -> Fun ( X ( Inv ` C ) Y ) )
13 funfvbrb
 |-  ( Fun ( X ( Inv ` C ) Y ) -> ( F e. dom ( X ( Inv ` C ) Y ) <-> F ( X ( Inv ` C ) Y ) ( ( X ( Inv ` C ) Y ) ` F ) ) )
14 12 13 syl
 |-  ( ph -> ( F e. dom ( X ( Inv ` C ) Y ) <-> F ( X ( Inv ` C ) Y ) ( ( X ( Inv ` C ) Y ) ` F ) ) )
15 1 2 3 4 5 7 rngcinv
 |-  ( ph -> ( F ( X ( Inv ` C ) Y ) ( ( X ( Inv ` C ) Y ) ` F ) <-> ( F e. ( X RngIsom Y ) /\ ( ( X ( Inv ` C ) Y ) ` F ) = `' F ) ) )
16 simpl
 |-  ( ( F e. ( X RngIsom Y ) /\ ( ( X ( Inv ` C ) Y ) ` F ) = `' F ) -> F e. ( X RngIsom Y ) )
17 15 16 syl6bi
 |-  ( ph -> ( F ( X ( Inv ` C ) Y ) ( ( X ( Inv ` C ) Y ) ` F ) -> F e. ( X RngIsom Y ) ) )
18 14 17 sylbid
 |-  ( ph -> ( F e. dom ( X ( Inv ` C ) Y ) -> F e. ( X RngIsom Y ) ) )
19 eqid
 |-  `' F = `' F
20 1 2 3 4 5 7 rngcinv
 |-  ( ph -> ( F ( X ( Inv ` C ) Y ) `' F <-> ( F e. ( X RngIsom Y ) /\ `' F = `' F ) ) )
21 funrel
 |-  ( Fun ( X ( Inv ` C ) Y ) -> Rel ( X ( Inv ` C ) Y ) )
22 12 21 syl
 |-  ( ph -> Rel ( X ( Inv ` C ) Y ) )
23 releldm
 |-  ( ( Rel ( X ( Inv ` C ) Y ) /\ F ( X ( Inv ` C ) Y ) `' F ) -> F e. dom ( X ( Inv ` C ) Y ) )
24 23 ex
 |-  ( Rel ( X ( Inv ` C ) Y ) -> ( F ( X ( Inv ` C ) Y ) `' F -> F e. dom ( X ( Inv ` C ) Y ) ) )
25 22 24 syl
 |-  ( ph -> ( F ( X ( Inv ` C ) Y ) `' F -> F e. dom ( X ( Inv ` C ) Y ) ) )
26 20 25 sylbird
 |-  ( ph -> ( ( F e. ( X RngIsom Y ) /\ `' F = `' F ) -> F e. dom ( X ( Inv ` C ) Y ) ) )
27 19 26 mpan2i
 |-  ( ph -> ( F e. ( X RngIsom Y ) -> F e. dom ( X ( Inv ` C ) Y ) ) )
28 18 27 impbid
 |-  ( ph -> ( F e. dom ( X ( Inv ` C ) Y ) <-> F e. ( X RngIsom Y ) ) )
29 11 28 bitrd
 |-  ( ph -> ( F e. ( X I Y ) <-> F e. ( X RngIsom Y ) ) )