Metamath Proof Explorer

Theorem fthinv

Description: A faithful functor reflects inverses. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Hypotheses fthsect.b 
|- B = ( Base ` C )
fthsect.h 
|- H = ( Hom ` C )
fthsect.f 
|- ( ph -> F ( C Faith D ) G )
fthsect.x 
|- ( ph -> X e. B )
fthsect.y 
|- ( ph -> Y e. B )
fthsect.m 
|- ( ph -> M e. ( X H Y ) )
fthsect.n 
|- ( ph -> N e. ( Y H X ) )
fthinv.s 
|- I = ( Inv ` C )
fthinv.t 
|- J = ( Inv ` D )
Assertion fthinv 
|- ( ph -> ( M ( X I Y ) N <-> ( ( X G Y ) ` M ) ( ( F ` X ) J ( F ` Y ) ) ( ( Y G X ) ` N ) ) )

Proof

Step Hyp Ref Expression
1 fthsect.b 
 |-  B = ( Base ` C )
2 fthsect.h 
 |-  H = ( Hom ` C )
3 fthsect.f 
 |-  ( ph -> F ( C Faith D ) G )
4 fthsect.x 
 |-  ( ph -> X e. B )
5 fthsect.y 
 |-  ( ph -> Y e. B )
6 fthsect.m 
 |-  ( ph -> M e. ( X H Y ) )
7 fthsect.n 
 |-  ( ph -> N e. ( Y H X ) )
8 fthinv.s 
 |-  I = ( Inv ` C )
9 fthinv.t 
 |-  J = ( Inv ` D )
10 eqid 
 |-  ( Sect ` C ) = ( Sect ` C )
11 eqid 
 |-  ( Sect ` D ) = ( Sect ` D )
12 1 2 3 4 5 6 7 10 11 fthsect 
 |-  ( ph -> ( M ( X ( Sect ` C ) Y ) N <-> ( ( X G Y ) ` M ) ( ( F ` X ) ( Sect ` D ) ( F ` Y ) ) ( ( Y G X ) ` N ) ) )
13 1 2 3 5 4 7 6 10 11 fthsect 
 |-  ( ph -> ( N ( Y ( Sect ` C ) X ) M <-> ( ( Y G X ) ` N ) ( ( F ` Y ) ( Sect ` D ) ( F ` X ) ) ( ( X G Y ) ` M ) ) )
14 12 13 anbi12d 
 |-  ( ph -> ( ( M ( X ( Sect ` C ) Y ) N /\ N ( Y ( Sect ` C ) X ) M ) <-> ( ( ( X G Y ) ` M ) ( ( F ` X ) ( Sect ` D ) ( F ` Y ) ) ( ( Y G X ) ` N ) /\ ( ( Y G X ) ` N ) ( ( F ` Y ) ( Sect ` D ) ( F ` X ) ) ( ( X G Y ) ` M ) ) ) )
15 fthfunc 
 |-  ( C Faith D ) C_ ( C Func D )
16 15 ssbri 
 |-  ( F ( C Faith D ) G -> F ( C Func D ) G )
17 3 16 syl 
 |-  ( ph -> F ( C Func D ) G )
18 df-br 
 |-  ( F ( C Func D ) G <-> <. F , G >. e. ( C Func D ) )
19 17 18 sylib 
 |-  ( ph -> <. F , G >. e. ( C Func D ) )
20 funcrcl 
 |-  ( <. F , G >. e. ( C Func D ) -> ( C e. Cat /\ D e. Cat ) )
21 19 20 syl 
 |-  ( ph -> ( C e. Cat /\ D e. Cat ) )
22 21 simpld 
 |-  ( ph -> C e. Cat )
23 1 8 22 4 5 10 isinv 
 |-  ( ph -> ( M ( X I Y ) N <-> ( M ( X ( Sect ` C ) Y ) N /\ N ( Y ( Sect ` C ) X ) M ) ) )
24 eqid 
 |-  ( Base ` D ) = ( Base ` D )
25 21 simprd 
 |-  ( ph -> D e. Cat )
26 1 24 17 funcf1 
 |-  ( ph -> F : B --> ( Base ` D ) )
27 26 4 ffvelrnd 
 |-  ( ph -> ( F ` X ) e. ( Base ` D ) )
28 26 5 ffvelrnd 
 |-  ( ph -> ( F ` Y ) e. ( Base ` D ) )
29 24 9 25 27 28 11 isinv 
 |-  ( ph -> ( ( ( X G Y ) ` M ) ( ( F ` X ) J ( F ` Y ) ) ( ( Y G X ) ` N ) <-> ( ( ( X G Y ) ` M ) ( ( F ` X ) ( Sect ` D ) ( F ` Y ) ) ( ( Y G X ) ` N ) /\ ( ( Y G X ) ` N ) ( ( F ` Y ) ( Sect ` D ) ( F ` X ) ) ( ( X G Y ) ` M ) ) ) )
30 14 23 29 3bitr4d 
 |-  ( ph -> ( M ( X I Y ) N <-> ( ( X G Y ) ` M ) ( ( F ` X ) J ( F ` Y ) ) ( ( Y G X ) ` N ) ) )