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	|- ( ph -> C e. Cat )
	invfval.x	|- ( ph -> X e. B )
	invfval.y	|- ( ph -> Y e. B )
Assertion	invsym2	|- ( ph -> `' ( X N Y ) = ( Y N X ) )

Proof

Step	Hyp	Ref	Expression
1		invfval.b	|- B = ( Base ` C )
2		invfval.n	|- N = ( Inv ` C )
3		invfval.c	|- ( ph -> C e. Cat )
4		invfval.x	|- ( ph -> X e. B )
5		invfval.y	|- ( ph -> Y e. B )
6		eqid	|- ( Hom ` C ) = ( Hom ` C )
7	1 2 3 5 4 6	invss	|- ( ph -> ( Y N X ) C_ ( ( Y ( Hom ` C ) X ) X. ( X ( Hom ` C ) Y ) ) )
8		relxp	|- Rel ( ( Y ( Hom ` C ) X ) X. ( X ( Hom ` C ) Y ) )
9		relss	|- ( ( Y N X ) C_ ( ( Y ( Hom ` C ) X ) X. ( X ( Hom ` C ) Y ) ) -> ( Rel ( ( Y ( Hom ` C ) X ) X. ( X ( Hom ` C ) Y ) ) -> Rel ( Y N X ) ) )
10	7 8 9	mpisyl	|- ( ph -> Rel ( Y N X ) )
11		relcnv	|- Rel `' ( X N Y )
12	10 11	jctil	|- ( ph -> ( Rel `' ( X N Y ) /\ Rel ( Y N X ) ) )
13	1 2 3 4 5	invsym	|- ( ph -> ( f ( X N Y ) g <-> g ( Y N X ) f ) )
14		vex	|- g e. _V
15		vex	|- f e. _V
16	14 15	brcnv	|- ( g `' ( X N Y ) f <-> f ( X N Y ) g )
17		df-br	|- ( g `' ( X N Y ) f <-> <. g , f >. e. `' ( X N Y ) )
18	16 17	bitr3i	|- ( f ( X N Y ) g <-> <. g , f >. e. `' ( X N Y ) )
19		df-br	|- ( g ( Y N X ) f <-> <. g , f >. e. ( Y N X ) )
20	13 18 19	3bitr3g	|- ( ph -> ( <. g , f >. e. `' ( X N Y ) <-> <. g , f >. e. ( Y N X ) ) )
21	20	eqrelrdv2	|- ( ( ( Rel `' ( X N Y ) /\ Rel ( Y N X ) ) /\ ph ) -> `' ( X N Y ) = ( Y N X ) )
22	12 21	mpancom	|- ( ph -> `' ( X N Y ) = ( Y N X ) )