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

Theorem 0opn 16982
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 4044 . 2  |-  U. (/)  =  (/)
2 0ss 3658 . . 3  |-  (/)  C_  J
3 uniopn 16975 . . 3  |-  ( ( J  e.  Top  /\  (/)  C_  J )  ->  U. (/)  e.  J
)
42, 3mpan2 654 . 2  |-  ( J  e.  Top  ->  U. (/)  e.  J
)
51, 4syl5eqelr 2523 1  |-  ( J  e.  Top  ->  (/)  e.  J
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726    C_ wss 3322   (/)c0 3630   U.cuni 4017   Topctop 16963
This theorem is referenced by:  0ntop  16983  istps2OLD  16991  topgele  17004  tgclb  17040  0top  17053  en1top  17054  en2top  17055  topcld  17104  clsval2  17119  ntr0  17150  opnnei  17189  0nei  17197  restrcl  17226  rest0  17238  ordtrest2lem  17272  iocpnfordt  17284  icomnfordt  17285  cnindis  17361  iscon2  17482  kqtop  17782  mopn0  18533  sxbrsigalem3  24627  cnambfre  26267
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-v 2960  df-dif 3325  df-in 3329  df-ss 3336  df-nul 3631  df-pw 3803  df-sn 3822  df-uni 4018  df-top 16968
  Copyright terms: Public domain W3C validator