Theorem 0opn 23229

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   ⊆ wss 3896  ∅c0 4277  ∪ cuni 4866  Topctop 23218

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-nul 4278  df-pw 4558  df-uni 4867  df-top 23219

This theorem is used by:  0ntop  23230  topgele  23255  tgclb  23295  0top  23308  en1top  23309  en2top  23310  topcld  23360  clsval2  23375  ntr0  23406  opnnei  23445  0nei  23453  restrcl  23482  rest0  23494  ordtrest2lem  23528  iocpnfordt  23540  icomnfordt  23541  cnindis  23617  isconn2  23739  kqtop  24071  mopn0  24824  locfinref  34521  ordtrest2NEWlem  34602  sxbrsigalem3  34952  cnambfre  38693