Metamath Proof Explorer

Theorem sectrcl2

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 )
sectrcl2.b 
|- B = ( Base ` C )
Assertion sectrcl2 
|- ( ph -> ( X e. B /\ Y e. B ) )

Proof

Step Hyp Ref Expression
1 sectrcl.s 
 |-  S = ( Sect ` C )
2 sectrcl.f 
 |-  ( ph -> F ( X S Y ) G )
3 sectrcl2.b 
 |-  B = ( Base ` C )
4 df-br 
 |-  ( F ( X S Y ) G <-> <. F , G >. e. ( X S Y ) )
5 2 4 sylib 
 |-  ( ph -> <. F , G >. e. ( X S Y ) )
6 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
7 eqid 
 |-  ( comp ` C ) = ( comp ` C )
8 eqid 
 |-  ( Id ` C ) = ( Id ` C )
9 1 2 sectrcl 
 |-  ( ph -> C e. Cat )
10 3 6 7 8 1 9 sectffval 
 |-  ( ph -> S = ( x e. B , y e. B |-> { <. f , g >. | ( ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) x ) ) /\ ( g ( <. x , y >. ( comp ` C ) x ) f ) = ( ( Id ` C ) ` x ) ) } ) )
11 10 oveqd 
 |-  ( ph -> ( X S Y ) = ( X ( x e. B , y e. B |-> { <. f , g >. | ( ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) x ) ) /\ ( g ( <. x , y >. ( comp ` C ) x ) f ) = ( ( Id ` C ) ` x ) ) } ) Y ) )
12 5 11 eleqtrd 
 |-  ( ph -> <. F , G >. e. ( X ( x e. B , y e. B |-> { <. f , g >. | ( ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) x ) ) /\ ( g ( <. x , y >. ( comp ` C ) x ) f ) = ( ( Id ` C ) ` x ) ) } ) Y ) )
13 eqid 
 |-  ( x e. B , y e. B |-> { <. f , g >. | ( ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) x ) ) /\ ( g ( <. x , y >. ( comp ` C ) x ) f ) = ( ( Id ` C ) ` x ) ) } ) = ( x e. B , y e. B |-> { <. f , g >. | ( ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) x ) ) /\ ( g ( <. x , y >. ( comp ` C ) x ) f ) = ( ( Id ` C ) ` x ) ) } )
14 13 elmpocl 
 |-  ( <. F , G >. e. ( X ( x e. B , y e. B |-> { <. f , g >. | ( ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) x ) ) /\ ( g ( <. x , y >. ( comp ` C ) x ) f ) = ( ( Id ` C ) ` x ) ) } ) Y ) -> ( X e. B /\ Y e. B ) )
15 12 14 syl 
 |-  ( ph -> ( X e. B /\ Y e. B ) )