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

Theorem 0opn 16932
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 4002 . 2  |-  U. (/)  =  (/)
2 0ss 3616 . . 3  |-  (/)  C_  J
3 uniopn 16925 . . 3  |-  ( ( J  e.  Top  /\  (/)  C_  J )  ->  U. (/)  e.  J
)
42, 3mpan2 653 . 2  |-  ( J  e.  Top  ->  U. (/)  e.  J
)
51, 4syl5eqelr 2489 1  |-  ( J  e.  Top  ->  (/)  e.  J
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721    C_ wss 3280   (/)c0 3588   U.cuni 3975   Topctop 16913
This theorem is referenced by:  0ntop  16933  istps2OLD  16941  topgele  16954  tgclb  16990  0top  17003  en1top  17004  en2top  17005  topcld  17054  clsval2  17069  ntr0  17100  opnnei  17139  0nei  17147  restrcl  17175  rest0  17187  ordtrest2lem  17221  iocpnfordt  17233  icomnfordt  17234  cnindis  17310  iscon2  17430  kqtop  17730  mopn0  18481  sxbrsigalem3  24575  cnambfre  26154
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-v 2918  df-dif 3283  df-in 3287  df-ss 3294  df-nul 3589  df-pw 3761  df-sn 3780  df-uni 3976  df-top 16918
  Copyright terms: Public domain W3C validator