Metamath Proof Explorer

Theorem funcinv

Description: The image of an inverse under a functor is an inverse. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses funcinv.b 
|- B = ( Base ` D )
funcinv.s 
|- I = ( Inv ` D )
funcinv.t 
|- J = ( Inv ` E )
funcinv.f 
|- ( ph -> F ( D Func E ) G )
funcinv.x 
|- ( ph -> X e. B )
funcinv.y 
|- ( ph -> Y e. B )
funcinv.m 
|- ( ph -> M ( X I Y ) N )
Assertion funcinv 
|- ( ph -> ( ( X G Y ) ` M ) ( ( F ` X ) J ( F ` Y ) ) ( ( Y G X ) ` N ) )

Proof

Step Hyp Ref Expression
1 funcinv.b 
 |-  B = ( Base ` D )
2 funcinv.s 
 |-  I = ( Inv ` D )
3 funcinv.t 
 |-  J = ( Inv ` E )
4 funcinv.f 
 |-  ( ph -> F ( D Func E ) G )
5 funcinv.x 
 |-  ( ph -> X e. B )
6 funcinv.y 
 |-  ( ph -> Y e. B )
7 funcinv.m 
 |-  ( ph -> M ( X I Y ) N )
8 eqid 
 |-  ( Sect ` D ) = ( Sect ` D )
9 eqid 
 |-  ( Sect ` E ) = ( Sect ` 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 simpld 
 |-  ( ph -> D e. Cat )
15 1 2 14 5 6 8 isinv 
 |-  ( ph -> ( M ( X I Y ) N <-> ( M ( X ( Sect ` D ) Y ) N /\ N ( Y ( Sect ` D ) X ) M ) ) )
16 7 15 mpbid 
 |-  ( ph -> ( M ( X ( Sect ` D ) Y ) N /\ N ( Y ( Sect ` D ) X ) M ) )
17 16 simpld 
 |-  ( ph -> M ( X ( Sect ` D ) Y ) N )
18 1 8 9 4 5 6 17 funcsect 
 |-  ( ph -> ( ( X G Y ) ` M ) ( ( F ` X ) ( Sect ` E ) ( F ` Y ) ) ( ( Y G X ) ` N ) )
19 16 simprd 
 |-  ( ph -> N ( Y ( Sect ` D ) X ) M )
20 1 8 9 4 6 5 19 funcsect 
 |-  ( ph -> ( ( Y G X ) ` N ) ( ( F ` Y ) ( Sect ` E ) ( F ` X ) ) ( ( X G Y ) ` M ) )
21 eqid 
 |-  ( Base ` E ) = ( Base ` E )
22 13 simprd 
 |-  ( ph -> E e. Cat )
23 1 21 4 funcf1 
 |-  ( ph -> F : B --> ( Base ` E ) )
24 23 5 ffvelrnd 
 |-  ( ph -> ( F ` X ) e. ( Base ` E ) )
25 23 6 ffvelrnd 
 |-  ( ph -> ( F ` Y ) e. ( Base ` E ) )
26 21 3 22 24 25 9 isinv 
 |-  ( ph -> ( ( ( X G Y ) ` M ) ( ( F ` X ) J ( F ` Y ) ) ( ( Y G X ) ` N ) <-> ( ( ( X G Y ) ` M ) ( ( F ` X ) ( Sect ` E ) ( F ` Y ) ) ( ( Y G X ) ` N ) /\ ( ( Y G X ) ` N ) ( ( F ` Y ) ( Sect ` E ) ( F ` X ) ) ( ( X G Y ) ` M ) ) ) )
27 18 20 26 mpbir2and 
 |-  ( ph -> ( ( X G Y ) ` M ) ( ( F ` X ) J ( F ` Y ) ) ( ( Y G X ) ` N ) )