Theorem 0opn 21512

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3936  ∅c0 4291  ∪ cuni 4838  Topctop 21501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-in 3943  df-ss 3952  df-nul 4292  df-pw 4541  df-sn 4568  df-uni 4839  df-top 21502

This theorem is referenced by:  0ntop  21513  topgele  21538  tgclb  21578  0top  21591  en1top  21592  en2top  21593  topcld  21643  clsval2  21658  ntr0  21689  opnnei  21728  0nei  21736  restrcl  21765  rest0  21777  ordtrest2lem  21811  iocpnfordt  21823  icomnfordt  21824  cnindis  21900  isconn2  22022  kqtop  22353  mopn0  23108  locfinref  31105  ordtrest2NEWlem  31165  sxbrsigalem3  31530  cnambfre  34955