Theorem 0opn 22791

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3914  ∅c0 4296  ∪ cuni 4871  Topctop 22780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-11 2158  ax-ext 2701  ax-sep 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-in 3921  df-ss 3931  df-nul 4297  df-pw 4565  df-sn 4590  df-uni 4872  df-top 22781

This theorem is referenced by:  0ntop  22792  topgele  22817  tgclb  22857  0top  22870  en1top  22871  en2top  22872  topcld  22922  clsval2  22937  ntr0  22968  opnnei  23007  0nei  23015  restrcl  23044  rest0  23056  ordtrest2lem  23090  iocpnfordt  23102  icomnfordt  23103  cnindis  23179  isconn2  23301  kqtop  23632  mopn0  24386  locfinref  33831  ordtrest2NEWlem  33912  sxbrsigalem3  34263  cnambfre  37662