Metamath Proof Explorer

Theorem ffthiso

Description: A fully faithful functor reflects isomorphisms. Corollary 3.32 of Adamek p. 35. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Hypotheses fthmon.b 
|- B = ( Base ` C )
fthmon.h 
|- H = ( Hom ` C )
fthmon.f 
|- ( ph -> F ( C Faith D ) G )
fthmon.x 
|- ( ph -> X e. B )
fthmon.y 
|- ( ph -> Y e. B )
fthmon.r 
|- ( ph -> R e. ( X H Y ) )
ffthiso.f 
|- ( ph -> F ( C Full D ) G )
ffthiso.s 
|- I = ( Iso ` C )
ffthiso.t 
|- J = ( Iso ` D )
Assertion ffthiso 
|- ( ph -> ( R e. ( X I Y ) <-> ( ( X G Y ) ` R ) e. ( ( F ` X ) J ( F ` Y ) ) ) )

Proof

Step Hyp Ref Expression
1 fthmon.b 
 |-  B = ( Base ` C )
2 fthmon.h 
 |-  H = ( Hom ` C )
3 fthmon.f 
 |-  ( ph -> F ( C Faith D ) G )
4 fthmon.x 
 |-  ( ph -> X e. B )
5 fthmon.y 
 |-  ( ph -> Y e. B )
6 fthmon.r 
 |-  ( ph -> R e. ( X H Y ) )
7 ffthiso.f 
 |-  ( ph -> F ( C Full D ) G )
8 ffthiso.s 
 |-  I = ( Iso ` C )
9 ffthiso.t 
 |-  J = ( Iso ` D )
10 fthfunc 
 |-  ( C Faith D ) C_ ( C Func D )
11 10 ssbri 
 |-  ( F ( C Faith D ) G -> F ( C Func D ) G )
12 3 11 syl 
 |-  ( ph -> F ( C Func D ) G )
13 12 adantr 
 |-  ( ( ph /\ R e. ( X I Y ) ) -> F ( C Func D ) G )
14 4 adantr 
 |-  ( ( ph /\ R e. ( X I Y ) ) -> X e. B )
15 5 adantr 
 |-  ( ( ph /\ R e. ( X I Y ) ) -> Y e. B )
16 simpr 
 |-  ( ( ph /\ R e. ( X I Y ) ) -> R e. ( X I Y ) )
17 1 8 9 13 14 15 16 funciso 
 |-  ( ( ph /\ R e. ( X I Y ) ) -> ( ( X G Y ) ` R ) e. ( ( F ` X ) J ( F ` Y ) ) )
18 eqid 
 |-  ( Inv ` C ) = ( Inv ` C )
19 df-br 
 |-  ( F ( C Func D ) G <-> <. F , G >. e. ( C Func D ) )
20 12 19 sylib 
 |-  ( ph -> <. F , G >. e. ( C Func D ) )
21 funcrcl 
 |-  ( <. F , G >. e. ( C Func D ) -> ( C e. Cat /\ D e. Cat ) )
22 20 21 syl 
 |-  ( ph -> ( C e. Cat /\ D e. Cat ) )
23 22 simpld 
 |-  ( ph -> C e. Cat )
24 23 ad3antrrr 
 |-  ( ( ( ( ph /\ ( ( X G Y ) ` R ) e. ( ( F ` X ) J ( F ` Y ) ) ) /\ f e. ( Y H X ) ) /\ ( ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) ` ( ( X G Y ) ` R ) ) = ( ( Y G X ) ` f ) ) -> C e. Cat )
25 4 ad3antrrr 
 |-  ( ( ( ( ph /\ ( ( X G Y ) ` R ) e. ( ( F ` X ) J ( F ` Y ) ) ) /\ f e. ( Y H X ) ) /\ ( ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) ` ( ( X G Y ) ` R ) ) = ( ( Y G X ) ` f ) ) -> X e. B )
26 5 ad3antrrr 
 |-  ( ( ( ( ph /\ ( ( X G Y ) ` R ) e. ( ( F ` X ) J ( F ` Y ) ) ) /\ f e. ( Y H X ) ) /\ ( ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) ` ( ( X G Y ) ` R ) ) = ( ( Y G X ) ` f ) ) -> Y e. B )
27 eqid 
 |-  ( Base ` D ) = ( Base ` D )
28 eqid 
 |-  ( Inv ` D ) = ( Inv ` D )
29 22 simprd 
 |-  ( ph -> D e. Cat )
30 1 27 12 funcf1 
 |-  ( ph -> F : B --> ( Base ` D ) )
31 30 4 ffvelrnd 
 |-  ( ph -> ( F ` X ) e. ( Base ` D ) )
32 30 5 ffvelrnd 
 |-  ( ph -> ( F ` Y ) e. ( Base ` D ) )
33 27 28 29 31 32 9 isoval 
 |-  ( ph -> ( ( F ` X ) J ( F ` Y ) ) = dom ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) )
34 33 eleq2d 
 |-  ( ph -> ( ( ( X G Y ) ` R ) e. ( ( F ` X ) J ( F ` Y ) ) <-> ( ( X G Y ) ` R ) e. dom ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) ) )
35 34 biimpa 
 |-  ( ( ph /\ ( ( X G Y ) ` R ) e. ( ( F ` X ) J ( F ` Y ) ) ) -> ( ( X G Y ) ` R ) e. dom ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) )
36 27 28 29 31 32 invfun 
 |-  ( ph -> Fun ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) )
37 36 adantr 
 |-  ( ( ph /\ ( ( X G Y ) ` R ) e. ( ( F ` X ) J ( F ` Y ) ) ) -> Fun ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) )
38 funfvbrb 
 |-  ( Fun ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) -> ( ( ( X G Y ) ` R ) e. dom ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) <-> ( ( X G Y ) ` R ) ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) ( ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) ` ( ( X G Y ) ` R ) ) ) )
39 37 38 syl 
 |-  ( ( ph /\ ( ( X G Y ) ` R ) e. ( ( F ` X ) J ( F ` Y ) ) ) -> ( ( ( X G Y ) ` R ) e. dom ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) <-> ( ( X G Y ) ` R ) ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) ( ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) ` ( ( X G Y ) ` R ) ) ) )
40 35 39 mpbid 
 |-  ( ( ph /\ ( ( X G Y ) ` R ) e. ( ( F ` X ) J ( F ` Y ) ) ) -> ( ( X G Y ) ` R ) ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) ( ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) ` ( ( X G Y ) ` R ) ) )
41 40 ad2antrr 
 |-  ( ( ( ( ph /\ ( ( X G Y ) ` R ) e. ( ( F ` X ) J ( F ` Y ) ) ) /\ f e. ( Y H X ) ) /\ ( ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) ` ( ( X G Y ) ` R ) ) = ( ( Y G X ) ` f ) ) -> ( ( X G Y ) ` R ) ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) ( ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) ` ( ( X G Y ) ` R ) ) )
