Metamath Proof Explorer

Theorem ringciso

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

Ref Expression
Hypotheses ringcsect.c 
|- C = ( RingCat ` U )
ringcsect.b 
|- B = ( Base ` C )
ringcsect.u 
|- ( ph -> U e. V )
ringcsect.x 
|- ( ph -> X e. B )
ringcsect.y 
|- ( ph -> Y e. B )
ringciso.n 
|- I = ( Iso ` C )
Assertion ringciso 
|- ( ph -> ( F e. ( X I Y ) <-> F e. ( X RingIso Y ) ) )

Proof

Step Hyp Ref Expression
1 ringcsect.c 
 |-  C = ( RingCat ` U )
2 ringcsect.b 
 |-  B = ( Base ` C )
3 ringcsect.u 
 |-  ( ph -> U e. V )
4 ringcsect.x 
 |-  ( ph -> X e. B )
5 ringcsect.y 
 |-  ( ph -> Y e. B )
6 ringciso.n 
 |-  I = ( Iso ` C )
7 eqid 
 |-  ( Inv ` C ) = ( Inv ` C )
8 1 ringccat 
 |-  ( 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 ringcinv 
 |-  ( ph -> ( F ( X ( Inv ` C ) Y ) ( ( X ( Inv ` C ) Y ) ` F ) <-> ( F e. ( X RingIso Y ) /\ ( ( X ( Inv ` C ) Y ) ` F ) = `' F ) ) )
16 simpl 
 |-  ( ( F e. ( X RingIso Y ) /\ ( ( X ( Inv ` C ) Y ) ` F ) = `' F ) -> F e. ( X RingIso Y ) )
17 15 16 syl6bi 
 |-  ( ph -> ( F ( X ( Inv ` C ) Y ) ( ( X ( Inv ` C ) Y ) ` F ) -> F e. ( X RingIso Y ) ) )
18 14 17 sylbid 
 |-  ( ph -> ( F e. dom ( X ( Inv ` C ) Y ) -> F e. ( X RingIso Y ) ) )
19 eqid 
 |-  `' F = `' F
20 1 2 3 4 5 7 ringcinv 
 |-  ( ph -> ( F ( X ( Inv ` C ) Y ) `' F <-> ( F e. ( X RingIso 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 RingIso Y ) /\ `' F = `' F ) -> F e. dom ( X ( Inv ` C ) Y ) ) )
27 19 26 mpan2i 
 |-  ( ph -> ( F e. ( X RingIso Y ) -> F e. dom ( X ( Inv ` C ) Y ) ) )
28 18 27 impbid 
 |-  ( ph -> ( F e. dom ( X ( Inv ` C ) Y ) <-> F e. ( X RingIso Y ) ) )
29 11 28 bitrd 
 |-  ( ph -> ( F e. ( X I Y ) <-> F e. ( X RingIso Y ) ) )