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 ∈ Cat
5 eqid ⊢ Base C = Base C
6 1 3 5 invrcl2 ⊢ F X N Y G → X ∈ Base C ∧ Y ∈ Base C
7 4 6 jca ⊢ F X N Y G → C ∈ Cat ∧ X ∈ Base C ∧ Y ∈ 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 ∈ Cat
10 2 8 5 sectrcl2 ⊢ F X S Y G ∧ G Y S X F → X ∈ Base C ∧ Y ∈ Base C
11 9 10 jca ⊢ F X S Y G ∧ G Y S X F → C ∈ Cat ∧ X ∈ Base C ∧ Y ∈ Base C
12 simpl ⊢ C ∈ Cat ∧ X ∈ Base C ∧ Y ∈ Base C → C ∈ Cat
13 simprl ⊢ C ∈ Cat ∧ X ∈ Base C ∧ Y ∈ Base C → X ∈ Base C
14 simprr ⊢ C ∈ Cat ∧ X ∈ Base C ∧ Y ∈ Base C → Y ∈ Base C
15 5 1 12 13 14 2 isinv ⊢ C ∈ Cat ∧ X ∈ Base C ∧ Y ∈ 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