Theorem ss2iundf

Description: Subclass theorem for indexed union. (Contributed by RP, 17-Jul-2020)

	Ref	Expression
Hypotheses	ss2iundf.xph	$$⊢Ⅎx\phi$$
	ss2iundf.yph	$$⊢Ⅎy\phi$$
	ss2iundf.y	$$⊢\underset{\_}{Ⅎ}yY$$
	ss2iundf.a	$$⊢\underset{\_}{Ⅎ}yA$$
	ss2iundf.b	$$⊢\underset{\_}{Ⅎ}yB$$
	ss2iundf.xc	$$⊢\underset{\_}{Ⅎ}xC$$
	ss2iundf.yc	$$⊢\underset{\_}{Ⅎ}yC$$
	ss2iundf.d	$$⊢\underset{\_}{Ⅎ}xD$$
	ss2iundf.g	$$⊢\underset{\_}{Ⅎ}yG$$
	ss2iundf.el	$$⊢\left(\phi \wedge x\in A\right)\to Y\in C$$
	ss2iundf.sub	$$⊢\left(\phi \wedge x\in A\wedge y=Y\right)\to D=G$$
	ss2iundf.ss	$$⊢\left(\phi \wedge x\in A\right)\to B\subseteq G$$
Assertion	ss2iundf	$$⊢\phi \to \bigcup _{x\in A}B\subseteq \bigcup _{y\in C}D$$

Proof

