Metamath Proof Explorer

Theorem fuciso

Description: A natural transformation is an isomorphism of functors iff all its components are isomorphisms. (Contributed by Mario Carneiro, 28-Jan-2017)

Ref Expression
Hypotheses fuciso.q 
|- Q = ( C FuncCat D )
fuciso.b 
|- B = ( Base ` C )
fuciso.n 
|- N = ( C Nat D )
fuciso.f 
|- ( ph -> F e. ( C Func D ) )
fuciso.g 
|- ( ph -> G e. ( C Func D ) )
fuciso.i 
|- I = ( Iso ` Q )
fuciso.j 
|- J = ( Iso ` D )
Assertion fuciso 
|- ( ph -> ( A e. ( F I G ) <-> ( A e. ( F N G ) /\ A. x e. B ( A ` x ) e. ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fuciso.q 
 |-  Q = ( C FuncCat D )
2 fuciso.b 
 |-  B = ( Base ` C )
3 fuciso.n 
 |-  N = ( C Nat D )
4 fuciso.f 
 |-  ( ph -> F e. ( C Func D ) )
5 fuciso.g 
 |-  ( ph -> G e. ( C Func D ) )
6 fuciso.i 
 |-  I = ( Iso ` Q )
7 fuciso.j 
 |-  J = ( Iso ` D )
8 1 fucbas 
 |-  ( C Func D ) = ( Base ` Q )
9 1 3 fuchom 
 |-  N = ( Hom ` Q )
10 funcrcl 
 |-  ( F e. ( C Func D ) -> ( C e. Cat /\ D e. Cat ) )
11 4 10 syl 
 |-  ( ph -> ( C e. Cat /\ D e. Cat ) )
12 11 simpld 
 |-  ( ph -> C e. Cat )
13 11 simprd 
 |-  ( ph -> D e. Cat )
14 1 12 13 fuccat 
 |-  ( ph -> Q e. Cat )
15 8 9 6 14 4 5 isohom 
 |-  ( ph -> ( F I G ) C_ ( F N G ) )
16 15 sselda 
 |-  ( ( ph /\ A e. ( F I G ) ) -> A e. ( F N G ) )
17 eqid 
 |-  ( Base ` D ) = ( Base ` D )
18 eqid 
 |-  ( Inv ` D ) = ( Inv ` D )
19 13 ad2antrr 
 |-  ( ( ( ph /\ A e. ( F I G ) ) /\ x e. B ) -> D e. Cat )
20 relfunc 
 |-  Rel ( C Func D )
21 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
22 20 4 21 sylancr 
 |-  ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
23 2 17 22 funcf1 
 |-  ( ph -> ( 1st ` F ) : B --> ( Base ` D ) )
24 23 adantr 
 |-  ( ( ph /\ A e. ( F I G ) ) -> ( 1st ` F ) : B --> ( Base ` D ) )
25 24 ffvelrnda 
 |-  ( ( ( ph /\ A e. ( F I G ) ) /\ x e. B ) -> ( ( 1st ` F ) ` x ) e. ( Base ` D ) )
26 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ G e. ( C Func D ) ) -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) )
27 20 5 26 sylancr 
 |-  ( ph -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) )
28 2 17 27 funcf1 
 |-  ( ph -> ( 1st ` G ) : B --> ( Base ` D ) )
29 28 adantr 
 |-  ( ( ph /\ A e. ( F I G ) ) -> ( 1st ` G ) : B --> ( Base ` D ) )
30 29 ffvelrnda 
 |-  ( ( ( ph /\ A e. ( F I G ) ) /\ x e. B ) -> ( ( 1st ` G ) ` x ) e. ( Base ` D ) )
31 eqid 
 |-  ( Inv ` Q ) = ( Inv ` Q )
32 8 31 14 4 5 6 isoval 
 |-  ( ph -> ( F I G ) = dom ( F ( Inv ` Q ) G ) )
