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

Metamath Proof Explorer

Theorem funciso

Description: The image of an isomorphism under a functor is an isomorphism. Proposition 3.21 of Adamek p. 32. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses funciso.b ⊢ B = Base D
funciso.s ⊢ I = Iso ⁡ D
funciso.t ⊢ J = Iso ⁡ E
funciso.f ⊢ φ → F D Func E G
funciso.x ⊢ φ → X ∈ B
funciso.y ⊢ φ → Y ∈ B
funciso.m ⊢ φ → M ∈ X I Y
Assertion funciso ⊢ φ → X G Y ⁡ M ∈ F ⁡ X J F ⁡ Y

Proof

Step Hyp Ref Expression
1 funciso.b ⊢ B = Base D
2 funciso.s ⊢ I = Iso ⁡ D
3 funciso.t ⊢ J = Iso ⁡ E
4 funciso.f ⊢ φ → F D Func E G
5 funciso.x ⊢ φ → X ∈ B
6 funciso.y ⊢ φ → Y ∈ B
7 funciso.m ⊢ φ → M ∈ X I Y
8 eqid ⊢ Base E = Base E
9 eqid ⊢ Inv ⁡ E = Inv ⁡ E
10 df-br ⊢ F D Func E G ↔ F G ∈ D Func E
11 4 10 sylib ⊢ φ → F G ∈ D Func E
12 funcrcl ⊢ F G ∈ D Func E → D ∈ Cat ∧ E ∈ Cat
13 11 12 syl ⊢ φ → D ∈ Cat ∧ E ∈ Cat
14 13 simprd ⊢ φ → E ∈ Cat
15 1 8 4 funcf1 ⊢ φ → F : B ⟶ Base E
16 15 5 ffvelcdmd ⊢ φ → F ⁡ X ∈ Base E
17 15 6 ffvelcdmd ⊢ φ → F ⁡ Y ∈ Base E
18 eqid ⊢ Inv ⁡ D = Inv ⁡ D
19 13 simpld ⊢ φ → D ∈ Cat
20 1 2 18 19 5 6 7 invisoinvr ⊢ φ → M X Inv ⁡ D Y X Inv ⁡ D Y ⁡ M
21 1 18 9 4 5 6 20 funcinv ⊢ φ → X G Y ⁡ M F ⁡ X Inv ⁡ E F ⁡ Y Y G X ⁡ X Inv ⁡ D Y ⁡ M
22 8 9 14 16 17 3 21 inviso1 ⊢ φ → X G Y ⁡ M ∈ F ⁡ X J F ⁡ Y