Metamath Proof Explorer

Theorem setcsect

Description: A section in the category of sets, written out. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses setcmon.c 
|- C = ( SetCat ` U )
setcmon.u 
|- ( ph -> U e. V )
setcmon.x 
|- ( ph -> X e. U )
setcmon.y 
|- ( ph -> Y e. U )
setcsect.n 
|- S = ( Sect ` C )
Assertion setcsect 
|- ( ph -> ( F ( X S Y ) G <-> ( F : X --> Y /\ G : Y --> X /\ ( G o. F ) = ( _I |` X ) ) ) )

Proof

Step Hyp Ref Expression
1 setcmon.c 
 |-  C = ( SetCat ` U )
2 setcmon.u 
 |-  ( ph -> U e. V )
3 setcmon.x 
 |-  ( ph -> X e. U )
4 setcmon.y 
 |-  ( ph -> Y e. U )
5 setcsect.n 
 |-  S = ( Sect ` C )
6 eqid 
 |-  ( Base ` C ) = ( Base ` C )
7 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
8 eqid 
 |-  ( comp ` C ) = ( comp ` C )
9 eqid 
 |-  ( Id ` C ) = ( Id ` C )
10 1 setccat 
 |-  ( U e. V -> C e. Cat )
11 2 10 syl 
 |-  ( ph -> C e. Cat )
12 1 2 setcbas 
 |-  ( ph -> U = ( Base ` C ) )
13 3 12 eleqtrd 
 |-  ( ph -> X e. ( Base ` C ) )
14 4 12 eleqtrd 
 |-  ( ph -> Y e. ( Base ` C ) )
15 6 7 8 9 5 11 13 14 issect 
 |-  ( ph -> ( F ( X S Y ) G <-> ( F e. ( X ( Hom ` C ) Y ) /\ G e. ( Y ( Hom ` C ) X ) /\ ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) ) )
16 1 2 7 3 4 elsetchom 
 |-  ( ph -> ( F e. ( X ( Hom ` C ) Y ) <-> F : X --> Y ) )
17 1 2 7 4 3 elsetchom 
 |-  ( ph -> ( G e. ( Y ( Hom ` C ) X ) <-> G : Y --> X ) )
18 16 17 anbi12d 
 |-  ( ph -> ( ( F e. ( X ( Hom ` C ) Y ) /\ G e. ( Y ( Hom ` C ) X ) ) <-> ( F : X --> Y /\ G : Y --> X ) ) )
19 18 anbi1d 
 |-  ( ph -> ( ( ( F e. ( X ( Hom ` C ) Y ) /\ G e. ( Y ( Hom ` C ) X ) ) /\ ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) <-> ( ( F : X --> Y /\ G : Y --> X ) /\ ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) ) )
20 2 adantr 
 |-  ( ( ph /\ ( F : X --> Y /\ G : Y --> X ) ) -> U e. V )
21 3 adantr 
 |-  ( ( ph /\ ( F : X --> Y /\ G : Y --> X ) ) -> X e. U )
22 4 adantr 
 |-  ( ( ph /\ ( F : X --> Y /\ G : Y --> X ) ) -> Y e. U )
23 simprl 
 |-  ( ( ph /\ ( F : X --> Y /\ G : Y --> X ) ) -> F : X --> Y )
24 simprr 
 |-  ( ( ph /\ ( F : X --> Y /\ G : Y --> X ) ) -> G : Y --> X )
25 1 20 8 21 22 21 23 24 setcco 
 |-  ( ( ph /\ ( F : X --> Y /\ G : Y --> X ) ) -> ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( G o. F ) )
26 1 9 2 3 setcid 
 |-  ( ph -> ( ( Id ` C ) ` X ) = ( _I |` X ) )
27 26 adantr 
 |-  ( ( ph /\ ( F : X --> Y /\ G : Y --> X ) ) -> ( ( Id ` C ) ` X ) = ( _I |` X ) )
28 25 27 eqeq12d 
 |-  ( ( ph /\ ( F : X --> Y /\ G : Y --> X ) ) -> ( ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) <-> ( G o. F ) = ( _I |` X ) ) )
29 28 pm5.32da 
 |-  ( ph -> ( ( ( F : X --> Y /\ G : Y --> X ) /\ ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) <-> ( ( F : X --> Y /\ G : Y --> X ) /\ ( G o. F ) = ( _I |` X ) ) ) )
30 19 29 bitrd 
 |-  ( ph -> ( ( ( F e. ( X ( Hom ` C ) Y ) /\ G e. ( Y ( Hom ` C ) X ) ) /\ ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) <-> ( ( F : X --> Y /\ G : Y --> X ) /\ ( G o. F ) = ( _I |` X ) ) ) )
31 df-3an 
 |-  ( ( F e. ( X ( Hom ` C ) Y ) /\ G e. ( Y ( Hom ` C ) X ) /\ ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) <-> ( ( F e. ( X ( Hom ` C ) Y ) /\ G e. ( Y ( Hom ` C ) X ) ) /\ ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) )
32 df-3an 
 |-  ( ( F : X --> Y /\ G : Y --> X /\ ( G o. F ) = ( _I |` X ) ) <-> ( ( F : X --> Y /\ G : Y --> X ) /\ ( G o. F ) = ( _I |` X ) ) )
33 30 31 32 3bitr4g 
 |-  ( ph -> ( ( F e. ( X ( Hom ` C ) Y ) /\ G e. ( Y ( Hom ` C ) X ) /\ ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) <-> ( F : X --> Y /\ G : Y --> X /\ ( G o. F ) = ( _I |` X ) ) ) )
34 15 33 bitrd 
 |-  ( ph -> ( F ( X S Y ) G <-> ( F : X --> Y /\ G : Y --> X /\ ( G o. F ) = ( _I |` X ) ) ) )