Theorem 0opn 23091

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ⊆ wss 3906  ∅c0 4286  ∪ cuni 4874  Topctop 23080

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-in 3913  df-ss 3923  df-nul 4287  df-pw 4566  df-uni 4875  df-top 23081

This theorem is used by:  0ntop  23092  topgele  23117  tgclb  23157  0top  23170  en1top  23171  en2top  23172  topcld  23222  clsval2  23237  ntr0  23268  opnnei  23307  0nei  23315  restrcl  23344  rest0  23356  ordtrest2lem  23390  iocpnfordt  23402  icomnfordt  23403  cnindis  23479  isconn2  23601  kqtop  23933  mopn0  24686  locfinref  34271  ordtrest2NEWlem  34352  sxbrsigalem3  34703  cnambfre  38352