This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem inviso1

Description: If G is an inverse to F , then F is an isomorphism. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses invfval.b ⊢ B = Base C
invfval.n ⊢ N = Inv ⁡ C
invfval.c ⊢ φ → C ∈ Cat
invss.x ⊢ φ → X ∈ B
invss.y ⊢ φ → Y ∈ B
isoval.n ⊢ I = Iso ⁡ C
inviso1.1 ⊢ φ → F X N Y G
Assertion inviso1 ⊢ φ → F ∈ X I Y

Proof

Step Hyp Ref Expression
1 invfval.b ⊢ B = Base C
2 invfval.n ⊢ N = Inv ⁡ C
3 invfval.c ⊢ φ → C ∈ Cat
4 invss.x ⊢ φ → X ∈ B
5 invss.y ⊢ φ → Y ∈ B
6 isoval.n ⊢ I = Iso ⁡ C
7 inviso1.1 ⊢ φ → F X N Y G
8 1 2 3 4 5 invfun ⊢ φ → Fun ⁡ X N Y
9 funrel ⊢ Fun ⁡ X N Y → Rel ⁡ X N Y
10 8 9 syl ⊢ φ → Rel ⁡ X N Y
11 releldm ⊢ Rel ⁡ X N Y ∧ F X N Y G → F ∈ dom ⁡ X N Y
12 10 7 11 syl2anc ⊢ φ → F ∈ dom ⁡ X N Y
13 1 2 3 4 5 6 isoval ⊢ φ → X I Y = dom ⁡ X N Y
14 12 13 eleqtrrd ⊢ φ → F ∈ X I Y