Metamath Proof Explorer

Theorem rngcisoALTV

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

Ref Expression
Hypotheses rngcsectALTV.c 
|- C = ( RngCatALTV ` U )
rngcsectALTV.b 
|- B = ( Base ` C )
rngcsectALTV.u 
|- ( ph -> U e. V )
rngcsectALTV.x 
|- ( ph -> X e. B )
rngcsectALTV.y 
|- ( ph -> Y e. B )
rngcisoALTV.n 
|- I = ( Iso ` C )
Assertion rngcisoALTV 
|- ( ph -> ( F e. ( X I Y ) <-> F e. ( X RngIso Y ) ) )

Proof

Step Hyp Ref Expression
1 rngcsectALTV.c 
 |-  C = ( RngCatALTV ` U )
2 rngcsectALTV.b 
 |-  B = ( Base ` C )
3 rngcsectALTV.u 
 |-  ( ph -> U e. V )
4 rngcsectALTV.x 
 |-  ( ph -> X e. B )
5 rngcsectALTV.y 
 |-  ( ph -> Y e. B )
6 rngcisoALTV.n 
 |-  I = ( Iso ` C )
7 eqid 
 |-  ( Inv ` C ) = ( Inv ` C )
8 1 rngccatALTV 
 |-  ( 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 rngcinvALTV 
 |-  ( 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 rngcinvALTV 
 |-  ( 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 ) ) )