This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 RngIso 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 RngIso Y ) /\ ( ( X ( Inv ` C ) Y ) ` F ) = `' F ) ) )
16 simpl 
 |-  ( ( F e. ( X RngIso Y ) /\ ( ( X ( Inv ` C ) Y ) ` F ) = `' F ) -> F e. ( X RngIso Y ) )
17 15 16 biimtrdi 
 |-  ( ph -> ( F ( X ( Inv ` C ) Y ) ( ( X ( Inv ` C ) Y ) ` F ) -> F e. ( X RngIso Y ) ) )
18 14 17 sylbid 
 |-  ( ph -> ( F e. dom ( X ( Inv ` C ) Y ) -> F e. ( X RngIso Y ) ) )
19 eqid 
 |-  `' F = `' F
20 1 2 3 4 5 7 rngcinv 
 |-  ( ph -> ( F ( X ( Inv ` C ) Y ) `' F <-> ( F e. ( X RngIso 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 RngIso Y ) /\ `' F = `' F ) -> F e. dom ( X ( Inv ` C ) Y ) ) )
27 19 26 mpan2i 
 |-  ( ph -> ( F e. ( X RngIso Y ) -> F e. dom ( X ( Inv ` C ) Y ) ) )
28 18 27 impbid 
 |-  ( ph -> ( F e. dom ( X ( Inv ` C ) Y ) <-> F e. ( X RngIso Y ) ) )
29 11 28 bitrd 
 |-  ( ph -> ( F e. ( X I Y ) <-> F e. ( X RngIso Y ) ) )