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

Theorem 0opn 20629
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 4436 . 2 ∅ = ∅
2 0ss 3949 . . 3 ∅ ⊆ 𝐽
3 uniopn 20622 . . 3 ((𝐽 ∈ Top ∧ ∅ ⊆ 𝐽) → ∅ ∈ 𝐽)
42, 3mpan2 706 . 2 (𝐽 ∈ Top → ∅ ∈ 𝐽)
51, 4syl5eqelr 2709 1 (𝐽 ∈ Top → ∅ ∈ 𝐽)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1992  wss 3560  c0 3896   cuni 4407  Topctop 20612
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-sep 4746
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ral 2917  df-rex 2918  df-v 3193  df-dif 3563  df-in 3567  df-ss 3574  df-nul 3897  df-pw 4137  df-sn 4154  df-uni 4408  df-top 20616
This theorem is referenced by:  0ntop  20630  topgele  20644  tgclb  20680  0top  20693  en1top  20694  en2top  20695  topcld  20744  clsval2  20759  ntr0  20790  opnnei  20829  0nei  20837  restrcl  20866  rest0  20878  ordtrest2lem  20912  iocpnfordt  20924  icomnfordt  20925  cnindis  21001  isconn2  21122  kqtop  21453  mopn0  22208  locfinref  29682  ordtrest2NEWlem  29742  sxbrsigalem3  30107  cnambfre  33076
  Copyright terms: Public domain W3C validator