Step	Hyp	Ref	Expression
1		ss2iundf.xph	$$⊢Ⅎx\phi$$
2		ss2iundf.yph	$$⊢Ⅎy\phi$$
3		ss2iundf.y	$$⊢\underset{\_}{Ⅎ}yY$$
4		ss2iundf.a	$$⊢\underset{\_}{Ⅎ}yA$$
5		ss2iundf.b	$$⊢\underset{\_}{Ⅎ}yB$$
6		ss2iundf.xc	$$⊢\underset{\_}{Ⅎ}xC$$
7		ss2iundf.yc	$$⊢\underset{\_}{Ⅎ}yC$$
8		ss2iundf.d	$$⊢\underset{\_}{Ⅎ}xD$$
9		ss2iundf.g	$$⊢\underset{\_}{Ⅎ}yG$$
10		ss2iundf.el	$$⊢\left(\phi \wedge x\in A\right)\to Y\in C$$
11		ss2iundf.sub	$$⊢\left(\phi \wedge x\in A\wedge y=Y\right)\to D=G$$
12		ss2iundf.ss	$$⊢\left(\phi \wedge x\in A\right)\to B\subseteq G$$
13		df-ral	$$⊢\forall y\in C\neg B\subseteq D\leftrightarrow \forall y\left(y\in C\to \neg B\subseteq D\right)$$
14	4	nfcri	$$⊢Ⅎyx\in A$$
15	2 14	nfan	$$⊢Ⅎy\left(\phi \wedge x\in A\right)$$
16		simpr	$$⊢\left(\left(\phi \wedge x\in A\right)\wedge y=Y\right)\to y=Y$$
17	16	eleq1d	$$⊢\left(\left(\phi \wedge x\in A\right)\wedge y=Y\right)\to \left(y\in C\leftrightarrow Y\in C\right)$$
18	17	biimprd	$$⊢\left(\left(\phi \wedge x\in A\right)\wedge y=Y\right)\to \left(Y\in C\to y\in C\right)$$
19	11	sseq2d	$$⊢\left(\phi \wedge x\in A\wedge y=Y\right)\to \left(B\subseteq D\leftrightarrow B\subseteq G\right)$$
20	19	3expa	$$⊢\left(\left(\phi \wedge x\in A\right)\wedge y=Y\right)\to \left(B\subseteq D\leftrightarrow B\subseteq G\right)$$
21	20	notbid	$$⊢\left(\left(\phi \wedge x\in A\right)\wedge y=Y\right)\to \left(\neg B\subseteq D\leftrightarrow \neg B\subseteq G\right)$$
22	21	biimpd	$$⊢\left(\left(\phi \wedge x\in A\right)\wedge y=Y\right)\to \left(\neg B\subseteq D\to \neg B\subseteq G\right)$$
23	18 22	imim12d	$$⊢\left(\left(\phi \wedge x\in A\right)\wedge y=Y\right)\to \left(\left(y\in C\to \neg B\subseteq D\right)\to \left(Y\in C\to \neg B\subseteq G\right)\right)$$
24	23	ex	$$⊢\left(\phi \wedge x\in A\right)\to \left(y=Y\to \left(\left(y\in C\to \neg B\subseteq D\right)\to \left(Y\in C\to \neg B\subseteq G\right)\right)\right)$$
25	15 24	alrimi	$$⊢\left(\phi \wedge x\in A\right)\to \forall y\left(y=Y\to \left(\left(y\in C\to \neg B\subseteq D\right)\to \left(Y\in C\to \neg B\subseteq G\right)\right)\right)$$
26	3 7	nfel	$$⊢ℲyY\in C$$
27	5 9	nfss	$$⊢ℲyB\subseteq G$$
28	27	nfn	$$⊢Ⅎy\neg B\subseteq G$$
29	26 28	nfim	$$⊢Ⅎy\left(Y\in C\to \neg B\subseteq G\right)$$
30	29 3	spcimgfi1	$$⊢\forall y\left(y=Y\to \left(\left(y\in C\to \neg B\subseteq D\right)\to \left(Y\in C\to \neg B\subseteq G\right)\right)\right)\to \left(Y\in C\to \left(\forall y\left(y\in C\to \neg B\subseteq D\right)\to \left(Y\in C\to \neg B\subseteq G\right)\right)\right)$$
31	25 10 30	sylc	$$⊢\left(\phi \wedge x\in A\right)\to \left(\forall y\left(y\in C\to \neg B\subseteq D\right)\to \left(Y\in C\to \neg B\subseteq G\right)\right)$$
32	10 31	mpid	$$⊢\left(\phi \wedge x\in A\right)\to \left(\forall y\left(y\in C\to \neg B\subseteq D\right)\to \neg B\subseteq G\right)$$
33	13 32	biimtrid	$$⊢\left(\phi \wedge x\in A\right)\to \left(\forall y\in C\neg B\subseteq D\to \neg B\subseteq G\right)$$
34	33	con2d	$$⊢\left(\phi \wedge x\in A\right)\to \left(B\subseteq G\to \neg \forall y\in C\neg B\subseteq D\right)$$
35		dfrex2	$$⊢\exists y\in CB\subseteq D\leftrightarrow \neg \forall y\in C\neg B\subseteq D$$
36	34 35	imbitrrdi	$$⊢\left(\phi \wedge x\in A\right)\to \left(B\subseteq G\to \exists y\in CB\subseteq D\right)$$
37	12 36	mpd	$$⊢\left(\phi \wedge x\in A\right)\to \exists y\in CB\subseteq D$$
38	1 37	ralrimia	$$⊢\phi \to \forall x\in A\exists y\in CB\subseteq D$$
39		ssel	$$⊢B\subseteq D\to \left(z\in B\to z\in D\right)$$
40	39	reximi	$$⊢\exists y\in CB\subseteq D\to \exists y\in C\left(z\in B\to z\in D\right)$$
41	5	nfcri	$$⊢Ⅎyz\in B$$
42	41	r19.37	$$⊢\exists y\in C\left(z\in B\to z\in D\right)\to \left(z\in B\to \exists y\in Cz\in D\right)$$
43	40 42	syl	$$⊢\exists y\in CB\subseteq D\to \left(z\in B\to \exists y\in Cz\in D\right)$$
44		eliun	$$⊢z\in \bigcup _{y\in C}D\leftrightarrow \exists y\in Cz\in D$$
45	43 44	imbitrrdi	$$⊢\exists y\in CB\subseteq D\to \left(z\in B\to z\in \bigcup _{y\in C}D\right)$$
46	45	ssrdv	$$⊢\exists y\in CB\subseteq D\to B\subseteq \bigcup _{y\in C}D$$
47	46	ralimi	$$⊢\forall x\in A\exists y\in CB\subseteq D\to \forall x\in AB\subseteq \bigcup _{y\in C}D$$
48	6 8	nfiun	$$⊢\underset{\_}{Ⅎ}x\bigcup _{y\in C}D$$
49	48	iunssf	$$⊢\bigcup _{x\in A}B\subseteq \bigcup _{y\in C}D\leftrightarrow \forall x\in AB\subseteq \bigcup _{y\in C}D$$
50	47 49	sylibr	$$⊢\forall x\in A\exists y\in CB\subseteq D\to \bigcup _{x\in A}B\subseteq \bigcup _{y\in C}D$$
51	38 50	syl	$$⊢\phi \to \bigcup _{x\in A}B\subseteq \bigcup _{y\in C}D$$