Metamath Proof Explorer

Theorem catcsect

Description: The property " F is a section of G " in a category of small categories (in a universe). (Contributed by Zhi Wang, 14-Nov-2025)

Ref Expression
Hypotheses catcsect.c 
|- C = ( CatCat ` U )
catcsect.h 
|- H = ( Hom ` C )
catcsect.i 
|- I = ( idFunc ` X )
catcsect.s 
|- S = ( Sect ` C )
Assertion catcsect 
|- ( F ( X S Y ) G <-> ( ( F e. ( X H Y ) /\ G e. ( Y H X ) ) /\ ( G o.func F ) = I ) )

Proof

Step Hyp Ref Expression
1 catcsect.c 
 |-  C = ( CatCat ` U )
2 catcsect.h 
 |-  H = ( Hom ` C )
3 catcsect.i 
 |-  I = ( idFunc ` X )
4 catcsect.s 
 |-  S = ( Sect ` C )
5 id 
 |-  ( F ( X S Y ) G -> F ( X S Y ) G )
6 4 5 sectrcl 
 |-  ( F ( X S Y ) G -> C e. Cat )
7 eqid 
 |-  ( Base ` C ) = ( Base ` C )
8 4 5 7 sectrcl2 
 |-  ( F ( X S Y ) G -> ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) ) )
9 6 8 jca 
 |-  ( F ( X S Y ) G -> ( C e. Cat /\ ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) ) ) )
10 simpl 
 |-  ( ( F e. ( X H Y ) /\ G e. ( Y H X ) ) -> F e. ( X H Y ) )
11 1 2 10 catcrcl 
 |-  ( ( F e. ( X H Y ) /\ G e. ( Y H X ) ) -> U e. _V )
12 1 catccat 
 |-  ( U e. _V -> C e. Cat )
13 11 12 syl 
 |-  ( ( F e. ( X H Y ) /\ G e. ( Y H X ) ) -> C e. Cat )
14 1 2 10 7 catcrcl2 
 |-  ( ( F e. ( X H Y ) /\ G e. ( Y H X ) ) -> ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) ) )
15 13 14 jca 
 |-  ( ( F e. ( X H Y ) /\ G e. ( Y H X ) ) -> ( C e. Cat /\ ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) ) ) )
16 15 3adant3 
 |-  ( ( F e. ( X H Y ) /\ G e. ( Y H X ) /\ ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) -> ( C e. Cat /\ ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) ) ) )
17 eqid 
 |-  ( comp ` C ) = ( comp ` C )
18 eqid 
 |-  ( Id ` C ) = ( Id ` C )
19 simpl 
 |-  ( ( C e. Cat /\ ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) ) ) -> C e. Cat )
20 simprl 
 |-  ( ( C e. Cat /\ ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) ) ) -> X e. ( Base ` C ) )
21 simprr 
 |-  ( ( C e. Cat /\ ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) ) ) -> Y e. ( Base ` C ) )
22 7 2 17 18 4 19 20 21 issect 
 |-  ( ( C e. Cat /\ ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) ) ) -> ( F ( X S Y ) G <-> ( F e. ( X H Y ) /\ G e. ( Y H X ) /\ ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) ) )
23 9 16 22 pm5.21nii 
 |-  ( F ( X S Y ) G <-> ( F e. ( X H Y ) /\ G e. ( Y H X ) /\ ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) )
24 df-3an 
 |-  ( ( F e. ( X H Y ) /\ G e. ( Y H X ) /\ ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) <-> ( ( F e. ( X H Y ) /\ G e. ( Y H X ) ) /\ ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) )
25 15 20 syl 
 |-  ( ( F e. ( X H Y ) /\ G e. ( Y H X ) ) -> X e. ( Base ` C ) )
26 15 21 syl 
 |-  ( ( F e. ( X H Y ) /\ G e. ( Y H X ) ) -> Y e. ( Base ` C ) )
27 1 2 10 elcatchom 
 |-  ( ( F e. ( X H Y ) /\ G e. ( Y H X ) ) -> F e. ( X Func Y ) )
28 simpr 
 |-  ( ( F e. ( X H Y ) /\ G e. ( Y H X ) ) -> G e. ( Y H X ) )
29 1 2 28 elcatchom 
 |-  ( ( F e. ( X H Y ) /\ G e. ( Y H X ) ) -> G e. ( Y Func X ) )
30 1 7 11 17 25 26 25 27 29 catcco 
 |-  ( ( F e. ( X H Y ) /\ G e. ( Y H X ) ) -> ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( G o.func F ) )
31 1 7 18 3 11 25 catcid 
 |-  ( ( F e. ( X H Y ) /\ G e. ( Y H X ) ) -> ( ( Id ` C ) ` X ) = I )
32 30 31 eqeq12d 
 |-  ( ( F e. ( X H Y ) /\ G e. ( Y H X ) ) -> ( ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) <-> ( G o.func F ) = I ) )
33 32 pm5.32i 
 |-  ( ( ( F e. ( X H Y ) /\ G e. ( Y H X ) ) /\ ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) <-> ( ( F e. ( X H Y ) /\ G e. ( Y H X ) ) /\ ( G o.func F ) = I ) )
34 23 24 33 3bitri 
 |-  ( F ( X S Y ) G <-> ( ( F e. ( X H Y ) /\ G e. ( Y H X ) ) /\ ( G o.func F ) = I ) )