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 
|- ( 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 ffvelcdmd 
 |-  ( ph -> ( F ` X ) e. ( Base ` E ) )
17 15 6 ffvelcdmd 
 |-  ( 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 ) ) )