Theorem 0opn 23026

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 4902	. 2 ⊢ ∪ ∅ = ∅
2		0ss 4363	. . 3 ⊢ ∅ ⊆ 𝐽
3		uniopn 23019	. . 3 ⊢ ((𝐽 ∈ Top ∧ ∅ ⊆ 𝐽) → ∪ ∅ ∈ 𝐽)
4	2, 3	mpan2 703	. 2 ⊢ (𝐽 ∈ Top → ∪ ∅ ∈ 𝐽)
5	1, 4	eqeltrrid 2874	1 ⊢ (𝐽 ∈ Top → ∅ ∈ 𝐽)

Syntax hints:   → wi 4   ∈ wcel 2149   ⊆ wss 3913  ∅c0 4294  ∪ cuni 4873  Topctop 23015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5258

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-in 3920  df-ss 3930  df-nul 4295  df-pw 4566  df-uni 4874  df-top 23016

This theorem is referenced by:  0ntop  23027  topgele  23052  tgclb  23092  0top  23105  en1top  23106  en2top  23107  topcld  23157  clsval2  23172  ntr0  23203  opnnei  23242  0nei  23250  restrcl  23279  rest0  23291  ordtrest2lem  23325  iocpnfordt  23337  icomnfordt  23338  cnindis  23414  isconn2  23536  kqtop  23867  mopn0  24620  locfinref  34172  ordtrest2NEWlem  34253  sxbrsigalem3  34603  cnambfre  38202