Theorem 0opn 22822

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 4888	. 2 ⊢ ∪ ∅ = ∅
2		0ss 4349	. . 3 ⊢ ∅ ⊆ 𝐽
3		uniopn 22815	. . 3 ⊢ ((𝐽 ∈ Top ∧ ∅ ⊆ 𝐽) → ∪ ∅ ∈ 𝐽)
4	2, 3	mpan2 691	. 2 ⊢ (𝐽 ∈ Top → ∪ ∅ ∈ 𝐽)
5	1, 4	eqeltrrid 2838	1 ⊢ (𝐽 ∈ Top → ∅ ∈ 𝐽)

Syntax hints:   → wi 4   ∈ wcel 2113   ⊆ wss 3898  ∅c0 4282  ∪ cuni 4860  Topctop 22811

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5238

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-in 3905  df-ss 3915  df-nul 4283  df-pw 4553  df-uni 4861  df-top 22812

This theorem is referenced by:  0ntop  22823  topgele  22848  tgclb  22888  0top  22901  en1top  22902  en2top  22903  topcld  22953  clsval2  22968  ntr0  22999  opnnei  23038  0nei  23046  restrcl  23075  rest0  23087  ordtrest2lem  23121  iocpnfordt  23133  icomnfordt  23134  cnindis  23210  isconn2  23332  kqtop  23663  mopn0  24416  locfinref  33877  ordtrest2NEWlem  33958  sxbrsigalem3  34308  cnambfre  37731