Theorem inopnd

Description: The intersection of two open sets of a topology is an open set. (Contributed by Glauco Siliprandi, 21-Dec-2024)

	Ref	Expression
Hypotheses	inopnd.1	|- ( ph -> J e. Top )
	inopnd.2	|- ( ph -> A e. J )
	inopnd.3	|- ( ph -> B e. J )
Assertion	inopnd	|- ( ph -> ( A i^i B ) e. J )

Proof

Step	Hyp	Ref	Expression
1		inopnd.1	|- ( ph -> J e. Top )
2		inopnd.2	|- ( ph -> A e. J )
3		inopnd.3	|- ( ph -> B e. J )
4		inopn	|- ( ( J e. Top /\ A e. J /\ B e. J ) -> ( A i^i B ) e. J )
5	1 2 3 4	syl3anc	|- ( ph -> ( A i^i B ) e. J )