iinssiin

Description: Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Step	Hyp	Ref	Expression
1		iinssiin.1	$⊢ Ⅎ x φ$
2		iinssiin.2	$⊢ (φ \land x \in A) \to B \subseteq C$
3		nfii1	$⊢ \underline{Ⅎ} x ⋂_{x \in A} B$
4	3	nfcri	$⊢ Ⅎ x y \in ⋂_{x \in A} B$
5	1 4	nfan	$⊢ Ⅎ x (φ \land y \in ⋂_{x \in A} B)$
6	2	adantlr	$⊢ ((φ \land y \in ⋂_{x \in A} B) \land x \in A) \to B \subseteq C$
7		eliinid	$⊢ (y \in ⋂_{x \in A} B \land x \in A) \to y \in B$
8	7	adantll	$⊢ ((φ \land y \in ⋂_{x \in A} B) \land x \in A) \to y \in B$
9	6 8	sseldd	$⊢ ((φ \land y \in ⋂_{x \in A} B) \land x \in A) \to y \in C$
10	9	ex	$⊢ (φ \land y \in ⋂_{x \in A} B) \to (x \in A \to y \in C)$
11	5 10	ralrimi	$⊢ (φ \land y \in ⋂_{x \in A} B) \to \forall x \in A y \in C$
12		eliin	$⊢ y \in V \to (y \in ⋂_{x \in A} C \leftrightarrow \forall x \in A y \in C)$
13	12	elv	$⊢ y \in ⋂_{x \in A} C \leftrightarrow \forall x \in A y \in C$
14	11 13	sylibr	$⊢ (φ \land y \in ⋂_{x \in A} B) \to y \in ⋂_{x \in A} C$
15	14	ssd	$⊢ φ \to ⋂_{x \in A} B \subseteq ⋂_{x \in A} C$

Metamath Proof Explorer