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 21784 | . . 3 ⊢ TopSp = {𝑓 ∣ (TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓))} | |
2 | 1 | eleq2i 2822 | . 2 ⊢ (𝐾 ∈ TopSp ↔ 𝐾 ∈ {𝑓 ∣ (TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓))}) |
3 | topontop 21764 | . . . 4 ⊢ (𝐽 ∈ (TopOn‘𝐴) → 𝐽 ∈ Top) | |
4 | 0ntop 21756 | . . . . . 6 ⊢ ¬ ∅ ∈ Top | |
5 | istps.j | . . . . . . . 8 ⊢ 𝐽 = (TopOpen‘𝐾) | |
6 | fvprc 6687 | . . . . . . . 8 ⊢ (¬ 𝐾 ∈ V → (TopOpen‘𝐾) = ∅) | |
7 | 5, 6 | syl5eq 2783 | . . . . . . 7 ⊢ (¬ 𝐾 ∈ V → 𝐽 = ∅) |
8 | 7 | eleq1d 2815 | . . . . . 6 ⊢ (¬ 𝐾 ∈ V → (𝐽 ∈ Top ↔ ∅ ∈ Top)) |
9 | 4, 8 | mtbiri 330 | . . . . 5 ⊢ (¬ 𝐾 ∈ V → ¬ 𝐽 ∈ Top) |
10 | 9 | con4i 114 | . . . 4 ⊢ (𝐽 ∈ Top → 𝐾 ∈ V) |
11 | 3, 10 | syl 17 | . . 3 ⊢ (𝐽 ∈ (TopOn‘𝐴) → 𝐾 ∈ V) |
12 | fveq2 6695 | . . . . 5 ⊢ (𝑓 = 𝐾 → (TopOpen‘𝑓) = (TopOpen‘𝐾)) | |
13 | 12, 5 | eqtr4di 2789 | . . . 4 ⊢ (𝑓 = 𝐾 → (TopOpen‘𝑓) = 𝐽) |
14 | fveq2 6695 | . . . . . 6 ⊢ (𝑓 = 𝐾 → (Base‘𝑓) = (Base‘𝐾)) | |
15 | istps.a | . . . . . 6 ⊢ 𝐴 = (Base‘𝐾) | |
16 | 14, 15 | eqtr4di 2789 | . . . . 5 ⊢ (𝑓 = 𝐾 → (Base‘𝑓) = 𝐴) |
17 | 16 | fveq2d 6699 | . . . 4 ⊢ (𝑓 = 𝐾 → (TopOn‘(Base‘𝑓)) = (TopOn‘𝐴)) |
18 | 13, 17 | eleq12d 2825 | . . 3 ⊢ (𝑓 = 𝐾 → ((TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓)) ↔ 𝐽 ∈ (TopOn‘𝐴))) |
19 | 11, 18 | elab3 3584 | . 2 ⊢ (𝐾 ∈ {𝑓 ∣ (TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓))} ↔ 𝐽 ∈ (TopOn‘𝐴)) |
20 | 2, 19 | bitri 278 | 1 ⊢ (𝐾 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 209 = wceq 1543 ∈ wcel 2112 {cab 2714 Vcvv 3398 ∅c0 4223 ‘cfv 6358 Basecbs 16666 TopOpenctopn 16880 Topctop 21744 TopOnctopon 21761 TopSpctps 21783 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2708 ax-sep 5177 ax-nul 5184 ax-pow 5243 ax-pr 5307 ax-un 7501 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2728 df-clel 2809 df-nfc 2879 df-ne 2933 df-ral 3056 df-rex 3057 df-rab 3060 df-v 3400 df-sbc 3684 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-nul 4224 df-if 4426 df-pw 4501 df-sn 4528 df-pr 4530 df-op 4534 df-uni 4806 df-br 5040 df-opab 5102 df-mpt 5121 df-id 5440 df-xp 5542 df-rel 5543 df-cnv 5544 df-co 5545 df-dm 5546 df-iota 6316 df-fun 6360 df-fv 6366 df-top 21745 df-topon 21762 df-topsp 21784 |
This theorem is referenced by: istps2 21786 tpspropd 21789 tsettps 21792 indistps2ALT 21865 resstps 22038 prdstps 22480 imastps 22572 xpstopnlem2 22662 tmdtopon 22932 tgptopon 22933 istgp2 22942 oppgtmd 22948 distgp 22950 indistgp 22951 efmndtmd 22952 qustgplem 22972 prdstmdd 22975 eltsms 22984 tsmscls 22989 tsmsgsum 22990 tsmsid 22991 tsmsmhm 22997 tsmsadd 22998 dvrcn 23035 cnmpt1vsca 23045 cnmpt2vsca 23046 tlmtgp 23047 ressusp 23116 tustps 23124 ucncn 23136 neipcfilu 23147 cnextucn 23154 ucnextcn 23155 isxms2 23300 ressxms 23377 prdsxmslem2 23381 nrgtrg 23542 cnfldtopon 23634 cnmpt1ds 23693 cnmpt2ds 23694 nmcn 23695 cnmpt1ip 24098 cnmpt2ip 24099 csscld 24100 clsocv 24101 minveclem4a 24281 rspectps 31501 mhmhmeotmd 31545 rrxtopon 43447 qndenserrnopnlem 43456 |
Copyright terms: Public domain | W3C validator |