Step | Hyp | Ref
| Expression |
1 | | invfval.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ Cat) |
2 | | isofval 16240 |
. . . . 5
⊢ (𝐶 ∈ Cat →
(Iso‘𝐶) = ((𝑧 ∈ V ↦ dom 𝑧) ∘ (Inv‘𝐶))) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → (Iso‘𝐶) = ((𝑧 ∈ V ↦ dom 𝑧) ∘ (Inv‘𝐶))) |
4 | | isoval.n |
. . . 4
⊢ 𝐼 = (Iso‘𝐶) |
5 | | invfval.n |
. . . . 5
⊢ 𝑁 = (Inv‘𝐶) |
6 | 5 | coeq2i 5204 |
. . . 4
⊢ ((𝑧 ∈ V ↦ dom 𝑧) ∘ 𝑁) = ((𝑧 ∈ V ↦ dom 𝑧) ∘ (Inv‘𝐶)) |
7 | 3, 4, 6 | 3eqtr4g 2669 |
. . 3
⊢ (𝜑 → 𝐼 = ((𝑧 ∈ V ↦ dom 𝑧) ∘ 𝑁)) |
8 | 7 | oveqd 6566 |
. 2
⊢ (𝜑 → (𝑋𝐼𝑌) = (𝑋((𝑧 ∈ V ↦ dom 𝑧) ∘ 𝑁)𝑌)) |
9 | | eqid 2610 |
. . . . . 6
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥))) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥))) |
10 | | ovex 6577 |
. . . . . . 7
⊢ (𝑥(Sect‘𝐶)𝑦) ∈ V |
11 | 10 | inex1 4727 |
. . . . . 6
⊢ ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥)) ∈ V |
12 | 9, 11 | fnmpt2i 7128 |
. . . . 5
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥))) Fn (𝐵 × 𝐵) |
13 | | invfval.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐶) |
14 | | invfval.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
15 | | invfval.y |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
16 | | eqid 2610 |
. . . . . . 7
⊢
(Sect‘𝐶) =
(Sect‘𝐶) |
17 | 13, 5, 1, 14, 15, 16 | invffval 16241 |
. . . . . 6
⊢ (𝜑 → 𝑁 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥)))) |
18 | 17 | fneq1d 5895 |
. . . . 5
⊢ (𝜑 → (𝑁 Fn (𝐵 × 𝐵) ↔ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥))) Fn (𝐵 × 𝐵))) |
19 | 12, 18 | mpbiri 247 |
. . . 4
⊢ (𝜑 → 𝑁 Fn (𝐵 × 𝐵)) |
20 | | opelxpi 5072 |
. . . . 5
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 〈𝑋, 𝑌〉 ∈ (𝐵 × 𝐵)) |
21 | 14, 15, 20 | syl2anc 691 |
. . . 4
⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ (𝐵 × 𝐵)) |
22 | | fvco2 6183 |
. . . 4
⊢ ((𝑁 Fn (𝐵 × 𝐵) ∧ 〈𝑋, 𝑌〉 ∈ (𝐵 × 𝐵)) → (((𝑧 ∈ V ↦ dom 𝑧) ∘ 𝑁)‘〈𝑋, 𝑌〉) = ((𝑧 ∈ V ↦ dom 𝑧)‘(𝑁‘〈𝑋, 𝑌〉))) |
23 | 19, 21, 22 | syl2anc 691 |
. . 3
⊢ (𝜑 → (((𝑧 ∈ V ↦ dom 𝑧) ∘ 𝑁)‘〈𝑋, 𝑌〉) = ((𝑧 ∈ V ↦ dom 𝑧)‘(𝑁‘〈𝑋, 𝑌〉))) |
24 | | df-ov 6552 |
. . 3
⊢ (𝑋((𝑧 ∈ V ↦ dom 𝑧) ∘ 𝑁)𝑌) = (((𝑧 ∈ V ↦ dom 𝑧) ∘ 𝑁)‘〈𝑋, 𝑌〉) |
25 | | ovex 6577 |
. . . . 5
⊢ (𝑋𝑁𝑌) ∈ V |
26 | | dmeq 5246 |
. . . . . 6
⊢ (𝑧 = (𝑋𝑁𝑌) → dom 𝑧 = dom (𝑋𝑁𝑌)) |
27 | | eqid 2610 |
. . . . . 6
⊢ (𝑧 ∈ V ↦ dom 𝑧) = (𝑧 ∈ V ↦ dom 𝑧) |
28 | 25 | dmex 6991 |
. . . . . 6
⊢ dom
(𝑋𝑁𝑌) ∈ V |
29 | 26, 27, 28 | fvmpt 6191 |
. . . . 5
⊢ ((𝑋𝑁𝑌) ∈ V → ((𝑧 ∈ V ↦ dom 𝑧)‘(𝑋𝑁𝑌)) = dom (𝑋𝑁𝑌)) |
30 | 25, 29 | ax-mp 5 |
. . . 4
⊢ ((𝑧 ∈ V ↦ dom 𝑧)‘(𝑋𝑁𝑌)) = dom (𝑋𝑁𝑌) |
31 | | df-ov 6552 |
. . . . 5
⊢ (𝑋𝑁𝑌) = (𝑁‘〈𝑋, 𝑌〉) |
32 | 31 | fveq2i 6106 |
. . . 4
⊢ ((𝑧 ∈ V ↦ dom 𝑧)‘(𝑋𝑁𝑌)) = ((𝑧 ∈ V ↦ dom 𝑧)‘(𝑁‘〈𝑋, 𝑌〉)) |
33 | 30, 32 | eqtr3i 2634 |
. . 3
⊢ dom
(𝑋𝑁𝑌) = ((𝑧 ∈ V ↦ dom 𝑧)‘(𝑁‘〈𝑋, 𝑌〉)) |
34 | 23, 24, 33 | 3eqtr4g 2669 |
. 2
⊢ (𝜑 → (𝑋((𝑧 ∈ V ↦ dom 𝑧) ∘ 𝑁)𝑌) = dom (𝑋𝑁𝑌)) |
35 | 8, 34 | eqtrd 2644 |
1
⊢ (𝜑 → (𝑋𝐼𝑌) = dom (𝑋𝑁𝑌)) |