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

Theorem 0opn 19173
Description: The empty set is an open subset of a topology. (Contributed by Stefan Allan, 27-Feb-2006.)
Assertion
Ref Expression
0opn  |-  ( J  e.  Top  ->  (/)  e.  J
)

Proof of Theorem 0opn
StepHypRef Expression
1 uni0 4265 . 2  |-  U. (/)  =  (/)
2 0ss 3807 . . 3  |-  (/)  C_  J
3 uniopn 19166 . . 3  |-  ( ( J  e.  Top  /\  (/)  C_  J )  ->  U. (/)  e.  J
)
42, 3mpan2 671 . 2  |-  ( J  e.  Top  ->  U. (/)  e.  J
)
51, 4syl5eqelr 2553 1  |-  ( J  e.  Top  ->  (/)  e.  J
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1762    C_ wss 3469   (/)c0 3778   U.cuni 4238   Topctop 19154
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-v 3108  df-dif 3472  df-in 3476  df-ss 3483  df-nul 3779  df-pw 4005  df-sn 4021  df-uni 4239  df-top 19159
This theorem is referenced by:  0ntop  19174  istps2OLD  19182  topgele  19195  tgclb  19231  0top  19244  en1top  19245  en2top  19246  topcld  19295  clsval2  19310  ntr0  19341  opnnei  19380  0nei  19388  restrcl  19417  rest0  19429  ordtrest2lem  19463  iocpnfordt  19475  icomnfordt  19476  cnindis  19552  iscon2  19674  kqtop  19974  mopn0  20729  ordtrest2NEWlem  27526  sxbrsigalem3  27869  cnambfre  29627
  Copyright terms: Public domain W3C validator