Theorem mopnin

Description: The intersection of two open sets of a metric space is open. (Contributed by NM, 4-Sep-2006) (Revised by Mario Carneiro, 23-Dec-2013)

	Ref	Expression
Hypothesis	mopni.1	|- J = ( MetOpen ` D )
Assertion	mopnin	|- ( ( D e. ( *Met ` X ) /\ A e. J /\ B e. J ) -> ( A i^i B ) e. J )

Proof

Step	Hyp	Ref	Expression
1		mopni.1	|- J = ( MetOpen ` D )
2	1	mopntop	|- ( D e. ( *Met ` X ) -> J e. Top )
3		inopn	|- ( ( J e. Top /\ A e. J /\ B e. J ) -> ( A i^i B ) e. J )
4	2 3	syl3an1	|- ( ( D e. ( *Met ` X ) /\ A e. J /\ B e. J ) -> ( A i^i B ) e. J )