Theorem 0opnt 7601

Description: The empty set is an open subset of a topology. (Contributed by Stefan Allan, 27-Feb-2006.)

Assertion

Ref	Expression
0opnt	|- (J e. Top -> (/) e. J)

Proof of Theorem 0opnt

Step	Hyp	Ref	Expression
1		0ss 2301	. . 3 |- (/) (_ J
2		uniopnt 7598	. . 3 |- ((J e. Top /\ (/) (_ J) -> U.(/) e. J)
3	1, 2	mpan2 696	. 2 |- (J e. Top -> U.(/) e. J)
4		uni0 2525	. 2 |- U.(/) = (/)
5	3, 4	syl5eqelr 1553	1 |- (J e. Top -> (/) e. J)

Syntax hints:   -> wi 3   e. wcel 958   (_ wss 2047  (/)c0 2280  U.cuni 2503  Topctop 7588

This theorem is referenced by:  istps2 7607  0top 7635  iooretop 7659  topcld 7675  ntr0 7710  0nei 7739  cnpco 7769  cnconst 7780  opn0 7873  empntop 10506  mapudiscn 10512  top1 10547  top2ind 10548

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-ral 1649  df-rex 1650  df-v 1812  df-dif 2049  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-uni 2504  df-top 7592

Copyright terms: Public domain