Theorem 0opn 23215

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ⊆ wss 3899  ∅c0 4279  ∪ cuni 4867  Topctop 23204

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-in 3906  df-ss 3916  df-nul 4280  df-pw 4559  df-uni 4868  df-top 23205

This theorem is used by:  0ntop  23216  topgele  23241  tgclb  23281  0top  23294  en1top  23295  en2top  23296  topcld  23346  clsval2  23361  ntr0  23392  opnnei  23431  0nei  23439  restrcl  23468  rest0  23480  ordtrest2lem  23514  iocpnfordt  23526  icomnfordt  23527  cnindis  23603  isconn2  23725  kqtop  24057  mopn0  24810  locfinref  34466  ordtrest2NEWlem  34547  sxbrsigalem3  34897  cnambfre  38566