Theorem 0opn 22807

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3905  ∅c0 4286  ∪ cuni 4861  Topctop 22796

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 5238

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 3397  df-v 3440  df-dif 3908  df-in 3912  df-ss 3922  df-nul 4287  df-pw 4555  df-sn 4580  df-uni 4862  df-top 22797

This theorem is referenced by:  0ntop  22808  topgele  22833  tgclb  22873  0top  22886  en1top  22887  en2top  22888  topcld  22938  clsval2  22953  ntr0  22984  opnnei  23023  0nei  23031  restrcl  23060  rest0  23072  ordtrest2lem  23106  iocpnfordt  23118  icomnfordt  23119  cnindis  23195  isconn2  23317  kqtop  23648  mopn0  24402  locfinref  33810  ordtrest2NEWlem  33891  sxbrsigalem3  34242  cnambfre  37650