Metamath Proof Explorer

Theorem sectrcl

Description: Reverse closure for section relations. (Contributed by Zhi Wang, 14-Nov-2025)

Ref Expression
Hypotheses sectrcl.s 
|- S = ( Sect ` C )
sectrcl.f 
|- ( ph -> F ( X S Y ) G )
Assertion sectrcl 
|- ( ph -> C e. Cat )

Proof

Step Hyp Ref Expression
1 sectrcl.s 
 |-  S = ( Sect ` C )
2 sectrcl.f 
 |-  ( ph -> F ( X S Y ) G )
3 df-br 
 |-  ( F ( X S Y ) G <-> <. F , G >. e. ( X S Y ) )
4 df-ov 
 |-  ( X S Y ) = ( S ` <. X , Y >. )
5 4 eleq2i 
 |-  ( <. F , G >. e. ( X S Y ) <-> <. F , G >. e. ( S ` <. X , Y >. ) )
6 3 5 bitri 
 |-  ( F ( X S Y ) G <-> <. F , G >. e. ( S ` <. X , Y >. ) )
7 elfvne0 
 |-  ( <. F , G >. e. ( S ` <. X , Y >. ) -> S =/= (/) )
8 6 7 sylbi 
 |-  ( F ( X S Y ) G -> S =/= (/) )
9 1 neeq1i 
 |-  ( S =/= (/) <-> ( Sect ` C ) =/= (/) )
10 n0 
 |-  ( ( Sect ` C ) =/= (/) <-> E. x x e. ( Sect ` C ) )
11 9 10 bitri 
 |-  ( S =/= (/) <-> E. x x e. ( Sect ` C ) )
12 8 11 sylib 
 |-  ( F ( X S Y ) G -> E. x x e. ( Sect ` C ) )
13 df-sect 
 |-  Sect = ( c e. Cat |-> ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> { <. f , g >. | [. ( Hom ` c ) / h ]. ( ( f e. ( x h y ) /\ g e. ( y h x ) ) /\ ( g ( <. x , y >. ( comp ` c ) x ) f ) = ( ( Id ` c ) ` x ) ) } ) )
14 13 mptrcl 
 |-  ( x e. ( Sect ` C ) -> C e. Cat )
15 14 exlimiv 
 |-  ( E. x x e. ( Sect ` C ) -> C e. Cat )
16 2 12 15 3syl 
 |-  ( ph -> C e. Cat )