This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem invsym

Description: The inverse relation is symmetric. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses invfval.b ⊢ B = Base C
invfval.n ⊢ N = Inv ⁡ C
invfval.c ⊢ φ → C ∈ Cat
invss.x ⊢ φ → X ∈ B
invss.y ⊢ φ → Y ∈ B
Assertion invsym ⊢ φ → F X N Y G ↔ G Y N X F

Proof

Step Hyp Ref Expression
1 invfval.b ⊢ B = Base C
2 invfval.n ⊢ N = Inv ⁡ C
3 invfval.c ⊢ φ → C ∈ Cat
4 invss.x ⊢ φ → X ∈ B
5 invss.y ⊢ φ → Y ∈ B
6 eqid ⊢ Sect ⁡ C = Sect ⁡ C
7 1 2 3 4 5 6 isinv ⊢ φ → F X N Y G ↔ F X Sect ⁡ C Y G ∧ G Y Sect ⁡ C X F
8 7 biancomd ⊢ φ → F X N Y G ↔ G Y Sect ⁡ C X F ∧ F X Sect ⁡ C Y G
9 1 2 3 5 4 6 isinv ⊢ φ → G Y N X F ↔ G Y Sect ⁡ C X F ∧ F X Sect ⁡ C Y G
10 8 9 bitr4d ⊢ φ → F X N Y G ↔ G Y N X F