Theorem invsym2

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

	Ref	Expression
Hypotheses	invfval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	invfval.n	⊢ 𝑁 = ( Inv ‘ 𝐶 )
	invfval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	invss.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	invss.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	invsym2	⊢ ( 𝜑 → ◡ ( 𝑋 𝑁 𝑌 ) = ( 𝑌 𝑁 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		invfval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		invfval.n	⊢ 𝑁 = ( Inv ‘ 𝐶 )
3		invfval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		invss.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		invss.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
7	1 2 3 5 4 6	invss	⊢ ( 𝜑 → ( 𝑌 𝑁 𝑋 ) ⊆ ( ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) × ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) )
8		relxp	⊢ Rel ( ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) × ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
9		relss	⊢ ( ( 𝑌 𝑁 𝑋 ) ⊆ ( ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) × ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) → ( Rel ( ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) × ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ) → Rel ( 𝑌 𝑁 𝑋 ) ) )
10	7 8 9	mpisyl	⊢ ( 𝜑 → Rel ( 𝑌 𝑁 𝑋 ) )
11		relcnv	⊢ Rel ◡ ( 𝑋 𝑁 𝑌 )
12	10 11	jctil	⊢ ( 𝜑 → ( Rel ◡ ( 𝑋 𝑁 𝑌 ) ∧ Rel ( 𝑌 𝑁 𝑋 ) ) )
13	1 2 3 4 5	invsym	⊢ ( 𝜑 → ( 𝑓 ( 𝑋 𝑁 𝑌 ) 𝑔 ↔ 𝑔 ( 𝑌 𝑁 𝑋 ) 𝑓 ) )
14		vex	⊢ 𝑔 ∈ V
15		vex	⊢ 𝑓 ∈ V
16	14 15	brcnv	⊢ ( 𝑔 ◡ ( 𝑋 𝑁 𝑌 ) 𝑓 ↔ 𝑓 ( 𝑋 𝑁 𝑌 ) 𝑔 )
17		df-br	⊢ ( 𝑔 ◡ ( 𝑋 𝑁 𝑌 ) 𝑓 ↔ ⟨ 𝑔 , 𝑓 ⟩ ∈ ◡ ( 𝑋 𝑁 𝑌 ) )
18	16 17	bitr3i	⊢ ( 𝑓 ( 𝑋 𝑁 𝑌 ) 𝑔 ↔ ⟨ 𝑔 , 𝑓 ⟩ ∈ ◡ ( 𝑋 𝑁 𝑌 ) )
19		df-br	⊢ ( 𝑔 ( 𝑌 𝑁 𝑋 ) 𝑓 ↔ ⟨ 𝑔 , 𝑓 ⟩ ∈ ( 𝑌 𝑁 𝑋 ) )
20	13 18 19	3bitr3g	⊢ ( 𝜑 → ( ⟨ 𝑔 , 𝑓 ⟩ ∈ ◡ ( 𝑋 𝑁 𝑌 ) ↔ ⟨ 𝑔 , 𝑓 ⟩ ∈ ( 𝑌 𝑁 𝑋 ) ) )
21	20	eqrelrdv2	⊢ ( ( ( Rel ◡ ( 𝑋 𝑁 𝑌 ) ∧ Rel ( 𝑌 𝑁 𝑋 ) ) ∧ 𝜑 ) → ◡ ( 𝑋 𝑁 𝑌 ) = ( 𝑌 𝑁 𝑋 ) )
22	12 21	mpancom	⊢ ( 𝜑 → ◡ ( 𝑋 𝑁 𝑌 ) = ( 𝑌 𝑁 𝑋 ) )