Theorem 0opn 22847

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 4916	. 2 ⊢ ∪ ∅ = ∅
2		0ss 4380	. . 3 ⊢ ∅ ⊆ 𝐽
3		uniopn 22840	. . 3 ⊢ ((𝐽 ∈ Top ∧ ∅ ⊆ 𝐽) → ∪ ∅ ∈ 𝐽)
4	2, 3	mpan2 691	. 2 ⊢ (𝐽 ∈ Top → ∪ ∅ ∈ 𝐽)
5	1, 4	eqeltrrid 2840	1 ⊢ (𝐽 ∈ Top → ∅ ∈ 𝐽)

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3931  ∅c0 4313  ∪ cuni 4888  Topctop 22836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-11 2158  ax-ext 2708  ax-sep 5271

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-in 3938  df-ss 3948  df-nul 4314  df-pw 4582  df-sn 4607  df-uni 4889  df-top 22837

This theorem is referenced by:  0ntop  22848  topgele  22873  tgclb  22913  0top  22926  en1top  22927  en2top  22928  topcld  22978  clsval2  22993  ntr0  23024  opnnei  23063  0nei  23071  restrcl  23100  rest0  23112  ordtrest2lem  23146  iocpnfordt  23158  icomnfordt  23159  cnindis  23235  isconn2  23357  kqtop  23688  mopn0  24442  locfinref  33877  ordtrest2NEWlem  33958  sxbrsigalem3  34309  cnambfre  37697