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

Theorem 0opn 19580
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 4262 . 2  |-  U. (/)  =  (/)
2 0ss 3813 . . 3  |-  (/)  C_  J
3 uniopn 19573 . . 3  |-  ( ( J  e.  Top  /\  (/)  C_  J )  ->  U. (/)  e.  J
)
42, 3mpan2 669 . 2  |-  ( J  e.  Top  ->  U. (/)  e.  J
)
51, 4syl5eqelr 2547 1  |-  ( J  e.  Top  ->  (/)  e.  J
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1823    C_ wss 3461   (/)c0 3783   U.cuni 4235   Topctop 19561
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-v 3108  df-dif 3464  df-in 3468  df-ss 3475  df-nul 3784  df-pw 4001  df-sn 4017  df-uni 4236  df-top 19566
This theorem is referenced by:  0ntop  19581  istps2OLD  19589  topgele  19602  tgclb  19639  0top  19652  en1top  19653  en2top  19654  topcld  19703  clsval2  19718  ntr0  19749  opnnei  19788  0nei  19796  restrcl  19825  rest0  19837  ordtrest2lem  19871  iocpnfordt  19883  icomnfordt  19884  cnindis  19960  iscon2  20081  kqtop  20412  mopn0  21167  locfinref  28079  ordtrest2NEWlem  28139  sxbrsigalem3  28480  cnambfre  30303
  Copyright terms: Public domain W3C validator