This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem invffval

Description: Value of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017) Removed redundant hypotheses. (Revised by Zhi Wang, 27-Oct-2025)

		Ref	Expression
	Hypotheses	invfval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
		invfval.n	⊢ 𝑁 = ( Inv ‘ 𝐶 )
		invfval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
		invffval.s	⊢ 𝑆 = ( Sect ‘ 𝐶 )
	Assertion	invffval	⊢ ( 𝜑 → 𝑁 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝑆 𝑦 ) ∩ ^◡ ( 𝑦 𝑆 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		invfval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		invfval.n	⊢ 𝑁 = ( Inv ‘ 𝐶 )
3		invfval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		invffval.s	⊢ 𝑆 = ( Sect ‘ 𝐶 )
5		fveq2	⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = ( Base ‘ 𝐶 ) )
6	5 1	eqtr4di	⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = 𝐵 )
7		fveq2	⊢ ( 𝑐 = 𝐶 → ( Sect ‘ 𝑐 ) = ( Sect ‘ 𝐶 ) )
8	7 4	eqtr4di	⊢ ( 𝑐 = 𝐶 → ( Sect ‘ 𝑐 ) = 𝑆 )
9	8	oveqd	⊢ ( 𝑐 = 𝐶 → ( 𝑥 ( Sect ‘ 𝑐 ) 𝑦 ) = ( 𝑥 𝑆 𝑦 ) )
10	8	oveqd	⊢ ( 𝑐 = 𝐶 → ( 𝑦 ( Sect ‘ 𝑐 ) 𝑥 ) = ( 𝑦 𝑆 𝑥 ) )
11	10	cnveqd	⊢ ( 𝑐 = 𝐶 → ^◡ ( 𝑦 ( Sect ‘ 𝑐 ) 𝑥 ) = ^◡ ( 𝑦 𝑆 𝑥 ) )
12	9 11	ineq12d	⊢ ( 𝑐 = 𝐶 → ( ( 𝑥 ( Sect ‘ 𝑐 ) 𝑦 ) ∩ ^◡ ( 𝑦 ( Sect ‘ 𝑐 ) 𝑥 ) ) = ( ( 𝑥 𝑆 𝑦 ) ∩ ^◡ ( 𝑦 𝑆 𝑥 ) ) )
13	6 6 12	mpoeq123dv	⊢ ( 𝑐 = 𝐶 → ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 𝑥 ( Sect ‘ 𝑐 ) 𝑦 ) ∩ ^◡ ( 𝑦 ( Sect ‘ 𝑐 ) 𝑥 ) ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝑆 𝑦 ) ∩ ^◡ ( 𝑦 𝑆 𝑥 ) ) ) )
14		df-inv	⊢ Inv = ( 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 𝑥 ( Sect ‘ 𝑐 ) 𝑦 ) ∩ ^◡ ( 𝑦 ( Sect ‘ 𝑐 ) 𝑥 ) ) ) )
15	1	fvexi	⊢ 𝐵 ∈ V
16	15 15	mpoex	⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝑆 𝑦 ) ∩ ^◡ ( 𝑦 𝑆 𝑥 ) ) ) ∈ V
17	13 14 16	fvmpt	⊢ ( 𝐶 ∈ Cat → ( Inv ‘ 𝐶 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝑆 𝑦 ) ∩ ^◡ ( 𝑦 𝑆 𝑥 ) ) ) )
18	3 17	syl	⊢ ( 𝜑 → ( Inv ‘ 𝐶 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝑆 𝑦 ) ∩ ^◡ ( 𝑦 𝑆 𝑥 ) ) ) )
19	2 18	eqtrid	⊢ ( 𝜑 → 𝑁 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝑆 𝑦 ) ∩ ^◡ ( 𝑦 𝑆 𝑥 ) ) ) )