Theorem isopn3i

Description: An open subset equals its own interior. (Contributed by Mario Carneiro, 30-Dec-2016)

	Ref	Expression
Assertion	isopn3i	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽 ) → 𝑆 ∈ 𝐽 )
2		elssuni	⊢ ( 𝑆 ∈ 𝐽 → 𝑆 ⊆ ∪ 𝐽 )
3		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
4	3	isopn3	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → ( 𝑆 ∈ 𝐽 ↔ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 ) )
5	2 4	sylan2	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽 ) → ( 𝑆 ∈ 𝐽 ↔ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 ) )
6	1 5	mpbid	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 )