Theorem 0opn 23129

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 23122	. . 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 2145   ⊆ wss 3899  ∅c0 4279  ∪ cuni 4867  Topctop 23118

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 2732  ax-sep 5251

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 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-in 3906  df-ss 3916  df-nul 4280  df-pw 4559  df-uni 4868  df-top 23119

This theorem is used by:  0ntop  23130  topgele  23155  tgclb  23195  0top  23208  en1top  23209  en2top  23210  topcld  23260  clsval2  23275  ntr0  23306  opnnei  23345  0nei  23353  restrcl  23382  rest0  23394  ordtrest2lem  23428  iocpnfordt  23440  icomnfordt  23441  cnindis  23517  isconn2  23639  kqtop  23971  mopn0  24724  locfinref  34351  ordtrest2NEWlem  34432  sxbrsigalem3  34783  cnambfre  38417