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

Theorem 0opn 21518
 Description: The empty set is an open subset of any topology. (Contributed by Stefan Allan, 27-Feb-2006.)
Assertion
Ref Expression
0opn (𝐽 ∈ Top → ∅ ∈ 𝐽)

Proof of Theorem 0opn
StepHypRef Expression
1 uni0 4852 . 2 ∅ = ∅
2 0ss 4333 . . 3 ∅ ⊆ 𝐽
3 uniopn 21511 . . 3 ((𝐽 ∈ Top ∧ ∅ ⊆ 𝐽) → ∅ ∈ 𝐽)
42, 3mpan2 690 . 2 (𝐽 ∈ Top → ∅ ∈ 𝐽)
51, 4eqeltrrid 2921 1 (𝐽 ∈ Top → ∅ ∈ 𝐽)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2115   ⊆ wss 3919  ∅c0 4276  ∪ cuni 4824  Topctop 21507 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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5190 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-dif 3922  df-in 3926  df-ss 3936  df-nul 4277  df-pw 4524  df-sn 4551  df-uni 4825  df-top 21508 This theorem is referenced by:  0ntop  21519  topgele  21544  tgclb  21584  0top  21597  en1top  21598  en2top  21599  topcld  21649  clsval2  21664  ntr0  21695  opnnei  21734  0nei  21742  restrcl  21771  rest0  21783  ordtrest2lem  21817  iocpnfordt  21829  icomnfordt  21830  cnindis  21906  isconn2  22028  kqtop  22359  mopn0  23114  locfinref  31174  ordtrest2NEWlem  31250  sxbrsigalem3  31615  cnambfre  35077
 Copyright terms: Public domain W3C validator