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	|- ( ph -> F ( D Func E ) G )
	funciso.x	|- ( ph -> X e. B )
	funciso.y	|- ( ph -> Y e. B )
	funciso.m	|- ( ph -> M e. ( X I Y ) )
Assertion	funciso	|- ( ph -> ( ( X G Y ) ` M ) e. ( ( 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	|- ( ph -> F ( D Func E ) G )
5		funciso.x	|- ( ph -> X e. B )
6		funciso.y	|- ( ph -> Y e. B )
7		funciso.m	|- ( ph -> M e. ( 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 >. e. ( D Func E ) )
11	4 10	sylib	|- ( ph -> <. F , G >. e. ( D Func E ) )
12		funcrcl	|- ( <. F , G >. e. ( D Func E ) -> ( D e. Cat /\ E e. Cat ) )
13	11 12	syl	|- ( ph -> ( D e. Cat /\ E e. Cat ) )
14	13	simprd	|- ( ph -> E e. Cat )
15	1 8 4	funcf1	|- ( ph -> F : B --> ( Base ` E ) )
16	15 5	ffvelrnd	|- ( ph -> ( F ` X ) e. ( Base ` E ) )
17	15 6	ffvelrnd	|- ( ph -> ( F ` Y ) e. ( Base ` E ) )
18		eqid	|- ( Inv ` D ) = ( Inv ` D )
19	13	simpld	|- ( ph -> D e. Cat )
20	1 2 18 19 5 6 7	invisoinvr	|- ( ph -> M ( X ( Inv ` D ) Y ) ( ( X ( Inv ` D ) Y ) ` M ) )
21	1 18 9 4 5 6 20	funcinv	|- ( ph -> ( ( 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	|- ( ph -> ( ( X G Y ) ` M ) e. ( ( F ` X ) J ( F ` Y ) ) )