| Step | Hyp | Ref
| Expression |
| 1 | | invfval.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ Cat) |
| 2 | | isofval 17801 |
. . . . 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 5871 |
. . . 4
⊢ ((𝑧 ∈ V ↦ dom 𝑧) ∘ 𝑁) = ((𝑧 ∈ V ↦ dom 𝑧) ∘ (Inv‘𝐶)) |
| 7 | 3, 4, 6 | 3eqtr4g 2802 |
. . 3
⊢ (𝜑 → 𝐼 = ((𝑧 ∈ V ↦ dom 𝑧) ∘ 𝑁)) |
| 8 | 7 | oveqd 7448 |
. 2
⊢ (𝜑 → (𝑋𝐼𝑌) = (𝑋((𝑧 ∈ V ↦ dom 𝑧) ∘ 𝑁)𝑌)) |
| 9 | | eqid 2737 |
. . . . . 6
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥))) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥))) |
| 10 | | ovex 7464 |
. . . . . . 7
⊢ (𝑥(Sect‘𝐶)𝑦) ∈ V |
| 11 | 10 | inex1 5317 |
. . . . . 6
⊢ ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥)) ∈ V |
| 12 | 9, 11 | fnmpoi 8095 |
. . . . 5
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥))) Fn (𝐵 × 𝐵) |
| 13 | | invfval.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐶) |
| 14 | | invfval.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
| 15 | | invfval.y |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
| 16 | | eqid 2737 |
. . . . . . 7
⊢
(Sect‘𝐶) =
(Sect‘𝐶) |
| 17 | 13, 5, 1, 14, 15, 16 | invffval 17802 |
. . . . . 6
⊢ (𝜑 → 𝑁 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥)))) |
| 18 | 17 | fneq1d 6661 |
. . . . 5
⊢ (𝜑 → (𝑁 Fn (𝐵 × 𝐵) ↔ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ ◡(𝑦(Sect‘𝐶)𝑥))) Fn (𝐵 × 𝐵))) |
| 19 | 12, 18 | mpbiri 258 |
. . . 4
⊢ (𝜑 → 𝑁 Fn (𝐵 × 𝐵)) |
| 20 | 14, 15 | opelxpd 5724 |
. . . 4
⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ (𝐵 × 𝐵)) |
| 21 | | fvco2 7006 |
. . . 4
⊢ ((𝑁 Fn (𝐵 × 𝐵) ∧ 〈𝑋, 𝑌〉 ∈ (𝐵 × 𝐵)) → (((𝑧 ∈ V ↦ dom 𝑧) ∘ 𝑁)‘〈𝑋, 𝑌〉) = ((𝑧 ∈ V ↦ dom 𝑧)‘(𝑁‘〈𝑋, 𝑌〉))) |
| 22 | 19, 20, 21 | syl2anc 584 |
. . 3
⊢ (𝜑 → (((𝑧 ∈ V ↦ dom 𝑧) ∘ 𝑁)‘〈𝑋, 𝑌〉) = ((𝑧 ∈ V ↦ dom 𝑧)‘(𝑁‘〈𝑋, 𝑌〉))) |
| 23 | | df-ov 7434 |
. . 3
⊢ (𝑋((𝑧 ∈ V ↦ dom 𝑧) ∘ 𝑁)𝑌) = (((𝑧 ∈ V ↦ dom 𝑧) ∘ 𝑁)‘〈𝑋, 𝑌〉) |
| 24 | | ovex 7464 |
. . . . 5
⊢ (𝑋𝑁𝑌) ∈ V |
| 25 | | dmeq 5914 |
. . . . . 6
⊢ (𝑧 = (𝑋𝑁𝑌) → dom 𝑧 = dom (𝑋𝑁𝑌)) |
| 26 | | eqid 2737 |
. . . . . 6
⊢ (𝑧 ∈ V ↦ dom 𝑧) = (𝑧 ∈ V ↦ dom 𝑧) |
| 27 | 24 | dmex 7931 |
. . . . . 6
⊢ dom
(𝑋𝑁𝑌) ∈ V |
| 28 | 25, 26, 27 | fvmpt 7016 |
. . . . 5
⊢ ((𝑋𝑁𝑌) ∈ V → ((𝑧 ∈ V ↦ dom 𝑧)‘(𝑋𝑁𝑌)) = dom (𝑋𝑁𝑌)) |
| 29 | 24, 28 | ax-mp 5 |
. . . 4
⊢ ((𝑧 ∈ V ↦ dom 𝑧)‘(𝑋𝑁𝑌)) = dom (𝑋𝑁𝑌) |
| 30 | | df-ov 7434 |
. . . . 5
⊢ (𝑋𝑁𝑌) = (𝑁‘〈𝑋, 𝑌〉) |
| 31 | 30 | fveq2i 6909 |
. . . 4
⊢ ((𝑧 ∈ V ↦ dom 𝑧)‘(𝑋𝑁𝑌)) = ((𝑧 ∈ V ↦ dom 𝑧)‘(𝑁‘〈𝑋, 𝑌〉)) |
| 32 | 29, 31 | eqtr3i 2767 |
. . 3
⊢ dom
(𝑋𝑁𝑌) = ((𝑧 ∈ V ↦ dom 𝑧)‘(𝑁‘〈𝑋, 𝑌〉)) |
| 33 | 22, 23, 32 | 3eqtr4g 2802 |
. 2
⊢ (𝜑 → (𝑋((𝑧 ∈ V ↦ dom 𝑧) ∘ 𝑁)𝑌) = dom (𝑋𝑁𝑌)) |
| 34 | 8, 33 | eqtrd 2777 |
1
⊢ (𝜑 → (𝑋𝐼𝑌) = dom (𝑋𝑁𝑌)) |