Theorem 0opn 23061

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

Syntax hints:   → wi 4   ∈ wcel 2143   ⊆ wss 3905  ∅c0 4286  ∪ cuni 4872  Topctop 23050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-in 3912  df-ss 3922  df-nul 4287  df-pw 4564  df-uni 4873  df-top 23051

This theorem is referenced by:  0ntop  23062  topgele  23087  tgclb  23127  0top  23140  en1top  23141  en2top  23142  topcld  23192  clsval2  23207  ntr0  23238  opnnei  23277  0nei  23285  restrcl  23314  rest0  23326  ordtrest2lem  23360  iocpnfordt  23372  icomnfordt  23373  cnindis  23449  isconn2  23571  kqtop  23902  mopn0  24655  locfinref  34231  ordtrest2NEWlem  34312  sxbrsigalem3  34662  cnambfre  38319