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	$⊢ φ \to F (D Func E) G$
	funciso.x	$⊢ φ \to X \in B$
	funciso.y	$⊢ φ \to Y \in B$
	funciso.m	$⊢ φ \to M \in (X I Y)$
Assertion	funciso	$⊢ φ \to (X G Y) (M) \in (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	$⊢ φ \to F (D Func E) G$
5		funciso.x	$⊢ φ \to X \in B$
6		funciso.y	$⊢ φ \to Y \in B$
7		funciso.m	$⊢ φ \to M \in (X I Y)$
8		eqid	$⊢ {Base}_{E} = {Base}_{E}$
9		eqid	$⊢ Inv (E) = Inv (E)$
10		df-br	$⊢ F (D Func E) G \leftrightarrow ⟨F, G⟩ \in (D Func E)$
11	4 10	sylib	$⊢ φ \to ⟨F, G⟩ \in (D Func E)$
12		funcrcl	$⊢ ⟨F, G⟩ \in (D Func E) \to (D \in Cat \land E \in Cat)$
13	11 12	syl	$⊢ φ \to (D \in Cat \land E \in Cat)$
14	13	simprd	$⊢ φ \to E \in Cat$
15	1 8 4	funcf1	$⊢ φ \to F : B ⟶ {Base}_{E}$
16	15 5	ffvelrnd	$⊢ φ \to F (X) \in {Base}_{E}$
17	15 6	ffvelrnd	$⊢ φ \to F (Y) \in {Base}_{E}$
18		eqid	$⊢ Inv (D) = Inv (D)$
19	13	simpld	$⊢ φ \to D \in Cat$
20	1 2 18 19 5 6 7	invisoinvr	$⊢ φ \to M (X Inv (D) Y) (X Inv (D) Y) (M)$
21	1 18 9 4 5 6 20	funcinv	$⊢ φ \to (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	$⊢ φ \to (X G Y) (M) \in (F (X) J F (Y))$

Metamath Proof Explorer

Theorem funciso

Proof