This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isopn3i

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

		Ref	Expression
	Assertion	isopn3i	$⊢ (J \in Top \land S \in J) \to int (J) (S) = S$

Step	Hyp	Ref	Expression
1		simpr	$⊢ (J \in Top \land S \in J) \to S \in J$
2		elssuni	$⊢ S \in J \to S \subseteq ⋃ J$
3		eqid	$⊢ ⋃ J = ⋃ J$
4	3	isopn3	$⊢ (J \in Top \land S \subseteq ⋃ J) \to (S \in J \leftrightarrow int (J) (S) = S)$
5	2 4	sylan2	$⊢ (J \in Top \land S \in J) \to (S \in J \leftrightarrow int (J) (S) = S)$
6	1 5	mpbid	$⊢ (J \in Top \land S \in J) \to int (J) (S) = S$