![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > istps | Structured version Visualization version GIF version |
Description: Express the predicate "is a topological space." (Contributed by Mario Carneiro, 13-Aug-2015.) |
Ref | Expression |
---|---|
istps.a | ⊢ 𝐴 = (Base‘𝐾) |
istps.j | ⊢ 𝐽 = (TopOpen‘𝐾) |
Ref | Expression |
---|---|
istps | ⊢ (𝐾 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-topsp 21107 | . . 3 ⊢ TopSp = {𝑓 ∣ (TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓))} | |
2 | 1 | eleq2i 2897 | . 2 ⊢ (𝐾 ∈ TopSp ↔ 𝐾 ∈ {𝑓 ∣ (TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓))}) |
3 | topontop 21087 | . . . 4 ⊢ (𝐽 ∈ (TopOn‘𝐴) → 𝐽 ∈ Top) | |
4 | 0ntop 21079 | . . . . . 6 ⊢ ¬ ∅ ∈ Top | |
5 | istps.j | . . . . . . . 8 ⊢ 𝐽 = (TopOpen‘𝐾) | |
6 | fvprc 6425 | . . . . . . . 8 ⊢ (¬ 𝐾 ∈ V → (TopOpen‘𝐾) = ∅) | |
7 | 5, 6 | syl5eq 2872 | . . . . . . 7 ⊢ (¬ 𝐾 ∈ V → 𝐽 = ∅) |
8 | 7 | eleq1d 2890 | . . . . . 6 ⊢ (¬ 𝐾 ∈ V → (𝐽 ∈ Top ↔ ∅ ∈ Top)) |
9 | 4, 8 | mtbiri 319 | . . . . 5 ⊢ (¬ 𝐾 ∈ V → ¬ 𝐽 ∈ Top) |
10 | 9 | con4i 114 | . . . 4 ⊢ (𝐽 ∈ Top → 𝐾 ∈ V) |
11 | 3, 10 | syl 17 | . . 3 ⊢ (𝐽 ∈ (TopOn‘𝐴) → 𝐾 ∈ V) |
12 | fveq2 6432 | . . . . 5 ⊢ (𝑓 = 𝐾 → (TopOpen‘𝑓) = (TopOpen‘𝐾)) | |
13 | 12, 5 | syl6eqr 2878 | . . . 4 ⊢ (𝑓 = 𝐾 → (TopOpen‘𝑓) = 𝐽) |
14 | fveq2 6432 | . . . . . 6 ⊢ (𝑓 = 𝐾 → (Base‘𝑓) = (Base‘𝐾)) | |
15 | istps.a | . . . . . 6 ⊢ 𝐴 = (Base‘𝐾) | |
16 | 14, 15 | syl6eqr 2878 | . . . . 5 ⊢ (𝑓 = 𝐾 → (Base‘𝑓) = 𝐴) |
17 | 16 | fveq2d 6436 | . . . 4 ⊢ (𝑓 = 𝐾 → (TopOn‘(Base‘𝑓)) = (TopOn‘𝐴)) |
18 | 13, 17 | eleq12d 2899 | . . 3 ⊢ (𝑓 = 𝐾 → ((TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓)) ↔ 𝐽 ∈ (TopOn‘𝐴))) |
19 | 11, 18 | elab3 3578 | . 2 ⊢ (𝐾 ∈ {𝑓 ∣ (TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓))} ↔ 𝐽 ∈ (TopOn‘𝐴)) |
20 | 2, 19 | bitri 267 | 1 ⊢ (𝐾 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 198 = wceq 1658 ∈ wcel 2166 {cab 2810 Vcvv 3413 ∅c0 4143 ‘cfv 6122 Basecbs 16221 TopOpenctopn 16434 Topctop 21067 TopOnctopon 21084 TopSpctps 21106 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-8 2168 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2390 ax-ext 2802 ax-sep 5004 ax-nul 5012 ax-pow 5064 ax-pr 5126 ax-un 7208 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2604 df-eu 2639 df-clab 2811 df-cleq 2817 df-clel 2820 df-nfc 2957 df-ral 3121 df-rex 3122 df-rab 3125 df-v 3415 df-sbc 3662 df-dif 3800 df-un 3802 df-in 3804 df-ss 3811 df-nul 4144 df-if 4306 df-pw 4379 df-sn 4397 df-pr 4399 df-op 4403 df-uni 4658 df-br 4873 df-opab 4935 df-mpt 4952 df-id 5249 df-xp 5347 df-rel 5348 df-cnv 5349 df-co 5350 df-dm 5351 df-iota 6085 df-fun 6124 df-fv 6130 df-top 21068 df-topon 21085 df-topsp 21107 |
This theorem is referenced by: istps2 21109 tpspropd 21112 tsettps 21115 indistps2ALT 21188 resstps 21361 prdstps 21802 imastps 21894 xpstopnlem2 21984 tmdtopon 22254 tgptopon 22255 istgp2 22264 oppgtmd 22270 distgp 22272 indistgp 22273 symgtgp 22274 qustgplem 22293 prdstmdd 22296 eltsms 22305 tsmscls 22310 tsmsgsum 22311 tsmsid 22312 tsmsmhm 22318 tsmsadd 22319 dvrcn 22356 cnmpt1vsca 22366 cnmpt2vsca 22367 tlmtgp 22368 ressusp 22438 tustps 22446 ucncn 22458 neipcfilu 22469 cnextucn 22476 ucnextcn 22477 isxms2 22622 ressxms 22699 prdsxmslem2 22703 nrgtrg 22863 cnfldtopon 22955 cnmpt1ds 23014 cnmpt2ds 23015 nmcn 23016 cnmpt1ip 23414 cnmpt2ip 23415 csscld 23416 clsocv 23417 minveclem4a 23597 mhmhmeotmd 30517 rrxtopon 41298 qndenserrnopnlem 41307 |
Copyright terms: Public domain | W3C validator |