Theorem invfval

Description: Value of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017)

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

Proof

Step	Hyp	Ref	Expression
1		invfval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		invfval.n	⊢ 𝑁 = ( Inv ‘ 𝐶 )
3		invfval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		invfval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		invfval.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6		invfval.s	⊢ 𝑆 = ( Sect ‘ 𝐶 )
7	1 2 3 4 4 6	invffval	⊢ ( 𝜑 → 𝑁 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝑆 𝑦 ) ∩ ◡ ( 𝑦 𝑆 𝑥 ) ) ) )
8		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → 𝑥 = 𝑋 )
9		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → 𝑦 = 𝑌 )
10	8 9	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝑥 𝑆 𝑦 ) = ( 𝑋 𝑆 𝑌 ) )
11	9 8	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝑦 𝑆 𝑥 ) = ( 𝑌 𝑆 𝑋 ) )
12	11	cnveqd	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ◡ ( 𝑦 𝑆 𝑥 ) = ◡ ( 𝑌 𝑆 𝑋 ) )
13	10 12	ineq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( ( 𝑥 𝑆 𝑦 ) ∩ ◡ ( 𝑦 𝑆 𝑥 ) ) = ( ( 𝑋 𝑆 𝑌 ) ∩ ◡ ( 𝑌 𝑆 𝑋 ) ) )
14		ovex	⊢ ( 𝑋 𝑆 𝑌 ) ∈ V
15	14	inex1	⊢ ( ( 𝑋 𝑆 𝑌 ) ∩ ◡ ( 𝑌 𝑆 𝑋 ) ) ∈ V
16	15	a1i	⊢ ( 𝜑 → ( ( 𝑋 𝑆 𝑌 ) ∩ ◡ ( 𝑌 𝑆 𝑋 ) ) ∈ V )
17	7 13 4 5 16	ovmpod	⊢ ( 𝜑 → ( 𝑋 𝑁 𝑌 ) = ( ( 𝑋 𝑆 𝑌 ) ∩ ◡ ( 𝑌 𝑆 𝑋 ) ) )