Description: The interior of the empty set. (Contributed by NM, 2-Oct-2007)
Ref | Expression | ||
---|---|---|---|
Assertion | ntr0 | ⊢ ( 𝐽 ∈ Top → ( ( int ‘ 𝐽 ) ‘ ∅ ) = ∅ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0opn | ⊢ ( 𝐽 ∈ Top → ∅ ∈ 𝐽 ) | |
2 | 0ss | ⊢ ∅ ⊆ ∪ 𝐽 | |
3 | eqid | ⊢ ∪ 𝐽 = ∪ 𝐽 | |
4 | 3 | isopn3 | ⊢ ( ( 𝐽 ∈ Top ∧ ∅ ⊆ ∪ 𝐽 ) → ( ∅ ∈ 𝐽 ↔ ( ( int ‘ 𝐽 ) ‘ ∅ ) = ∅ ) ) |
5 | 2 4 | mpan2 | ⊢ ( 𝐽 ∈ Top → ( ∅ ∈ 𝐽 ↔ ( ( int ‘ 𝐽 ) ‘ ∅ ) = ∅ ) ) |
6 | 1 5 | mpbid | ⊢ ( 𝐽 ∈ Top → ( ( int ‘ 𝐽 ) ‘ ∅ ) = ∅ ) |