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 ⊢ φ → U ∈ V
ringcsect.x ⊢ φ → X ∈ B
ringcsect.y ⊢ φ → Y ∈ B
ringciso.n ⊢ I = Iso ⁡ C
Assertion ringciso ⊢ φ → F ∈ X I Y ↔ F ∈ X RingIso Y

Proof

Step Hyp Ref Expression
1 ringcsect.c ⊢ C = RingCat ⁡ U
2 ringcsect.b ⊢ B = Base C
3 ringcsect.u ⊢ φ → U ∈ V
4 ringcsect.x ⊢ φ → X ∈ B
5 ringcsect.y ⊢ φ → Y ∈ B
6 ringciso.n ⊢ I = Iso ⁡ C
7 eqid ⊢ Inv ⁡ C = Inv ⁡ C
8 1 ringccat ⊢ U ∈ V → C ∈ Cat
9 3 8 syl ⊢ φ → C ∈ Cat
10 2 7 9 4 5 6 isoval ⊢ φ → X I Y = dom ⁡ X Inv ⁡ C Y
11 10 eleq2d ⊢ φ → F ∈ X I Y ↔ F ∈ dom ⁡ X Inv ⁡ C Y
12 2 7 9 4 5 invfun ⊢ φ → Fun ⁡ X Inv ⁡ C Y
13 funfvbrb ⊢ Fun ⁡ X Inv ⁡ C Y → F ∈ dom ⁡ X Inv ⁡ C Y ↔ F X Inv ⁡ C Y X Inv ⁡ C Y ⁡ F
14 12 13 syl ⊢ φ → F ∈ dom ⁡ X Inv ⁡ C Y ↔ F X Inv ⁡ C Y X Inv ⁡ C Y ⁡ F
15 1 2 3 4 5 7 ringcinv ⊢ φ → F X Inv ⁡ C Y X Inv ⁡ C Y ⁡ F ↔ F ∈ X RingIso Y ∧ X Inv ⁡ C Y ⁡ F = F -1
16 simpl ⊢ F ∈ X RingIso Y ∧ X Inv ⁡ C Y ⁡ F = F -1 → F ∈ X RingIso Y
17 15 16 syl6bi ⊢ φ → F X Inv ⁡ C Y X Inv ⁡ C Y ⁡ F → F ∈ X RingIso Y
18 14 17 sylbid ⊢ φ → F ∈ dom ⁡ X Inv ⁡ C Y → F ∈ X RingIso Y
19 eqid ⊢ F -1 = F -1
20 1 2 3 4 5 7 ringcinv ⊢ φ → F X Inv ⁡ C Y F -1 ↔ F ∈ X RingIso Y ∧ F -1 = F -1
21 funrel ⊢ Fun ⁡ X Inv ⁡ C Y → Rel ⁡ X Inv ⁡ C Y
22 12 21 syl ⊢ φ → Rel ⁡ X Inv ⁡ C Y
23 releldm ⊢ Rel ⁡ X Inv ⁡ C Y ∧ F X Inv ⁡ C Y F -1 → F ∈ dom ⁡ X Inv ⁡ C Y
24 23 ex ⊢ Rel ⁡ X Inv ⁡ C Y → F X Inv ⁡ C Y F -1 → F ∈ dom ⁡ X Inv ⁡ C Y
25 22 24 syl ⊢ φ → F X Inv ⁡ C Y F -1 → F ∈ dom ⁡ X Inv ⁡ C Y
26 20 25 sylbird ⊢ φ → F ∈ X RingIso Y ∧ F -1 = F -1 → F ∈ dom ⁡ X Inv ⁡ C Y
27 19 26 mpan2i ⊢ φ → F ∈ X RingIso Y → F ∈ dom ⁡ X Inv ⁡ C Y
28 18 27 impbid ⊢ φ → F ∈ dom ⁡ X Inv ⁡ C Y ↔ F ∈ X RingIso Y
29 11 28 bitrd ⊢ φ → F ∈ X I Y ↔ F ∈ X RingIso Y