Description: The empty set is an open subset of any topology. (Contributed by Stefan Allan, 27-Feb-2006)
Ref | Expression | ||
---|---|---|---|
Assertion | 0opn | ⊢ ( 𝐽 ∈ Top → ∅ ∈ 𝐽 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uni0 | ⊢ ∪ ∅ = ∅ | |
2 | 0ss | ⊢ ∅ ⊆ 𝐽 | |
3 | uniopn | ⊢ ( ( 𝐽 ∈ Top ∧ ∅ ⊆ 𝐽 ) → ∪ ∅ ∈ 𝐽 ) | |
4 | 2 3 | mpan2 | ⊢ ( 𝐽 ∈ Top → ∪ ∅ ∈ 𝐽 ) |
5 | 1 4 | eqeltrrid | ⊢ ( 𝐽 ∈ Top → ∅ ∈ 𝐽 ) |