Metamath Proof Explorer

Theorem fucinv

Description: Two natural transformations are inverses of each other iff all the components are inverse. (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 ) )
fucinv.i 
|- I = ( Inv ` Q )
fucinv.j 
|- J = ( Inv ` D )
Assertion fucinv 
|- ( ph -> ( U ( F I G ) V <-> ( U e. ( F N G ) /\ V e. ( G N F ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ( V ` 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 fucinv.i 
 |-  I = ( Inv ` Q )
7 fucinv.j 
 |-  J = ( Inv ` D )
8 eqid 
 |-  ( Sect ` Q ) = ( Sect ` Q )
9 eqid 
 |-  ( Sect ` D ) = ( Sect ` D )
10 1 2 3 4 5 8 9 fucsect 
 |-  ( ph -> ( U ( F ( Sect ` Q ) G ) V <-> ( U e. ( F N G ) /\ V e. ( G N F ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) ) ) )
11 1 2 3 5 4 8 9 fucsect 
 |-  ( ph -> ( V ( G ( Sect ` Q ) F ) U <-> ( V e. ( G N F ) /\ U e. ( F N G ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) )
12 10 11 anbi12d 
 |-  ( ph -> ( ( U ( F ( Sect ` Q ) G ) V /\ V ( G ( Sect ` Q ) F ) U ) <-> ( ( U e. ( F N G ) /\ V e. ( G N F ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) ) /\ ( V e. ( G N F ) /\ U e. ( F N G ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) ) )
13 1 fucbas 
 |-  ( C Func D ) = ( Base ` Q )
14 funcrcl 
 |-  ( F e. ( C Func D ) -> ( C e. Cat /\ D e. Cat ) )
15 4 14 syl 
 |-  ( ph -> ( C e. Cat /\ D e. Cat ) )
16 15 simpld 
 |-  ( ph -> C e. Cat )
17 15 simprd 
 |-  ( ph -> D e. Cat )
18 1 16 17 fuccat 
 |-  ( ph -> Q e. Cat )
19 13 6 18 4 5 8 isinv 
 |-  ( ph -> ( U ( F I G ) V <-> ( U ( F ( Sect ` Q ) G ) V /\ V ( G ( Sect ` Q ) F ) U ) ) )
20 eqid 
 |-  ( Base ` D ) = ( Base ` D )
21 17 adantr 
 |-  ( ( ph /\ x e. B ) -> D e. Cat )
22 relfunc 
 |-  Rel ( C Func D )
23 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
24 22 4 23 sylancr 
 |-  ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
25 2 20 24 funcf1 
 |-  ( ph -> ( 1st ` F ) : B --> ( Base ` D ) )
26 25 ffvelcdmda 
 |-  ( ( ph /\ x e. B ) -> ( ( 1st ` F ) ` x ) e. ( Base ` D ) )
27 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ G e. ( C Func D ) ) -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) )
28 22 5 27 sylancr 
 |-  ( ph -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) )
29 2 20 28 funcf1 
 |-  ( ph -> ( 1st ` G ) : B --> ( Base ` D ) )
30 29 ffvelcdmda 
 |-  ( ( ph /\ x e. B ) -> ( ( 1st ` G ) ` x ) e. ( Base ` D ) )
31 20 7 21 26 30 9 isinv 
 |-  ( ( ph /\ x e. B ) -> ( ( U ` x ) ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ( V ` x ) <-> ( ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) /\ ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) )
32 31 ralbidva 
 |-  ( ph -> ( A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ( V ` x ) <-> A. x e. B ( ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) /\ ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) )
33 r19.26 
 |-  ( A. x e. B ( ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) /\ ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) <-> ( A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) )
34 32 33 bitrdi 
 |-  ( ph -> ( A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ( V ` x ) <-> ( A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) )
35 34 anbi2d 
 |-  ( ph -> ( ( ( U e. ( F N G ) /\ V e. ( G N F ) ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ( V ` x ) ) <-> ( ( U e. ( F N G ) /\ V e. ( G N F ) ) /\ ( A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) ) )
36 df-3an 
 |-  ( ( U e. ( F N G ) /\ V e. ( G N F ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ( V ` x ) ) <-> ( ( U e. ( F N G ) /\ V e. ( G N F ) ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ( V ` x ) ) )
37 df-3an 
 |-  ( ( U e. ( F N G ) /\ V e. ( G N F ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) ) <-> ( ( U e. ( F N G ) /\ V e. ( G N F ) ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) ) )
38 3ancoma 
 |-  ( ( V e. ( G N F ) /\ U e. ( F N G ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) <-> ( U e. ( F N G ) /\ V e. ( G N F ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) )
39 df-3an 
 |-  ( ( U e. ( F N G ) /\ V e. ( G N F ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) <-> ( ( U e. ( F N G ) /\ V e. ( G N F ) ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) )
40 38 39 bitri 
 |-  ( ( V e. ( G N F ) /\ U e. ( F N G ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) <-> ( ( U e. ( F N G ) /\ V e. ( G N F ) ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) )
41 37 40 anbi12i 
 |-  ( ( ( U e. ( F N G ) /\ V e. ( G N F ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) ) /\ ( V e. ( G N F ) /\ U e. ( F N G ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) <-> ( ( ( U e. ( F N G ) /\ V e. ( G N F ) ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) ) /\ ( ( U e. ( F N G ) /\ V e. ( G N F ) ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) )
42 anandi 
 |-  ( ( ( U e. ( F N G ) /\ V e. ( G N F ) ) /\ ( A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) <-> ( ( ( U e. ( F N G ) /\ V e. ( G N F ) ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) ) /\ ( ( U e. ( F N G ) /\ V e. ( G N F ) ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) )
43 41 42 bitr4i 
 |-  ( ( ( U e. ( F N G ) /\ V e. ( G N F ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) ) /\ ( V e. ( G N F ) /\ U e. ( F N G ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) <-> ( ( U e. ( F N G ) /\ V e. ( G N F ) ) /\ ( A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) )
44 35 36 43 3bitr4g 
 |-  ( ph -> ( ( U e. ( F N G ) /\ V e. ( G N F ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ( V ` x ) ) <-> ( ( U e. ( F N G ) /\ V e. ( G N F ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) ( Sect ` D ) ( ( 1st ` G ) ` x ) ) ( V ` x ) ) /\ ( V e. ( G N F ) /\ U e. ( F N G ) /\ A. x e. B ( V ` x ) ( ( ( 1st ` G ) ` x ) ( Sect ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) ) )
45 12 19 44 3bitr4d 
 |-  ( ph -> ( U ( F I G ) V <-> ( U e. ( F N G ) /\ V e. ( G N F ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ( V ` x ) ) ) )