Theorem 0opn 21210

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 4737	. 2 ⊢ ∪ ∅ = ∅
2		0ss 4234	. . 3 ⊢ ∅ ⊆ 𝐽
3		uniopn 21203	. . 3 ⊢ ((𝐽 ∈ Top ∧ ∅ ⊆ 𝐽) → ∪ ∅ ∈ 𝐽)
4	2, 3	mpan2 678	. 2 ⊢ (𝐽 ∈ Top → ∪ ∅ ∈ 𝐽)
5	1, 4	syl5eqelr 2868	1 ⊢ (𝐽 ∈ Top → ∅ ∈ 𝐽)

Syntax hints:   → wi 4   ∈ wcel 2048   ⊆ wss 3828  ∅c0 4177  ∪ cuni 4710  Topctop 21199

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2747  ax-sep 5058

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2756  df-cleq 2768  df-clel 2843  df-nfc 2915  df-ral 3090  df-rex 3091  df-v 3414  df-dif 3831  df-in 3835  df-ss 3842  df-nul 4178  df-pw 4422  df-sn 4440  df-uni 4711  df-top 21200

This theorem is referenced by:  0ntop  21211  topgele  21236  tgclb  21276  0top  21289  en1top  21290  en2top  21291  topcld  21341  clsval2  21356  ntr0  21387  opnnei  21426  0nei  21434  restrcl  21463  rest0  21475  ordtrest2lem  21509  iocpnfordt  21521  icomnfordt  21522  cnindis  21598  isconn2  21720  kqtop  22051  mopn0  22805  locfinref  30740  ordtrest2NEWlem  30800  sxbrsigalem3  31166  cnambfre  34359