![]() |
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 22923 | . . 3 ⊢ TopSp = {𝑓 ∣ (TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓))} | |
2 | 1 | eleq2i 2818 | . 2 ⊢ (𝐾 ∈ TopSp ↔ 𝐾 ∈ {𝑓 ∣ (TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓))}) |
3 | topontop 22903 | . . . 4 ⊢ (𝐽 ∈ (TopOn‘𝐴) → 𝐽 ∈ Top) | |
4 | 0ntop 22895 | . . . . . 6 ⊢ ¬ ∅ ∈ Top | |
5 | istps.j | . . . . . . . 8 ⊢ 𝐽 = (TopOpen‘𝐾) | |
6 | fvprc 6885 | . . . . . . . 8 ⊢ (¬ 𝐾 ∈ V → (TopOpen‘𝐾) = ∅) | |
7 | 5, 6 | eqtrid 2778 | . . . . . . 7 ⊢ (¬ 𝐾 ∈ V → 𝐽 = ∅) |
8 | 7 | eleq1d 2811 | . . . . . 6 ⊢ (¬ 𝐾 ∈ V → (𝐽 ∈ Top ↔ ∅ ∈ Top)) |
9 | 4, 8 | mtbiri 326 | . . . . 5 ⊢ (¬ 𝐾 ∈ V → ¬ 𝐽 ∈ Top) |
10 | 9 | con4i 114 | . . . 4 ⊢ (𝐽 ∈ Top → 𝐾 ∈ V) |
11 | 3, 10 | syl 17 | . . 3 ⊢ (𝐽 ∈ (TopOn‘𝐴) → 𝐾 ∈ V) |
12 | fveq2 6893 | . . . . 5 ⊢ (𝑓 = 𝐾 → (TopOpen‘𝑓) = (TopOpen‘𝐾)) | |
13 | 12, 5 | eqtr4di 2784 | . . . 4 ⊢ (𝑓 = 𝐾 → (TopOpen‘𝑓) = 𝐽) |
14 | fveq2 6893 | . . . . . 6 ⊢ (𝑓 = 𝐾 → (Base‘𝑓) = (Base‘𝐾)) | |
15 | istps.a | . . . . . 6 ⊢ 𝐴 = (Base‘𝐾) | |
16 | 14, 15 | eqtr4di 2784 | . . . . 5 ⊢ (𝑓 = 𝐾 → (Base‘𝑓) = 𝐴) |
17 | 16 | fveq2d 6897 | . . . 4 ⊢ (𝑓 = 𝐾 → (TopOn‘(Base‘𝑓)) = (TopOn‘𝐴)) |
18 | 13, 17 | eleq12d 2820 | . . 3 ⊢ (𝑓 = 𝐾 → ((TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓)) ↔ 𝐽 ∈ (TopOn‘𝐴))) |
19 | 11, 18 | elab3 3673 | . 2 ⊢ (𝐾 ∈ {𝑓 ∣ (TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓))} ↔ 𝐽 ∈ (TopOn‘𝐴)) |
20 | 2, 19 | bitri 274 | 1 ⊢ (𝐾 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 = wceq 1534 ∈ wcel 2099 {cab 2703 Vcvv 3462 ∅c0 4322 ‘cfv 6546 Basecbs 17208 TopOpenctopn 17431 Topctop 22883 TopOnctopon 22900 TopSpctps 22922 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-sep 5296 ax-nul 5303 ax-pow 5361 ax-pr 5425 ax-un 7738 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ral 3052 df-rex 3061 df-rab 3420 df-v 3464 df-dif 3949 df-un 3951 df-in 3953 df-ss 3963 df-nul 4323 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-op 4630 df-uni 4906 df-br 5146 df-opab 5208 df-mpt 5229 df-id 5572 df-xp 5680 df-rel 5681 df-cnv 5682 df-co 5683 df-dm 5684 df-iota 6498 df-fun 6548 df-fv 6554 df-top 22884 df-topon 22901 df-topsp 22923 |
This theorem is referenced by: istps2 22925 tpspropd 22928 tsettps 22931 indistps2ALT 23006 resstps 23179 prdstps 23621 imastps 23713 xpstopnlem2 23803 tmdtopon 24073 tgptopon 24074 istgp2 24083 oppgtmd 24089 distgp 24091 indistgp 24092 efmndtmd 24093 qustgplem 24113 prdstmdd 24116 eltsms 24125 tsmscls 24130 tsmsgsum 24131 tsmsid 24132 tsmsmhm 24138 tsmsadd 24139 dvrcn 24176 cnmpt1vsca 24186 cnmpt2vsca 24187 tlmtgp 24188 ressusp 24257 tustps 24266 ucncn 24278 neipcfilu 24289 cnextucn 24296 ucnextcn 24297 isxms2 24442 ressxms 24522 prdsxmslem2 24526 nrgtrg 24695 cnfldtopon 24787 cnmpt1ds 24846 cnmpt2ds 24847 nmcn 24848 cnmpt1ip 25263 cnmpt2ip 25264 csscld 25265 clsocv 25266 minveclem4a 25446 rspectps 33711 mhmhmeotmd 33755 rrxtopon 45945 qndenserrnopnlem 45954 |
Copyright terms: Public domain | W3C validator |