Metamath Proof Explorer

Theorem invsym2

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
invfval.x ⊢ φ → X ∈ B
invfval.y ⊢ φ → Y ∈ B
Assertion invsym2 ⊢ φ → X N Y -1 = Y N X

Proof

Step Hyp Ref Expression
1 invfval.b ⊢ B = Base C
2 invfval.n ⊢ N = Inv ⁡ C
3 invfval.c ⊢ φ → C ∈ Cat
4 invfval.x ⊢ φ → X ∈ B
5 invfval.y ⊢ φ → Y ∈ B
6 eqid ⊢ Hom ⁡ C = Hom ⁡ C
7 1 2 3 5 4 6 invss ⊢ φ → Y N X ⊆ Y Hom ⁡ C X × X Hom ⁡ C Y
8 relxp ⊢ Rel ⁡ Y Hom ⁡ C X × X Hom ⁡ C Y
9 relss ⊢ Y N X ⊆ Y Hom ⁡ C X × X Hom ⁡ C Y → Rel ⁡ Y Hom ⁡ C X × X Hom ⁡ C Y → Rel ⁡ Y N X
10 7 8 9 mpisyl ⊢ φ → Rel ⁡ Y N X
11 relcnv ⊢ Rel ⁡ X N Y -1
12 10 11 jctil ⊢ φ → Rel ⁡ X N Y -1 ∧ Rel ⁡ Y N X
13 1 2 3 4 5 invsym ⊢ φ → f X N Y g ↔ g Y N X f
14 vex ⊢ g ∈ V
15 vex ⊢ f ∈ V
16 14 15 brcnv ⊢ g X N Y -1 f ↔ f X N Y g
17 df-br ⊢ g X N Y -1 f ↔ g f ∈ X N Y -1
18 16 17 bitr3i ⊢ f X N Y g ↔ g f ∈ X N Y -1
19 df-br ⊢ g Y N X f ↔ g f ∈ Y N X
20 13 18 19 3bitr3g ⊢ φ → g f ∈ X N Y -1 ↔ g f ∈ Y N X
21 20 eqrelrdv2 ⊢ Rel ⁡ X N Y -1 ∧ Rel ⁡ Y N X ∧ φ → X N Y -1 = Y N X
22 12 21 mpancom ⊢ φ → X N Y -1 = Y N X