42 simpr 
 |-  ( ( ( ( ph /\ ( ( X G Y ) ` R ) e. ( ( F ` X ) J ( F ` Y ) ) ) /\ f e. ( Y H X ) ) /\ ( ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) ` ( ( X G Y ) ` R ) ) = ( ( Y G X ) ` f ) ) -> ( ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) ` ( ( X G Y ) ` R ) ) = ( ( Y G X ) ` f ) )
43 41 42 breqtrd 
 |-  ( ( ( ( ph /\ ( ( X G Y ) ` R ) e. ( ( F ` X ) J ( F ` Y ) ) ) /\ f e. ( Y H X ) ) /\ ( ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) ` ( ( X G Y ) ` R ) ) = ( ( Y G X ) ` f ) ) -> ( ( X G Y ) ` R ) ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) ( ( Y G X ) ` f ) )
44 3 ad3antrrr 
 |-  ( ( ( ( ph /\ ( ( X G Y ) ` R ) e. ( ( F ` X ) J ( F ` Y ) ) ) /\ f e. ( Y H X ) ) /\ ( ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) ` ( ( X G Y ) ` R ) ) = ( ( Y G X ) ` f ) ) -> F ( C Faith D ) G )
45 6 ad3antrrr 
 |-  ( ( ( ( ph /\ ( ( X G Y ) ` R ) e. ( ( F ` X ) J ( F ` Y ) ) ) /\ f e. ( Y H X ) ) /\ ( ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) ` ( ( X G Y ) ` R ) ) = ( ( Y G X ) ` f ) ) -> R e. ( X H Y ) )
46 simplr 
 |-  ( ( ( ( ph /\ ( ( X G Y ) ` R ) e. ( ( F ` X ) J ( F ` Y ) ) ) /\ f e. ( Y H X ) ) /\ ( ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) ` ( ( X G Y ) ` R ) ) = ( ( Y G X ) ` f ) ) -> f e. ( Y H X ) )
47 1 2 44 25 26 45 46 18 28 fthinv 
 |-  ( ( ( ( ph /\ ( ( X G Y ) ` R ) e. ( ( F ` X ) J ( F ` Y ) ) ) /\ f e. ( Y H X ) ) /\ ( ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) ` ( ( X G Y ) ` R ) ) = ( ( Y G X ) ` f ) ) -> ( R ( X ( Inv ` C ) Y ) f <-> ( ( X G Y ) ` R ) ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) ( ( Y G X ) ` f ) ) )
