Theorem 0opn 23231

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   ⊆ wss 3896  ∅c0 4277  ∪ cuni 4866  Topctop 23220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-nul 4278  df-pw 4558  df-uni 4867  df-top 23221

This theorem is used by:  0ntop  23232  topgele  23257  tgclb  23297  0top  23310  en1top  23311  en2top  23312  topcld  23362  clsval2  23377  ntr0  23408  opnnei  23447  0nei  23455  restrcl  23484  rest0  23496  ordtrest2lem  23530  iocpnfordt  23542  icomnfordt  23543  cnindis  23619  isconn2  23741  kqtop  24073  mopn0  24826  locfinref  34523  ordtrest2NEWlem  34604  sxbrsigalem3  34954  cnambfre  38695