Metamath Proof Explorer

Theorem ringcisoALTV

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

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

Proof

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