Mathbox for Richard Penner |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > neicvgnvo | Structured version Visualization version GIF version |
Description: If neighborhood and convergent functions are related by operator 𝐻, it is its own converse function. (Contributed by RP, 11-Jun-2021.) |
Ref | Expression |
---|---|
neicvg.o | ⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)}))) |
neicvg.p | ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜)))))) |
neicvg.d | ⊢ 𝐷 = (𝑃‘𝐵) |
neicvg.f | ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵) |
neicvg.g | ⊢ 𝐺 = (𝐵𝑂𝒫 𝐵) |
neicvg.h | ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺)) |
neicvg.r | ⊢ (𝜑 → 𝑁𝐻𝑀) |
Ref | Expression |
---|---|
neicvgnvo | ⊢ (𝜑 → ◡𝐻 = 𝐻) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neicvg.h | . . . . 5 ⊢ 𝐻 = (𝐹 ∘ (𝐷 ∘ 𝐺)) | |
2 | 1 | cnveqi 5816 | . . . 4 ⊢ ◡𝐻 = ◡(𝐹 ∘ (𝐷 ∘ 𝐺)) |
3 | cnvco 5827 | . . . 4 ⊢ ◡(𝐹 ∘ (𝐷 ∘ 𝐺)) = (◡(𝐷 ∘ 𝐺) ∘ ◡𝐹) | |
4 | cnvco 5827 | . . . . 5 ⊢ ◡(𝐷 ∘ 𝐺) = (◡𝐺 ∘ ◡𝐷) | |
5 | 4 | coeq1i 5801 | . . . 4 ⊢ (◡(𝐷 ∘ 𝐺) ∘ ◡𝐹) = ((◡𝐺 ∘ ◡𝐷) ∘ ◡𝐹) |
6 | 2, 3, 5 | 3eqtri 2768 | . . 3 ⊢ ◡𝐻 = ((◡𝐺 ∘ ◡𝐷) ∘ ◡𝐹) |
7 | neicvg.o | . . . . . 6 ⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)}))) | |
8 | neicvg.d | . . . . . . 7 ⊢ 𝐷 = (𝑃‘𝐵) | |
9 | neicvg.r | . . . . . . 7 ⊢ (𝜑 → 𝑁𝐻𝑀) | |
10 | 8, 1, 9 | neicvgbex 42051 | . . . . . 6 ⊢ (𝜑 → 𝐵 ∈ V) |
11 | 10 | pwexd 5322 | . . . . . 6 ⊢ (𝜑 → 𝒫 𝐵 ∈ V) |
12 | neicvg.g | . . . . . 6 ⊢ 𝐺 = (𝐵𝑂𝒫 𝐵) | |
13 | neicvg.f | . . . . . 6 ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵) | |
14 | 7, 10, 11, 12, 13 | fsovcnvd 41951 | . . . . 5 ⊢ (𝜑 → ◡𝐺 = 𝐹) |
15 | neicvg.p | . . . . . 6 ⊢ 𝑃 = (𝑛 ∈ V ↦ (𝑝 ∈ (𝒫 𝑛 ↑m 𝒫 𝑛) ↦ (𝑜 ∈ 𝒫 𝑛 ↦ (𝑛 ∖ (𝑝‘(𝑛 ∖ 𝑜)))))) | |
16 | 15, 8, 10 | dssmapnvod 41957 | . . . . 5 ⊢ (𝜑 → ◡𝐷 = 𝐷) |
17 | 14, 16 | coeq12d 5806 | . . . 4 ⊢ (𝜑 → (◡𝐺 ∘ ◡𝐷) = (𝐹 ∘ 𝐷)) |
18 | 7, 11, 10, 13, 12 | fsovcnvd 41951 | . . . 4 ⊢ (𝜑 → ◡𝐹 = 𝐺) |
19 | 17, 18 | coeq12d 5806 | . . 3 ⊢ (𝜑 → ((◡𝐺 ∘ ◡𝐷) ∘ ◡𝐹) = ((𝐹 ∘ 𝐷) ∘ 𝐺)) |
20 | 6, 19 | eqtrid 2788 | . 2 ⊢ (𝜑 → ◡𝐻 = ((𝐹 ∘ 𝐷) ∘ 𝐺)) |
21 | coass 6203 | . . 3 ⊢ ((𝐹 ∘ 𝐷) ∘ 𝐺) = (𝐹 ∘ (𝐷 ∘ 𝐺)) | |
22 | 21, 1 | eqtr4i 2767 | . 2 ⊢ ((𝐹 ∘ 𝐷) ∘ 𝐺) = 𝐻 |
23 | 20, 22 | eqtrdi 2792 | 1 ⊢ (𝜑 → ◡𝐻 = 𝐻) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2105 {crab 3403 Vcvv 3441 ∖ cdif 3895 𝒫 cpw 4547 class class class wbr 5092 ↦ cmpt 5175 ◡ccnv 5619 ∘ ccom 5624 ‘cfv 6479 (class class class)co 7337 ∈ cmpo 7339 ↑m cmap 8686 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2707 ax-rep 5229 ax-sep 5243 ax-nul 5250 ax-pow 5308 ax-pr 5372 ax-un 7650 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2886 df-ne 2941 df-ral 3062 df-rex 3071 df-reu 3350 df-rab 3404 df-v 3443 df-sbc 3728 df-csb 3844 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-nul 4270 df-if 4474 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4853 df-iun 4943 df-br 5093 df-opab 5155 df-mpt 5176 df-id 5518 df-xp 5626 df-rel 5627 df-cnv 5628 df-co 5629 df-dm 5630 df-rn 5631 df-res 5632 df-ima 5633 df-iota 6431 df-fun 6481 df-fn 6482 df-f 6483 df-f1 6484 df-fo 6485 df-f1o 6486 df-fv 6487 df-ov 7340 df-oprab 7341 df-mpo 7342 df-1st 7899 df-2nd 7900 df-map 8688 |
This theorem is referenced by: neicvgnvor 42055 |
Copyright terms: Public domain | W3C validator |