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

Proof

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