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

Theorem 0opn 16650
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 3854 . 2  |-  U. (/)  =  (/)
2 0ss 3483 . . 3  |-  (/)  C_  J
3 uniopn 16643 . . 3  |-  ( ( J  e.  Top  /\  (/)  C_  J )  ->  U. (/)  e.  J
)
42, 3mpan2 652 . 2  |-  ( J  e.  Top  ->  U. (/)  e.  J
)
51, 4syl5eqelr 2368 1  |-  ( J  e.  Top  ->  (/)  e.  J
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684    C_ wss 3152   (/)c0 3455   U.cuni 3827   Topctop 16631
This theorem is referenced by:  0ntop  16651  istps2OLD  16659  topgele  16672  tgclb  16708  0top  16721  en1top  16722  en2top  16723  topcld  16772  clsval2  16787  ntr0  16818  opnnei  16857  0nei  16865  restrcl  16888  rest0  16900  ordtrest2lem  16933  iocpnfordt  16945  icomnfordt  16946  cnindis  17020  iscon2  17140  kqtop  17436  mopn0  18044
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-v 2790  df-dif 3155  df-in 3159  df-ss 3166  df-nul 3456  df-pw 3627  df-sn 3646  df-uni 3828  df-top 16636
  Copyright terms: Public domain W3C validator