Theorem 0opn 21509

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

Assertion

Ref	Expression
0opn	⊢ (𝐽 ∈ Top → ∅ ∈ 𝐽)

Proof of Theorem 0opn

Step	Hyp	Ref	Expression
1		uni0 4828	. 2 ⊢ ∪ ∅ = ∅
2		0ss 4304	. . 3 ⊢ ∅ ⊆ 𝐽
3		uniopn 21502	. . 3 ⊢ ((𝐽 ∈ Top ∧ ∅ ⊆ 𝐽) → ∪ ∅ ∈ 𝐽)
4	2, 3	mpan2 690	. 2 ⊢ (𝐽 ∈ Top → ∪ ∅ ∈ 𝐽)
5	1, 4	eqeltrrid 2895	1 ⊢ (𝐽 ∈ Top → ∅ ∈ 𝐽)

Syntax hints:   → wi 4   ∈ wcel 2111   ⊆ wss 3881  ∅c0 4243  ∪ cuni 4800  Topctop 21498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-dif 3884  df-in 3888  df-ss 3898  df-nul 4244  df-pw 4499  df-sn 4526  df-uni 4801  df-top 21499

This theorem is referenced by:  0ntop  21510  topgele  21535  tgclb  21575  0top  21588  en1top  21589  en2top  21590  topcld  21640  clsval2  21655  ntr0  21686  opnnei  21725  0nei  21733  restrcl  21762  rest0  21774  ordtrest2lem  21808  iocpnfordt  21820  icomnfordt  21821  cnindis  21897  isconn2  22019  kqtop  22350  mopn0  23105  locfinref  31194  ordtrest2NEWlem  31275  sxbrsigalem3  31640  cnambfre  35105