Theorem 0opn 22053

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 4869	. 2 ⊢ ∪ ∅ = ∅
2		0ss 4330	. . 3 ⊢ ∅ ⊆ 𝐽
3		uniopn 22046	. . 3 ⊢ ((𝐽 ∈ Top ∧ ∅ ⊆ 𝐽) → ∪ ∅ ∈ 𝐽)
4	2, 3	mpan2 688	. 2 ⊢ (𝐽 ∈ Top → ∪ ∅ ∈ 𝐽)
5	1, 4	eqeltrrid 2844	1 ⊢ (𝐽 ∈ Top → ∅ ∈ 𝐽)

Syntax hints:   → wi 4   ∈ wcel 2106   ⊆ wss 3887  ∅c0 4256  ∪ cuni 4839  Topctop 22042

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-11 2154  ax-ext 2709  ax-sep 5223

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-in 3894  df-ss 3904  df-nul 4257  df-pw 4535  df-sn 4562  df-uni 4840  df-top 22043

This theorem is referenced by:  0ntop  22054  topgele  22079  tgclb  22120  0top  22133  en1top  22134  en2top  22135  topcld  22186  clsval2  22201  ntr0  22232  opnnei  22271  0nei  22279  restrcl  22308  rest0  22320  ordtrest2lem  22354  iocpnfordt  22366  icomnfordt  22367  cnindis  22443  isconn2  22565  kqtop  22896  mopn0  23654  locfinref  31791  ordtrest2NEWlem  31872  sxbrsigalem3  32239  cnambfre  35825