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

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

Proof of Theorem 0opn
StepHypRef Expression
1 uni0 4601 . 2 ∅ = ∅
2 0ss 4116 . . 3 ∅ ⊆ 𝐽
3 uniopn 20922 . . 3 ((𝐽 ∈ Top ∧ ∅ ⊆ 𝐽) → ∅ ∈ 𝐽)
42, 3mpan2 671 . 2 (𝐽 ∈ Top → ∅ ∈ 𝐽)
51, 4syl5eqelr 2855 1 (𝐽 ∈ Top → ∅ ∈ 𝐽)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2145  wss 3723  c0 4063   cuni 4574  Topctop 20918
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-v 3353  df-dif 3726  df-in 3730  df-ss 3737  df-nul 4064  df-pw 4299  df-sn 4317  df-uni 4575  df-top 20919
This theorem is referenced by:  0ntop  20930  topgele  20955  tgclb  20995  0top  21008  en1top  21009  en2top  21010  topcld  21060  clsval2  21075  ntr0  21106  opnnei  21145  0nei  21153  restrcl  21182  rest0  21194  ordtrest2lem  21228  iocpnfordt  21240  icomnfordt  21241  cnindis  21317  isconn2  21438  kqtop  21769  mopn0  22523  locfinref  30248  ordtrest2NEWlem  30308  sxbrsigalem3  30674  cnambfre  33790
  Copyright terms: Public domain W3C validator