invsym2

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

Step	Hyp	Ref	Expression
1		invfval.b	$⊢ B = {Base}_{C}$
2		invfval.n	$⊢ N = Inv (C)$
3		invfval.c	$⊢ φ \to C \in Cat$
4		invfval.x	$⊢ φ \to X \in B$
5		invfval.y	$⊢ φ \to Y \in B$
6		eqid	$⊢ Hom (C) = Hom (C)$
7	1 2 3 5 4 6	invss	$⊢ φ \to Y N X \subseteq (Y Hom (C) X) \times (X Hom (C) Y)$
8		relxp	$⊢ Rel ((Y Hom (C) X) \times (X Hom (C) Y))$
9		relss	$⊢ Y N X \subseteq (Y Hom (C) X) \times (X Hom (C) Y) \to (Rel ((Y Hom (C) X) \times (X Hom (C) Y)) \to Rel (Y N X))$
10	7 8 9	mpisyl	$⊢ φ \to Rel (Y N X)$
11		relcnv	$⊢ Rel {(X N Y)}^{-1}$
12	10 11	jctil	$⊢ φ \to (Rel {(X N Y)}^{-1} \land Rel (Y N X))$
13	1 2 3 4 5	invsym	$⊢ φ \to (f (X N Y) g \leftrightarrow g (Y N X) f)$
14		vex	$⊢ g \in V$
15		vex	$⊢ f \in V$
16	14 15	brcnv	$⊢ g {(X N Y)}^{-1} f \leftrightarrow f (X N Y) g$
17		df-br	$⊢ g {(X N Y)}^{-1} f \leftrightarrow ⟨g, f⟩ \in {(X N Y)}^{-1}$
18	16 17	bitr3i	$⊢ f (X N Y) g \leftrightarrow ⟨g, f⟩ \in {(X N Y)}^{-1}$
19		df-br	$⊢ g (Y N X) f \leftrightarrow ⟨g, f⟩ \in (Y N X)$
20	13 18 19	3bitr3g	$⊢ φ \to (⟨g, f⟩ \in {(X N Y)}^{-1} \leftrightarrow ⟨g, f⟩ \in (Y N X))$
21	20	eqrelrdv2	$⊢ ((Rel {(X N Y)}^{-1} \land Rel (Y N X)) \land φ) \to {(X N Y)}^{-1} = Y N X$
22	12 21	mpancom	$⊢ φ \to {(X N Y)}^{-1} = Y N X$

Metamath Proof Explorer