MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  istps Structured version   Visualization version   GIF version

Theorem istps 21539
Description: Express the predicate "is a topological space." (Contributed by Mario Carneiro, 13-Aug-2015.)
Hypotheses
Ref Expression
istps.a 𝐴 = (Base‘𝐾)
istps.j 𝐽 = (TopOpen‘𝐾)
Assertion
Ref Expression
istps (𝐾 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝐴))

Proof of Theorem istps
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef Expression
1 df-topsp 21538 . . 3 TopSp = {𝑓 ∣ (TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓))}
21eleq2i 2881 . 2 (𝐾 ∈ TopSp ↔ 𝐾 ∈ {𝑓 ∣ (TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓))})
3 topontop 21518 . . . 4 (𝐽 ∈ (TopOn‘𝐴) → 𝐽 ∈ Top)
4 0ntop 21510 . . . . . 6 ¬ ∅ ∈ Top
5 istps.j . . . . . . . 8 𝐽 = (TopOpen‘𝐾)
6 fvprc 6638 . . . . . . . 8 𝐾 ∈ V → (TopOpen‘𝐾) = ∅)
75, 6syl5eq 2845 . . . . . . 7 𝐾 ∈ V → 𝐽 = ∅)
87eleq1d 2874 . . . . . 6 𝐾 ∈ V → (𝐽 ∈ Top ↔ ∅ ∈ Top))
94, 8mtbiri 330 . . . . 5 𝐾 ∈ V → ¬ 𝐽 ∈ Top)
109con4i 114 . . . 4 (𝐽 ∈ Top → 𝐾 ∈ V)
113, 10syl 17 . . 3 (𝐽 ∈ (TopOn‘𝐴) → 𝐾 ∈ V)
12 fveq2 6645 . . . . 5 (𝑓 = 𝐾 → (TopOpen‘𝑓) = (TopOpen‘𝐾))
1312, 5eqtr4di 2851 . . . 4 (𝑓 = 𝐾 → (TopOpen‘𝑓) = 𝐽)
14 fveq2 6645 . . . . . 6 (𝑓 = 𝐾 → (Base‘𝑓) = (Base‘𝐾))
15 istps.a . . . . . 6 𝐴 = (Base‘𝐾)
1614, 15eqtr4di 2851 . . . . 5 (𝑓 = 𝐾 → (Base‘𝑓) = 𝐴)
1716fveq2d 6649 . . . 4 (𝑓 = 𝐾 → (TopOn‘(Base‘𝑓)) = (TopOn‘𝐴))
1813, 17eleq12d 2884 . . 3 (𝑓 = 𝐾 → ((TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓)) ↔ 𝐽 ∈ (TopOn‘𝐴)))
1911, 18elab3 3622 . 2 (𝐾 ∈ {𝑓 ∣ (TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓))} ↔ 𝐽 ∈ (TopOn‘𝐴))
202, 19bitri 278 1 (𝐾 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 209   = wceq 1538  wcel 2111  {cab 2776  Vcvv 3441  c0 4243  cfv 6324  Basecbs 16475  TopOpenctopn 16687  Topctop 21498  TopOnctopon 21515  TopSpctps 21537
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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-iota 6283  df-fun 6326  df-fv 6332  df-top 21499  df-topon 21516  df-topsp 21538
This theorem is referenced by:  istps2  21540  tpspropd  21543  tsettps  21546  indistps2ALT  21619  resstps  21792  prdstps  22234  imastps  22326  xpstopnlem2  22416  tmdtopon  22686  tgptopon  22687  istgp2  22696  oppgtmd  22702  distgp  22704  indistgp  22705  efmndtmd  22706  qustgplem  22726  prdstmdd  22729  eltsms  22738  tsmscls  22743  tsmsgsum  22744  tsmsid  22745  tsmsmhm  22751  tsmsadd  22752  dvrcn  22789  cnmpt1vsca  22799  cnmpt2vsca  22800  tlmtgp  22801  ressusp  22871  tustps  22879  ucncn  22891  neipcfilu  22902  cnextucn  22909  ucnextcn  22910  isxms2  23055  ressxms  23132  prdsxmslem2  23136  nrgtrg  23296  cnfldtopon  23388  cnmpt1ds  23447  cnmpt2ds  23448  nmcn  23449  cnmpt1ip  23851  cnmpt2ip  23852  csscld  23853  clsocv  23854  minveclem4a  24034  rspectps  31236  mhmhmeotmd  31280  rrxtopon  42928  qndenserrnopnlem  42937
  Copyright terms: Public domain W3C validator