Metamath Proof Explorer

Theorem isinv2

Description: The property " F is an inverse of G ". (Contributed by Zhi Wang, 14-Nov-2025)

Ref Expression
Hypotheses isinv2.n 
|- N = ( Inv ` C )
isinv2.s 
|- S = ( Sect ` C )
Assertion isinv2 
|- ( F ( X N Y ) G <-> ( F ( X S Y ) G /\ G ( Y S X ) F ) )

Proof

Step Hyp Ref Expression
1 isinv2.n 
 |-  N = ( Inv ` C )
2 isinv2.s 
 |-  S = ( Sect ` C )
3 id 
 |-  ( F ( X N Y ) G -> F ( X N Y ) G )
4 1 3 invrcl 
 |-  ( F ( X N Y ) G -> C e. Cat )
5 eqid 
 |-  ( Base ` C ) = ( Base ` C )
6 1 3 5 invrcl2 
 |-  ( F ( X N Y ) G -> ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) ) )
7 4 6 jca 
 |-  ( F ( X N Y ) G -> ( C e. Cat /\ ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) ) ) )
8 simpl 
 |-  ( ( F ( X S Y ) G /\ G ( Y S X ) F ) -> F ( X S Y ) G )
9 2 8 sectrcl 
 |-  ( ( F ( X S Y ) G /\ G ( Y S X ) F ) -> C e. Cat )
10 2 8 5 sectrcl2 
 |-  ( ( F ( X S Y ) G /\ G ( Y S X ) F ) -> ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) ) )
11 9 10 jca 
 |-  ( ( F ( X S Y ) G /\ G ( Y S X ) F ) -> ( C e. Cat /\ ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) ) ) )
12 simpl 
 |-  ( ( C e. Cat /\ ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) ) ) -> C e. Cat )
13 simprl 
 |-  ( ( C e. Cat /\ ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) ) ) -> X e. ( Base ` C ) )
14 simprr 
 |-  ( ( C e. Cat /\ ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) ) ) -> Y e. ( Base ` C ) )
15 5 1 12 13 14 2 isinv 
 |-  ( ( C e. Cat /\ ( X e. ( Base ` C ) /\ Y e. ( Base ` C ) ) ) -> ( F ( X N Y ) G <-> ( F ( X S Y ) G /\ G ( Y S X ) F ) ) )
16 7 11 15 pm5.21nii 
 |-  ( F ( X N Y ) G <-> ( F ( X S Y ) G /\ G ( Y S X ) F ) )