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

Proof

Step Hyp Ref Expression
1 rngcsectALTV.c ⊢ C = RngCatALTV ⁡ U
2 rngcsectALTV.b ⊢ B = Base C
3 rngcsectALTV.u ⊢ φ → U ∈ V
4 rngcsectALTV.x ⊢ φ → X ∈ B
5 rngcsectALTV.y ⊢ φ → Y ∈ B
6 rngcisoALTV.n ⊢ I = Iso ⁡ C
7 eqid ⊢ Inv ⁡ C = Inv ⁡ C
8 1 rngccatALTV ⊢ 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 rngcinvALTV ⊢ φ → F X Inv ⁡ C Y X Inv ⁡ C Y ⁡ F ↔ F ∈ X RngIsom Y ∧ X Inv ⁡ C Y ⁡ F = F -1
16 simpl ⊢ F ∈ X RngIsom Y ∧ X Inv ⁡ C Y ⁡ F = F -1 → F ∈ X RngIsom Y
17 15 16 syl6bi ⊢ φ → F X Inv ⁡ C Y X Inv ⁡ C Y ⁡ F → F ∈ X RngIsom Y
18 14 17 sylbid ⊢ φ → F ∈ dom ⁡ X Inv ⁡ C Y → F ∈ X RngIsom Y
19 eqid ⊢ F -1 = F -1
20 1 2 3 4 5 7 rngcinvALTV ⊢ φ → F X Inv ⁡ C Y F -1 ↔ F ∈ X RngIsom 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 RngIsom Y ∧ F -1 = F -1 → F ∈ dom ⁡ X Inv ⁡ C Y
27 19 26 mpan2i ⊢ φ → F ∈ X RngIsom Y → F ∈ dom ⁡ X Inv ⁡ C Y
28 18 27 impbid ⊢ φ → F ∈ dom ⁡ X Inv ⁡ C Y ↔ F ∈ X RngIsom Y
29 11 28 bitrd ⊢ φ → F ∈ X I Y ↔ F ∈ X RngIsom Y