Theorem 0opn 20709

Description: The empty set is an open subset of a topology. (Contributed by Stefan Allan, 27-Feb-2006.)

Assertion

Ref	Expression
0opn	⊢ (𝐽 ∈ Top → ∅ ∈ 𝐽)

Proof of Theorem 0opn

Step	Hyp	Ref	Expression
1		uni0 4465	. 2 ⊢ ∪ ∅ = ∅
2		0ss 3972	. . 3 ⊢ ∅ ⊆ 𝐽
3		uniopn 20702	. . 3 ⊢ ((𝐽 ∈ Top ∧ ∅ ⊆ 𝐽) → ∪ ∅ ∈ 𝐽)
4	2, 3	mpan2 707	. 2 ⊢ (𝐽 ∈ Top → ∪ ∅ ∈ 𝐽)
5	1, 4	syl5eqelr 2706	1 ⊢ (𝐽 ∈ Top → ∅ ∈ 𝐽)

Syntax hints:   → wi 4   ∈ wcel 1990   ⊆ wss 3574  ∅c0 3915  ∪ cuni 4436  Topctop 20698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-v 3202  df-dif 3577  df-in 3581  df-ss 3588  df-nul 3916  df-pw 4160  df-sn 4178  df-uni 4437  df-top 20699

This theorem is referenced by:  0ntop  20710  topgele  20734  tgclb  20774  0top  20787  en1top  20788  en2top  20789  topcld  20839  clsval2  20854  ntr0  20885  opnnei  20924  0nei  20932  restrcl  20961  rest0  20973  ordtrest2lem  21007  iocpnfordt  21019  icomnfordt  21020  cnindis  21096  isconn2  21217  kqtop  21548  mopn0  22303  locfinref  29908  ordtrest2NEWlem  29968  sxbrsigalem3  30334  cnambfre  33458