Theorem iinss2d

Description: Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 24-Jan-2025)

	Ref	Expression
Hypotheses	iinss2d.1	$$⊢Ⅎx\phi$$
	iinss2d.2	$$⊢\underset{\_}{Ⅎ}xA$$
	iinss2d.3	$$⊢\underset{\_}{Ⅎ}xC$$
	iinss2d.4	$$⊢\phi \to A\ne \varnothing$$
	iinss2d.5	$$⊢\left(\phi \wedge x\in A\right)\to B\subseteq C$$
Assertion	iinss2d	$$⊢\phi \to \bigcap _{x\in A}B\subseteq C$$

Proof

Step	Hyp	Ref	Expression
1		iinss2d.1	$$⊢Ⅎx\phi$$
2		iinss2d.2	$$⊢\underset{\_}{Ⅎ}xA$$
3		iinss2d.3	$$⊢\underset{\_}{Ⅎ}xC$$
4		iinss2d.4	$$⊢\phi \to A\ne \varnothing$$
5		iinss2d.5	$$⊢\left(\phi \wedge x\in A\right)\to B\subseteq C$$
6	5	3adant3	$$⊢\left(\phi \wedge x\in A\wedge \top \right)\to B\subseteq C$$
7	2	n0f	$$⊢A\ne \varnothing \leftrightarrow \exists xx\in A$$
8	4 7	sylib	$$⊢\phi \to \exists xx\in A$$
9		rextru	$$⊢\exists xx\in A\leftrightarrow \exists x\in A\top$$
10	8 9	sylib	$$⊢\phi \to \exists x\in A\top$$
11	1 6 10	reximdd	$$⊢\phi \to \exists x\in AB\subseteq C$$
12	3	iinssf	$$⊢\exists x\in AB\subseteq C\to \bigcap _{x\in A}B\subseteq C$$
13	11 12	syl	$$⊢\phi \to \bigcap _{x\in A}B\subseteq C$$