48 43 47 mpbird 
 |-  ( ( ( ( ph /\ ( ( X G Y ) ` R ) e. ( ( F ` X ) J ( F ` Y ) ) ) /\ f e. ( Y H X ) ) /\ ( ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) ` ( ( X G Y ) ` R ) ) = ( ( Y G X ) ` f ) ) -> R ( X ( Inv ` C ) Y ) f )
49 1 18 24 25 26 8 48 inviso1 
 |-  ( ( ( ( ph /\ ( ( X G Y ) ` R ) e. ( ( F ` X ) J ( F ` Y ) ) ) /\ f e. ( Y H X ) ) /\ ( ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) ` ( ( X G Y ) ` R ) ) = ( ( Y G X ) ` f ) ) -> R e. ( X I Y ) )
50 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
51 7 adantr 
 |-  ( ( ph /\ ( ( X G Y ) ` R ) e. ( ( F ` X ) J ( F ` Y ) ) ) -> F ( C Full D ) G )
52 5 adantr 
 |-  ( ( ph /\ ( ( X G Y ) ` R ) e. ( ( F ` X ) J ( F ` Y ) ) ) -> Y e. B )
53 4 adantr 
 |-  ( ( ph /\ ( ( X G Y ) ` R ) e. ( ( F ` X ) J ( F ` Y ) ) ) -> X e. B )
54 27 50 9 29 32 31 isohom 
 |-  ( ph -> ( ( F ` Y ) J ( F ` X ) ) C_ ( ( F ` Y ) ( Hom ` D ) ( F ` X ) ) )
55 54 adantr 
 |-  ( ( ph /\ ( ( X G Y ) ` R ) e. ( ( F ` X ) J ( F ` Y ) ) ) -> ( ( F ` Y ) J ( F ` X ) ) C_ ( ( F ` Y ) ( Hom ` D ) ( F ` X ) ) )
56 27 28 29 31 32 9 invf 
 |-  ( ph -> ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) : ( ( F ` X ) J ( F ` Y ) ) --> ( ( F ` Y ) J ( F ` X ) ) )
57 56 ffvelrnda 
 |-  ( ( ph /\ ( ( X G Y ) ` R ) e. ( ( F ` X ) J ( F ` Y ) ) ) -> ( ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) ` ( ( X G Y ) ` R ) ) e. ( ( F ` Y ) J ( F ` X ) ) )
58 55 57 sseldd 
 |-  ( ( ph /\ ( ( X G Y ) ` R ) e. ( ( F ` X ) J ( F ` Y ) ) ) -> ( ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) ` ( ( X G Y ) ` R ) ) e. ( ( F ` Y ) ( Hom ` D ) ( F ` X ) ) )
59 1 50 2 51 52 53 58 fulli 
 |-  ( ( ph /\ ( ( X G Y ) ` R ) e. ( ( F ` X ) J ( F ` Y ) ) ) -> E. f e. ( Y H X ) ( ( ( F ` X ) ( Inv ` D ) ( F ` Y ) ) ` ( ( X G Y ) ` R ) ) = ( ( Y G X ) ` f ) )
60 49 59 r19.29a 
 |-  ( ( ph /\ ( ( X G Y ) ` R ) e. ( ( F ` X ) J ( F ` Y ) ) ) -> R e. ( X I Y ) )
61 17 60 impbida 
 |-  ( ph -> ( R e. ( X I Y ) <-> ( ( X G Y ) ` R ) e. ( ( F ` X ) J ( F ` Y ) ) ) )