33 32 eleq2d 
 |-  ( ph -> ( A e. ( F I G ) <-> A e. dom ( F ( Inv ` Q ) G ) ) )
34 8 31 14 4 5 invfun 
 |-  ( ph -> Fun ( F ( Inv ` Q ) G ) )
35 funfvbrb 
 |-  ( Fun ( F ( Inv ` Q ) G ) -> ( A e. dom ( F ( Inv ` Q ) G ) <-> A ( F ( Inv ` Q ) G ) ( ( F ( Inv ` Q ) G ) ` A ) ) )
36 34 35 syl 
 |-  ( ph -> ( A e. dom ( F ( Inv ` Q ) G ) <-> A ( F ( Inv ` Q ) G ) ( ( F ( Inv ` Q ) G ) ` A ) ) )
37 33 36 bitrd 
 |-  ( ph -> ( A e. ( F I G ) <-> A ( F ( Inv ` Q ) G ) ( ( F ( Inv ` Q ) G ) ` A ) ) )
38 37 biimpa 
 |-  ( ( ph /\ A e. ( F I G ) ) -> A ( F ( Inv ` Q ) G ) ( ( F ( Inv ` Q ) G ) ` A ) )
39 1 2 3 4 5 31 18 fucinv 
 |-  ( ph -> ( A ( F ( Inv ` Q ) G ) ( ( F ( Inv ` Q ) G ) ` A ) <-> ( A e. ( F N G ) /\ ( ( F ( Inv ` Q ) G ) ` A ) e. ( G N F ) /\ A. x e. B ( A ` x ) ( ( ( 1st ` F ) ` x ) ( Inv ` D ) ( ( 1st ` G ) ` x ) ) ( ( ( F ( Inv ` Q ) G ) ` A ) ` x ) ) ) )
40 39 adantr 
 |-  ( ( ph /\ A e. ( F I G ) ) -> ( A ( F ( Inv ` Q ) G ) ( ( F ( Inv ` Q ) G ) ` A ) <-> ( A e. ( F N G ) /\ ( ( F ( Inv ` Q ) G ) ` A ) e. ( G N F ) /\ A. x e. B ( A ` x ) ( ( ( 1st ` F ) ` x ) ( Inv ` D ) ( ( 1st ` G ) ` x ) ) ( ( ( F ( Inv ` Q ) G ) ` A ) ` x ) ) ) )
41 38 40 mpbid 
 |-  ( ( ph /\ A e. ( F I G ) ) -> ( A e. ( F N G ) /\ ( ( F ( Inv ` Q ) G ) ` A ) e. ( G N F ) /\ A. x e. B ( A ` x ) ( ( ( 1st ` F ) ` x ) ( Inv ` D ) ( ( 1st ` G ) ` x ) ) ( ( ( F ( Inv ` Q ) G ) ` A ) ` x ) ) )
42 41 simp3d 
 |-  ( ( ph /\ A e. ( F I G ) ) -> A. x e. B ( A ` x ) ( ( ( 1st ` F ) ` x ) ( Inv ` D ) ( ( 1st ` G ) ` x ) ) ( ( ( F ( Inv ` Q ) G ) ` A ) ` x ) )
43 42 r19.21bi 
 |-  ( ( ( ph /\ A e. ( F I G ) ) /\ x e. B ) -> ( A ` x ) ( ( ( 1st ` F ) ` x ) ( Inv ` D ) ( ( 1st ` G ) ` x ) ) ( ( ( F ( Inv ` Q ) G ) ` A ) ` x ) )
44 17 18 19 25 30 7 43 inviso1 
 |-  ( ( ( ph /\ A e. ( F I G ) ) /\ x e. B ) -> ( A ` x ) e. ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) )
45 44 ralrimiva 
 |-  ( ( ph /\ A e. ( F I G ) ) -> A. x e. B ( A ` x ) e. ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) )
46 16 45 jca 
 |-  ( ( ph /\ A e. ( F I G ) ) -> ( A e. ( F N G ) /\ A. x e. B ( A ` x ) e. ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ) )
47 14 adantr 
 |-  ( ( ph /\ ( A e. ( F N G ) /\ A. x e. B ( A ` x ) e. ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ) ) -> Q e. Cat )
48 4 adantr 
 |-  ( ( ph /\ ( A e. ( F N G ) /\ A. x e. B ( A ` x ) e. ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ) ) -> F e. ( C Func D ) )
49 5 adantr 
 |-  ( ( ph /\ ( A e. ( F N G ) /\ A. x e. B ( A ` x ) e. ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ) ) -> G e. ( C Func D ) )
50 simprl 
 |-  ( ( ph /\ ( A e. ( F N G ) /\ A. x e. B ( A ` x ) e. ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ) ) -> A e. ( F N G ) )
51 13 ad2antrr 
 |-  ( ( ( ph /\ ( A e. ( F N G ) /\ A. x e. B ( A ` x ) e. ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ) ) /\ y e. B ) -> D e. Cat )
52 23 adantr 
 |-  ( ( ph /\ ( A e. ( F N G ) /\ A. x e. B ( A ` x ) e. ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ) ) -> ( 1st ` F ) : B --> ( Base ` D ) )
53 52 ffvelrnda 
 |-  ( ( ( ph /\ ( A e. ( F N G ) /\ A. x e. B ( A ` x ) e. ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ) ) /\ y e. B ) -> ( ( 1st ` F ) ` y ) e. ( Base ` D ) )
54 28 adantr 
 |-  ( ( ph /\ ( A e. ( F N G ) /\ A. x e. B ( A ` x ) e. ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ) ) -> ( 1st ` G ) : B --> ( Base ` D ) )
55 54 ffvelrnda 
 |-  ( ( ( ph /\ ( A e. ( F N G ) /\ A. x e. B ( A ` x ) e. ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ) ) /\ y e. B ) -> ( ( 1st ` G ) ` y ) e. ( Base ` D ) )
56 simprr 
 |-  ( ( ph /\ ( A e. ( F N G ) /\ A. x e. B ( A ` x ) e. ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ) ) -> A. x e. B ( A ` x ) e. ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) )
57 fveq2 
 |-  ( x = y -> ( A ` x ) = ( A ` y ) )
58 fveq2 
 |-  ( x = y -> ( ( 1st ` F ) ` x ) = ( ( 1st ` F ) ` y ) )
59 fveq2 
 |-  ( x = y -> ( ( 1st ` G ) ` x ) = ( ( 1st ` G ) ` y ) )
60 58 59 oveq12d 
 |-  ( x = y -> ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) = ( ( ( 1st ` F ) ` y ) J ( ( 1st ` G ) ` y ) ) )
61 57 60 eleq12d 
 |-  ( x = y -> ( ( A ` x ) e. ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) <-> ( A ` y ) e. ( ( ( 1st ` F ) ` y ) J ( ( 1st ` G ) ` y ) ) ) )
62 61 rspccva 
 |-  ( ( A. x e. B ( A ` x ) e. ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) /\ y e. B ) -> ( A ` y ) e. ( ( ( 1st ` F ) ` y ) J ( ( 1st ` G ) ` y ) ) )
63 56 62 sylan 
 |-  ( ( ( ph /\ ( A e. ( F N G ) /\ A. x e. B ( A ` x ) e. ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ) ) /\ y e. B ) -> ( A ` y ) e. ( ( ( 1st ` F ) ` y ) J ( ( 1st ` G ) ` y ) ) )
64 17 7 18 51 53 55 63 invisoinvr 
 |-  ( ( ( ph /\ ( A e. ( F N G ) /\ A. x e. B ( A ` x ) e. ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ) ) /\ y e. B ) -> ( A ` y ) ( ( ( 1st ` F ) ` y ) ( Inv ` D ) ( ( 1st ` G ) ` y ) ) ( ( ( ( 1st ` F ) ` y ) ( Inv ` D ) ( ( 1st ` G ) ` y ) ) ` ( A ` y ) ) )
65 1 2 3 48 49 31 18 50 64 invfuc 
 |-  ( ( ph /\ ( A e. ( F N G ) /\ A. x e. B ( A ` x ) e. ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ) ) -> A ( F ( Inv ` Q ) G ) ( y e. B |-> ( ( ( ( 1st ` F ) ` y ) ( Inv ` D ) ( ( 1st ` G ) ` y ) ) ` ( A ` y ) ) ) )
66 8 31 47 48 49 6 65 inviso1 
 |-  ( ( ph /\ ( A e. ( F N G ) /\ A. x e. B ( A ` x ) e. ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ) ) -> A e. ( F I G ) )
67 46 66 impbida 
 |-  ( ph -> ( A e. ( F I G ) <-> ( A e. ( F N G ) /\ A. x e. B ( A ` x ) e. ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ) ) )