Theorem ntr0

Description: The interior of the empty set. (Contributed by NM, 2-Oct-2007)

	Ref	Expression
Assertion	ntr0	⊢ ( 𝐽 ∈ Top → ( ( int ‘ 𝐽 ) ‘ ∅ ) = ∅ )

Proof

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 ‘ 𝐽 ) ‘ ∅ ) = ∅ )