Metamath Proof Explorer

Theorem invffval

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 invffval ( 𝜑 → 𝑁 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝑆 𝑦 ) ∩ ◡ ( 𝑦 𝑆 𝑥 ) ) ) )

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 fveq2 ⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = ( Base ‘ 𝐶 ) )
8 7 1 eqtr4di ⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = 𝐵 )
9 fveq2 ⊢ ( 𝑐 = 𝐶 → ( Sect ‘ 𝑐 ) = ( Sect ‘ 𝐶 ) )
10 9 6 eqtr4di ⊢ ( 𝑐 = 𝐶 → ( Sect ‘ 𝑐 ) = 𝑆 )
11 10 oveqd ⊢ ( 𝑐 = 𝐶 → ( 𝑥 ( Sect ‘ 𝑐 ) 𝑦 ) = ( 𝑥 𝑆 𝑦 ) )
12 10 oveqd ⊢ ( 𝑐 = 𝐶 → ( 𝑦 ( Sect ‘ 𝑐 ) 𝑥 ) = ( 𝑦 𝑆 𝑥 ) )
13 12 cnveqd ⊢ ( 𝑐 = 𝐶 → ◡ ( 𝑦 ( Sect ‘ 𝑐 ) 𝑥 ) = ◡ ( 𝑦 𝑆 𝑥 ) )
14 11 13 ineq12d ⊢ ( 𝑐 = 𝐶 → ( ( 𝑥 ( Sect ‘ 𝑐 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝑐 ) 𝑥 ) ) = ( ( 𝑥 𝑆 𝑦 ) ∩ ◡ ( 𝑦 𝑆 𝑥 ) ) )
15 8 8 14 mpoeq123dv ⊢ ( 𝑐 = 𝐶 → ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 𝑥 ( Sect ‘ 𝑐 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝑐 ) 𝑥 ) ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝑆 𝑦 ) ∩ ◡ ( 𝑦 𝑆 𝑥 ) ) ) )
16 df-inv ⊢ Inv = ( 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 𝑥 ( Sect ‘ 𝑐 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝑐 ) 𝑥 ) ) ) )
17 1 fvexi ⊢ 𝐵 ∈ V
18 17 17 mpoex ⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝑆 𝑦 ) ∩ ◡ ( 𝑦 𝑆 𝑥 ) ) ) ∈ V
19 15 16 18 fvmpt ⊢ ( 𝐶 ∈ Cat → ( Inv ‘ 𝐶 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝑆 𝑦 ) ∩ ◡ ( 𝑦 𝑆 𝑥 ) ) ) )
20 3 19 syl ⊢ ( 𝜑 → ( Inv ‘ 𝐶 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝑆 𝑦 ) ∩ ◡ ( 𝑦 𝑆 𝑥 ) ) ) )
21 2 20 eqtrid ⊢ ( 𝜑 → 𝑁 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝑆 𝑦 ) ∩ ◡ ( 𝑦 𝑆 𝑥 ) ) ) )