rintopn

Description: A finite relative intersection of open sets is open. (Contributed by Mario Carneiro, 22-Aug-2015)

		Ref	Expression
	Hypothesis	1open.1	$⊢ X = ⋃ J$
	Assertion	rintopn	$⊢ (J \in Top \land A \subseteq J \land A \in Fin) \to X \cap ⋂ A \in J$

Step	Hyp	Ref	Expression
1		1open.1	$⊢ X = ⋃ J$
2		intiin	$⊢ ⋂ A = ⋂_{x \in A} x$
3	2	ineq2i	$⊢ X \cap ⋂ A = X \cap ⋂_{x \in A} x$
4		dfss3	$⊢ A \subseteq J \leftrightarrow \forall x \in A x \in J$
5	1	riinopn	$⊢ (J \in Top \land A \in Fin \land \forall x \in A x \in J) \to X \cap ⋂_{x \in A} x \in J$
6	5	3com23	$⊢ (J \in Top \land \forall x \in A x \in J \land A \in Fin) \to X \cap ⋂_{x \in A} x \in J$
7	4 6	syl3an2b	$⊢ (J \in Top \land A \subseteq J \land A \in Fin) \to X \cap ⋂_{x \in A} x \in J$
8	3 7	eqeltrid	$⊢ (J \in Top \land A \subseteq J \land A \in Fin) \to X \cap ⋂ A \in J$

Metamath Proof Explorer