Theorem 0opn 22952

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 4891	. 2 ⊢ ∪ ∅ = ∅
2		0ss 4351	. . 3 ⊢ ∅ ⊆ 𝐽
3		uniopn 22945	. . 3 ⊢ ((𝐽 ∈ Top ∧ ∅ ⊆ 𝐽) → ∪ ∅ ∈ 𝐽)
4	2, 3	mpan2 701	. 2 ⊢ (𝐽 ∈ Top → ∪ ∅ ∈ 𝐽)
5	1, 4	eqeltrrid 2866	1 ⊢ (𝐽 ∈ Top → ∅ ∈ 𝐽)

Syntax hints:   → wi 4   ∈ wcel 2141   ⊆ wss 3902  ∅c0 4283  ∪ cuni 4862  Topctop 22941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5243

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-in 3909  df-ss 3919  df-nul 4284  df-pw 4554  df-uni 4863  df-top 22942

This theorem is referenced by:  0ntop  22953  topgele  22978  tgclb  23018  0top  23031  en1top  23032  en2top  23033  topcld  23083  clsval2  23098  ntr0  23129  opnnei  23168  0nei  23176  restrcl  23205  rest0  23217  ordtrest2lem  23251  iocpnfordt  23263  icomnfordt  23264  cnindis  23340  isconn2  23462  kqtop  23793  mopn0  24546  locfinref  34099  ordtrest2NEWlem  34180  sxbrsigalem3  34530  cnambfre  38128