riinn0

Description: Relative intersection of a nonempty family. (Contributed by Stefan O'Rear, 3-Apr-2015)

		Ref	Expression
	Assertion	riinn0	$⊢ (\forall x \in X S \subseteq A \land X \neq \emptyset) \to A \cap ⋂_{x \in X} S = ⋂_{x \in X} S$

Step	Hyp	Ref	Expression
1		incom	$⊢ A \cap ⋂_{x \in X} S = ⋂_{x \in X} S \cap A$
2		r19.2z	$⊢ (X \neq \emptyset \land \forall x \in X S \subseteq A) \to \exists x \in X S \subseteq A$
3	2	ancoms	$⊢ (\forall x \in X S \subseteq A \land X \neq \emptyset) \to \exists x \in X S \subseteq A$
4		iinss	$⊢ \exists x \in X S \subseteq A \to ⋂_{x \in X} S \subseteq A$
5	3 4	syl	$⊢ (\forall x \in X S \subseteq A \land X \neq \emptyset) \to ⋂_{x \in X} S \subseteq A$
6		dfss2	$⊢ ⋂_{x \in X} S \subseteq A \leftrightarrow ⋂_{x \in X} S \cap A = ⋂_{x \in X} S$
7	5 6	sylib	$⊢ (\forall x \in X S \subseteq A \land X \neq \emptyset) \to ⋂_{x \in X} S \cap A = ⋂_{x \in X} S$
8	1 7	eqtrid	$⊢ (\forall x \in X S \subseteq A \land X \neq \emptyset) \to A \cap ⋂_{x \in X} S = ⋂_{x \in X} S$

Metamath Proof Explorer