Theorem iinssdf

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

	Ref	Expression
Hypotheses	iinssdf.a	$$⊢\underset{\_}{Ⅎ}xA$$
	iinssdf.n	$$⊢\underset{\_}{Ⅎ}xX$$
	iinssdf.c	$$⊢\underset{\_}{Ⅎ}xC$$
	iinssdf.d	$$⊢\underset{\_}{Ⅎ}xD$$
	iinssdf.x	$$⊢\phi \to X\in A$$
	iinssdf.b	$$⊢x=X\to B=D$$
	iinssdf.s	$$⊢\phi \to D\subseteq C$$
Assertion	iinssdf	$$⊢\phi \to \bigcap _{x\in A}B\subseteq C$$

Proof

Step	Hyp	Ref	Expression
1		iinssdf.a	$$⊢\underset{\_}{Ⅎ}xA$$
2		iinssdf.n	$$⊢\underset{\_}{Ⅎ}xX$$
3		iinssdf.c	$$⊢\underset{\_}{Ⅎ}xC$$
4		iinssdf.d	$$⊢\underset{\_}{Ⅎ}xD$$
5		iinssdf.x	$$⊢\phi \to X\in A$$
6		iinssdf.b	$$⊢x=X\to B=D$$
7		iinssdf.s	$$⊢\phi \to D\subseteq C$$
8	4 3	nfss	$$⊢ℲxD\subseteq C$$
9	6	sseq1d	$$⊢x=X\to \left(B\subseteq C\leftrightarrow D\subseteq C\right)$$
10	8 2 1 9	rspcef	$$⊢\left(X\in A\wedge D\subseteq C\right)\to \exists x\in AB\subseteq C$$
11	5 7 10	syl2anc	$$⊢\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$$