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

Theorem 0opn 18497
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 4113 . 2  |-  U. (/)  =  (/)
2 0ss 3661 . . 3  |-  (/)  C_  J
3 uniopn 18490 . . 3  |-  ( ( J  e.  Top  /\  (/)  C_  J )  ->  U. (/)  e.  J
)
42, 3mpan2 671 . 2  |-  ( J  e.  Top  ->  U. (/)  e.  J
)
51, 4syl5eqelr 2523 1  |-  ( J  e.  Top  ->  (/)  e.  J
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756    C_ wss 3323   (/)c0 3632   U.cuni 4086   Topctop 18478
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-v 2969  df-dif 3326  df-in 3330  df-ss 3337  df-nul 3633  df-pw 3857  df-sn 3873  df-uni 4087  df-top 18483
This theorem is referenced by:  0ntop  18498  istps2OLD  18506  topgele  18519  tgclb  18555  0top  18568  en1top  18569  en2top  18570  topcld  18619  clsval2  18634  ntr0  18665  opnnei  18704  0nei  18712  restrcl  18741  rest0  18753  ordtrest2lem  18787  iocpnfordt  18799  icomnfordt  18800  cnindis  18876  iscon2  18998  kqtop  19298  mopn0  20053  ordtrest2NEWlem  26321  sxbrsigalem3  26656  cnambfre  28411
  Copyright terms: Public domain W3C validator