Metamath Proof Explorer

Theorem rngciso

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

Ref Expression
Hypotheses rngcsect.c ⊢ C = RngCat ⁡ U
rngcsect.b ⊢ B = Base C
rngcsect.u ⊢ φ → U ∈ V
rngcsect.x ⊢ φ → X ∈ B
rngcsect.y ⊢ φ → Y ∈ B
rngciso.n ⊢ I = Iso ⁡ C
Assertion rngciso ⊢ φ → F ∈ X I Y ↔ F ∈ X RngIsom Y

Proof

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