Metamath Proof Explorer

Theorem invffval

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

Ref Expression
Hypotheses invfval.b ⊢ B = Base C
invfval.n ⊢ N = Inv ⁡ C
invfval.c ⊢ φ → C ∈ Cat
invfval.x ⊢ φ → X ∈ B
invfval.y ⊢ φ → Y ∈ B
invfval.s ⊢ S = Sect ⁡ C
Assertion invffval ⊢ φ → N = x ∈ B , y ∈ B ⟼ x S y ∩ y S x -1

Proof

Step Hyp Ref Expression
1 invfval.b ⊢ B = Base C
2 invfval.n ⊢ N = Inv ⁡ C
3 invfval.c ⊢ φ → C ∈ Cat
4 invfval.x ⊢ φ → X ∈ B
5 invfval.y ⊢ φ → Y ∈ B
6 invfval.s ⊢ S = Sect ⁡ C
7 fveq2 ⊢ c = C → Base c = Base C
8 7 1 eqtr4di ⊢ c = C → Base c = B
9 fveq2 ⊢ c = C → Sect ⁡ c = Sect ⁡ C
10 9 6 eqtr4di ⊢ c = C → Sect ⁡ c = S
11 10 oveqd ⊢ c = C → x Sect ⁡ c y = x S y
12 10 oveqd ⊢ c = C → y Sect ⁡ c x = y S x
13 12 cnveqd ⊢ c = C → y Sect ⁡ c x -1 = y S x -1
14 11 13 ineq12d ⊢ c = C → x Sect ⁡ c y ∩ y Sect ⁡ c x -1 = x S y ∩ y S x -1
15 8 8 14 mpoeq123dv ⊢ c = C → x ∈ Base c , y ∈ Base c ⟼ x Sect ⁡ c y ∩ y Sect ⁡ c x -1 = x ∈ B , y ∈ B ⟼ x S y ∩ y S x -1
16 df-inv ⊢ Inv = c ∈ Cat ⟼ x ∈ Base c , y ∈ Base c ⟼ x Sect ⁡ c y ∩ y Sect ⁡ c x -1
17 1 fvexi ⊢ B ∈ V
18 17 17 mpoex ⊢ x ∈ B , y ∈ B ⟼ x S y ∩ y S x -1 ∈ V
19 15 16 18 fvmpt ⊢ C ∈ Cat → Inv ⁡ C = x ∈ B , y ∈ B ⟼ x S y ∩ y S x -1
20 3 19 syl ⊢ φ → Inv ⁡ C = x ∈ B , y ∈ B ⟼ x S y ∩ y S x -1
21 2 20 eqtrid ⊢ φ → N = x ∈ B , y ∈ B ⟼ x S y ∩ y S x -1