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 ffvelrnda
 |-  ( ( 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 ffvelrnda
 |-  ( ( 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 ) ) ) )