Theorem 0opn 22405

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

Syntax hints:   → wi 4   ∈ wcel 2106   ⊆ wss 3948  ∅c0 4322  ∪ cuni 4908  Topctop 22394

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-11 2154  ax-ext 2703  ax-sep 5299

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-in 3955  df-ss 3965  df-nul 4323  df-pw 4604  df-sn 4629  df-uni 4909  df-top 22395

This theorem is referenced by:  0ntop  22406  topgele  22431  tgclb  22472  0top  22485  en1top  22486  en2top  22487  topcld  22538  clsval2  22553  ntr0  22584  opnnei  22623  0nei  22631  restrcl  22660  rest0  22672  ordtrest2lem  22706  iocpnfordt  22718  icomnfordt  22719  cnindis  22795  isconn2  22917  kqtop  23248  mopn0  24006  locfinref  32816  ordtrest2NEWlem  32897  sxbrsigalem3  33266  cnambfre  36531