![]() |
Mathbox for Richard Penner |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > ntrneiel | Structured version Visualization version GIF version |
Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, 𝐹, then there is an equivalence between membership in the interior of a set and non-membership in the closure of the complement of the set. (Contributed by RP, 29-May-2021.) |
Ref | Expression |
---|---|
ntrnei.o | ⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)}))) |
ntrnei.f | ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵) |
ntrnei.r | ⊢ (𝜑 → 𝐼𝐹𝑁) |
ntrnei.x | ⊢ (𝜑 → 𝑋 ∈ 𝐵) |
ntrnei.s | ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵) |
Ref | Expression |
---|---|
ntrneiel | ⊢ (𝜑 → (𝑋 ∈ (𝐼‘𝑆) ↔ 𝑆 ∈ (𝑁‘𝑋))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ntrnei.s | . . 3 ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝐵) | |
2 | fveq2 6862 | . . . . 5 ⊢ (𝑚 = 𝑆 → (𝐼‘𝑚) = (𝐼‘𝑆)) | |
3 | 2 | eleq2d 2818 | . . . 4 ⊢ (𝑚 = 𝑆 → (𝑋 ∈ (𝐼‘𝑚) ↔ 𝑋 ∈ (𝐼‘𝑆))) |
4 | 3 | elrab3 3664 | . . 3 ⊢ (𝑆 ∈ 𝒫 𝐵 → (𝑆 ∈ {𝑚 ∈ 𝒫 𝐵 ∣ 𝑋 ∈ (𝐼‘𝑚)} ↔ 𝑋 ∈ (𝐼‘𝑆))) |
5 | 1, 4 | syl 17 | . 2 ⊢ (𝜑 → (𝑆 ∈ {𝑚 ∈ 𝒫 𝐵 ∣ 𝑋 ∈ (𝐼‘𝑚)} ↔ 𝑋 ∈ (𝐼‘𝑆))) |
6 | ntrnei.o | . . . . 5 ⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑m 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)}))) | |
7 | ntrnei.f | . . . . . . 7 ⊢ 𝐹 = (𝒫 𝐵𝑂𝐵) | |
8 | ntrnei.r | . . . . . . 7 ⊢ (𝜑 → 𝐼𝐹𝑁) | |
9 | 6, 7, 8 | ntrneibex 42500 | . . . . . 6 ⊢ (𝜑 → 𝐵 ∈ V) |
10 | 9 | pwexd 5354 | . . . . 5 ⊢ (𝜑 → 𝒫 𝐵 ∈ V) |
11 | 6, 7, 8 | ntrneiiex 42503 | . . . . 5 ⊢ (𝜑 → 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) |
12 | eqid 2731 | . . . . 5 ⊢ (𝐹‘𝐼) = (𝐹‘𝐼) | |
13 | ntrnei.x | . . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝐵) | |
14 | 6, 10, 9, 7, 11, 12, 13 | fsovfvfvd 42438 | . . . 4 ⊢ (𝜑 → ((𝐹‘𝐼)‘𝑋) = {𝑚 ∈ 𝒫 𝐵 ∣ 𝑋 ∈ (𝐼‘𝑚)}) |
15 | 6, 7, 8 | ntrneifv1 42506 | . . . . 5 ⊢ (𝜑 → (𝐹‘𝐼) = 𝑁) |
16 | 15 | fveq1d 6864 | . . . 4 ⊢ (𝜑 → ((𝐹‘𝐼)‘𝑋) = (𝑁‘𝑋)) |
17 | 14, 16 | eqtr3d 2773 | . . 3 ⊢ (𝜑 → {𝑚 ∈ 𝒫 𝐵 ∣ 𝑋 ∈ (𝐼‘𝑚)} = (𝑁‘𝑋)) |
18 | 17 | eleq2d 2818 | . 2 ⊢ (𝜑 → (𝑆 ∈ {𝑚 ∈ 𝒫 𝐵 ∣ 𝑋 ∈ (𝐼‘𝑚)} ↔ 𝑆 ∈ (𝑁‘𝑋))) |
19 | 5, 18 | bitr3d 280 | 1 ⊢ (𝜑 → (𝑋 ∈ (𝐼‘𝑆) ↔ 𝑆 ∈ (𝑁‘𝑋))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1541 ∈ wcel 2106 {crab 3418 Vcvv 3459 𝒫 cpw 4580 class class class wbr 5125 ↦ cmpt 5208 ‘cfv 6516 (class class class)co 7377 ∈ cmpo 7379 ↑m cmap 8787 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 ax-rep 5262 ax-sep 5276 ax-nul 5283 ax-pow 5340 ax-pr 5404 ax-un 7692 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-ral 3061 df-rex 3070 df-reu 3365 df-rab 3419 df-v 3461 df-sbc 3758 df-csb 3874 df-dif 3931 df-un 3933 df-in 3935 df-ss 3945 df-nul 4303 df-if 4507 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4886 df-iun 4976 df-br 5126 df-opab 5188 df-mpt 5209 df-id 5551 df-xp 5659 df-rel 5660 df-cnv 5661 df-co 5662 df-dm 5663 df-rn 5664 df-res 5665 df-ima 5666 df-iota 6468 df-fun 6518 df-fn 6519 df-f 6520 df-f1 6521 df-fo 6522 df-f1o 6523 df-fv 6524 df-ov 7380 df-oprab 7381 df-mpo 7382 df-1st 7941 df-2nd 7942 df-map 8789 |
This theorem is referenced by: ntrneifv3 42509 ntrneineine0lem 42510 ntrneineine1lem 42511 ntrneifv4 42512 ntrneiel2 42513 ntrneicls00 42516 ntrneicls11 42517 ntrneiiso 42518 ntrneik2 42519 ntrneix2 42520 ntrneikb 42521 ntrneixb 42522 ntrneik3 42523 ntrneix3 42524 ntrneik13 42525 ntrneix13 42526 ntrneik4w 42527 ntrneik4 42528 clsneiel1 42535 neicvgel1 42546 |
Copyright terms: Public domain | W3C validator |