Theorem invsym

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	invsym	⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ↔ 𝐺 ( 𝑌 𝑁 𝑋 ) 𝐹 ) )

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	⊢ ( Sect ‘ 𝐶 ) = ( Sect ‘ 𝐶 )
7	1 2 3 4 5 6	isinv	⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ↔ ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐺 ∧ 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ) ) )
8	7	biancomd	⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ↔ ( 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ∧ 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐺 ) ) )
9	1 2 3 5 4 6	isinv	⊢ ( 𝜑 → ( 𝐺 ( 𝑌 𝑁 𝑋 ) 𝐹 ↔ ( 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ∧ 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐺 ) ) )
10	8 9	bitr4d	⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ↔ 𝐺 ( 𝑌 𝑁 𝑋 ) 𝐹 ) )