Metamath Proof Explorer

Theorem fucsect

Description: Two natural transformations are in a section iff all the components are in a section relation. (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 ) )
fucsect.s 
|- S = ( Sect ` Q )
fucsect.t 
|- T = ( Sect ` D )
Assertion fucsect 
|- ( ph -> ( U ( F S G ) V <-> ( U e. ( F N G ) /\ V e. ( G N F ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) T ( ( 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 fucsect.s 
 |-  S = ( Sect ` Q )
7 fucsect.t 
 |-  T = ( Sect ` D )
8 1 fucbas 
 |-  ( C Func D ) = ( Base ` Q )
9 1 3 fuchom 
 |-  N = ( Hom ` Q )
10 eqid 
 |-  ( comp ` Q ) = ( comp ` Q )
11 eqid 
 |-  ( Id ` Q ) = ( Id ` Q )
12 funcrcl 
 |-  ( F e. ( C Func D ) -> ( C e. Cat /\ D e. Cat ) )
13 4 12 syl 
 |-  ( ph -> ( C e. Cat /\ D e. Cat ) )
14 13 simpld 
 |-  ( ph -> C e. Cat )
15 13 simprd 
 |-  ( ph -> D e. Cat )
16 1 14 15 fuccat 
 |-  ( ph -> Q e. Cat )
17 8 9 10 11 6 16 4 5 issect 
 |-  ( ph -> ( U ( F S G ) V <-> ( U e. ( F N G ) /\ V e. ( G N F ) /\ ( V ( <. F , G >. ( comp ` Q ) F ) U ) = ( ( Id ` Q ) ` F ) ) ) )
18 ovex 
 |-  ( ( V ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) e. _V
19 18 rgenw 
 |-  A. x e. B ( ( V ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) e. _V
20 mpteqb 
 |-  ( A. x e. B ( ( V ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) e. _V -> ( ( x e. B |-> ( ( V ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) = ( x e. B |-> ( ( Id ` D ) ` ( ( 1st ` F ) ` x ) ) ) <-> A. x e. B ( ( V ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) = ( ( Id ` D ) ` ( ( 1st ` F ) ` x ) ) ) )
21 19 20 mp1i 
 |-  ( ( ph /\ ( U e. ( F N G ) /\ V e. ( G N F ) ) ) -> ( ( x e. B |-> ( ( V ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) = ( x e. B |-> ( ( Id ` D ) ` ( ( 1st ` F ) ` x ) ) ) <-> A. x e. B ( ( V ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) = ( ( Id ` D ) ` ( ( 1st ` F ) ` x ) ) ) )
22 eqid 
 |-  ( comp ` D ) = ( comp ` D )
23 simprl 
 |-  ( ( ph /\ ( U e. ( F N G ) /\ V e. ( G N F ) ) ) -> U e. ( F N G ) )
24 simprr 
 |-  ( ( ph /\ ( U e. ( F N G ) /\ V e. ( G N F ) ) ) -> V e. ( G N F ) )
25 1 3 2 22 10 23 24 fucco 
 |-  ( ( ph /\ ( U e. ( F N G ) /\ V e. ( G N F ) ) ) -> ( V ( <. F , G >. ( comp ` Q ) F ) U ) = ( x e. B |-> ( ( V ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) )
26 eqid 
 |-  ( Id ` D ) = ( Id ` D )
27 4 adantr 
 |-  ( ( ph /\ ( U e. ( F N G ) /\ V e. ( G N F ) ) ) -> F e. ( C Func D ) )
28 1 11 26 27 fucid 
 |-  ( ( ph /\ ( U e. ( F N G ) /\ V e. ( G N F ) ) ) -> ( ( Id ` Q ) ` F ) = ( ( Id ` D ) o. ( 1st ` F ) ) )
29 15 adantr 
 |-  ( ( ph /\ ( U e. ( F N G ) /\ V e. ( G N F ) ) ) -> D e. Cat )
30 eqid 
 |-  ( Base ` D ) = ( Base ` D )
31 30 26 cidfn 
 |-  ( D e. Cat -> ( Id ` D ) Fn ( Base ` D ) )
32 29 31 syl 
 |-  ( ( ph /\ ( U e. ( F N G ) /\ V e. ( G N F ) ) ) -> ( Id ` D ) Fn ( Base ` D ) )
33 dffn2 
 |-  ( ( Id ` D ) Fn ( Base ` D ) <-> ( Id ` D ) : ( Base ` D ) --> _V )
34 32 33 sylib 
 |-  ( ( ph /\ ( U e. ( F N G ) /\ V e. ( G N F ) ) ) -> ( Id ` D ) : ( Base ` D ) --> _V )
35 relfunc 
 |-  Rel ( C Func D )
36 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
37 35 4 36 sylancr 
 |-  ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
38 2 30 37 funcf1 
 |-  ( ph -> ( 1st ` F ) : B --> ( Base ` D ) )
39 38 adantr 
 |-  ( ( ph /\ ( U e. ( F N G ) /\ V e. ( G N F ) ) ) -> ( 1st ` F ) : B --> ( Base ` D ) )
40 fcompt 
 |-  ( ( ( Id ` D ) : ( Base ` D ) --> _V /\ ( 1st ` F ) : B --> ( Base ` D ) ) -> ( ( Id ` D ) o. ( 1st ` F ) ) = ( x e. B |-> ( ( Id ` D ) ` ( ( 1st ` F ) ` x ) ) ) )
41 34 39 40 syl2anc 
 |-  ( ( ph /\ ( U e. ( F N G ) /\ V e. ( G N F ) ) ) -> ( ( Id ` D ) o. ( 1st ` F ) ) = ( x e. B |-> ( ( Id ` D ) ` ( ( 1st ` F ) ` x ) ) ) )
42 28 41 eqtrd 
 |-  ( ( ph /\ ( U e. ( F N G ) /\ V e. ( G N F ) ) ) -> ( ( Id ` Q ) ` F ) = ( x e. B |-> ( ( Id ` D ) ` ( ( 1st ` F ) ` x ) ) ) )
43 25 42 eqeq12d 
 |-  ( ( ph /\ ( U e. ( F N G ) /\ V e. ( G N F ) ) ) -> ( ( V ( <. F , G >. ( comp ` Q ) F ) U ) = ( ( Id ` Q ) ` F ) <-> ( x e. B |-> ( ( V ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) ) = ( x e. B |-> ( ( Id ` D ) ` ( ( 1st ` F ) ` x ) ) ) ) )
44 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
45 29 adantr 
 |-  ( ( ( ph /\ ( U e. ( F N G ) /\ V e. ( G N F ) ) ) /\ x e. B ) -> D e. Cat )
46 39 ffvelrnda 
 |-  ( ( ( ph /\ ( U e. ( F N G ) /\ V e. ( G N F ) ) ) /\ x e. B ) -> ( ( 1st ` F ) ` x ) e. ( Base ` D ) )
47 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ G e. ( C Func D ) ) -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) )
48 35 5 47 sylancr 
 |-  ( ph -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) )
49 2 30 48 funcf1 
 |-  ( ph -> ( 1st ` G ) : B --> ( Base ` D ) )
50 49 adantr 
 |-  ( ( ph /\ ( U e. ( F N G ) /\ V e. ( G N F ) ) ) -> ( 1st ` G ) : B --> ( Base ` D ) )
51 50 ffvelrnda 
 |-  ( ( ( ph /\ ( U e. ( F N G ) /\ V e. ( G N F ) ) ) /\ x e. B ) -> ( ( 1st ` G ) ` x ) e. ( Base ` D ) )
52 23 adantr 
 |-  ( ( ( ph /\ ( U e. ( F N G ) /\ V e. ( G N F ) ) ) /\ x e. B ) -> U e. ( F N G ) )
53 3 52 nat1st2nd 
 |-  ( ( ( ph /\ ( U e. ( F N G ) /\ V e. ( G N F ) ) ) /\ x e. B ) -> U e. ( <. ( 1st ` F ) , ( 2nd ` F ) >. N <. ( 1st ` G ) , ( 2nd ` G ) >. ) )
54 simpr 
 |-  ( ( ( ph /\ ( U e. ( F N G ) /\ V e. ( G N F ) ) ) /\ x e. B ) -> x e. B )
55 3 53 2 44 54 natcl 
 |-  ( ( ( ph /\ ( U e. ( F N G ) /\ V e. ( G N F ) ) ) /\ x e. B ) -> ( U ` x ) e. ( ( ( 1st ` F ) ` x ) ( Hom ` D ) ( ( 1st ` G ) ` x ) ) )
56 24 adantr 
 |-  ( ( ( ph /\ ( U e. ( F N G ) /\ V e. ( G N F ) ) ) /\ x e. B ) -> V e. ( G N F ) )
57 3 56 nat1st2nd 
 |-  ( ( ( ph /\ ( U e. ( F N G ) /\ V e. ( G N F ) ) ) /\ x e. B ) -> V e. ( <. ( 1st ` G ) , ( 2nd ` G ) >. N <. ( 1st ` F ) , ( 2nd ` F ) >. ) )
58 3 57 2 44 54 natcl 
 |-  ( ( ( ph /\ ( U e. ( F N G ) /\ V e. ( G N F ) ) ) /\ x e. B ) -> ( V ` x ) e. ( ( ( 1st ` G ) ` x ) ( Hom ` D ) ( ( 1st ` F ) ` x ) ) )
59 30 44 22 26 7 45 46 51 55 58 issect2 
 |-  ( ( ( ph /\ ( U e. ( F N G ) /\ V e. ( G N F ) ) ) /\ x e. B ) -> ( ( U ` x ) ( ( ( 1st ` F ) ` x ) T ( ( 1st ` G ) ` x ) ) ( V ` x ) <-> ( ( V ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) = ( ( Id ` D ) ` ( ( 1st ` F ) ` x ) ) ) )
60 59 ralbidva 
 |-  ( ( ph /\ ( U e. ( F N G ) /\ V e. ( G N F ) ) ) -> ( A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) T ( ( 1st ` G ) ` x ) ) ( V ` x ) <-> A. x e. B ( ( V ` x ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ( comp ` D ) ( ( 1st ` F ) ` x ) ) ( U ` x ) ) = ( ( Id ` D ) ` ( ( 1st ` F ) ` x ) ) ) )
61 21 43 60 3bitr4d 
 |-  ( ( ph /\ ( U e. ( F N G ) /\ V e. ( G N F ) ) ) -> ( ( V ( <. F , G >. ( comp ` Q ) F ) U ) = ( ( Id ` Q ) ` F ) <-> A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) T ( ( 1st ` G ) ` x ) ) ( V ` x ) ) )
62 61 pm5.32da 
 |-  ( ph -> ( ( ( U e. ( F N G ) /\ V e. ( G N F ) ) /\ ( V ( <. F , G >. ( comp ` Q ) F ) U ) = ( ( Id ` Q ) ` F ) ) <-> ( ( U e. ( F N G ) /\ V e. ( G N F ) ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) T ( ( 1st ` G ) ` x ) ) ( V ` x ) ) ) )
63 df-3an 
 |-  ( ( U e. ( F N G ) /\ V e. ( G N F ) /\ ( V ( <. F , G >. ( comp ` Q ) F ) U ) = ( ( Id ` Q ) ` F ) ) <-> ( ( U e. ( F N G ) /\ V e. ( G N F ) ) /\ ( V ( <. F , G >. ( comp ` Q ) F ) U ) = ( ( Id ` Q ) ` F ) ) )
64 df-3an 
 |-  ( ( U e. ( F N G ) /\ V e. ( G N F ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) T ( ( 1st ` G ) ` x ) ) ( V ` x ) ) <-> ( ( U e. ( F N G ) /\ V e. ( G N F ) ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) T ( ( 1st ` G ) ` x ) ) ( V ` x ) ) )
65 62 63 64 3bitr4g 
 |-  ( ph -> ( ( U e. ( F N G ) /\ V e. ( G N F ) /\ ( V ( <. F , G >. ( comp ` Q ) F ) U ) = ( ( Id ` Q ) ` F ) ) <-> ( U e. ( F N G ) /\ V e. ( G N F ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) T ( ( 1st ` G ) ` x ) ) ( V ` x ) ) ) )
66 17 65 bitrd 
 |-  ( ph -> ( U ( F S G ) V <-> ( U e. ( F N G ) /\ V e. ( G N F ) /\ A. x e. B ( U ` x ) ( ( ( 1st ` F ) ` x ) T ( ( 1st ` G ) ` x ) ) ( V ` x ) ) ) )