ss2iundf

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

	Ref	Expression
Hypotheses	ss2iundf.xph	$⊢ Ⅎ x φ$
	ss2iundf.yph	$⊢ Ⅎ y φ$
	ss2iundf.y	$⊢ \underline{Ⅎ} y Y$
	ss2iundf.a	$⊢ \underline{Ⅎ} y A$
	ss2iundf.b	$⊢ \underline{Ⅎ} y B$
	ss2iundf.xc	$⊢ \underline{Ⅎ} x C$
	ss2iundf.yc	$⊢ \underline{Ⅎ} y C$
	ss2iundf.d	$⊢ \underline{Ⅎ} x D$
	ss2iundf.g	$⊢ \underline{Ⅎ} y G$
	ss2iundf.el	$⊢ (φ \land x \in A) \to Y \in C$
	ss2iundf.sub	$⊢ (φ \land x \in A \land y = Y) \to D = G$
	ss2iundf.ss	$⊢ (φ \land x \in A) \to B \subseteq G$
Assertion	ss2iundf	$⊢ φ \to ⋃_{x \in A} B \subseteq ⋃_{y \in C} D$

Proof

Step	Hyp	Ref	Expression
1		ss2iundf.xph	$⊢ Ⅎ x φ$
2		ss2iundf.yph	$⊢ Ⅎ y φ$
3		ss2iundf.y	$⊢ \underline{Ⅎ} y Y$
4		ss2iundf.a	$⊢ \underline{Ⅎ} y A$
5		ss2iundf.b	$⊢ \underline{Ⅎ} y B$
6		ss2iundf.xc	$⊢ \underline{Ⅎ} x C$
7		ss2iundf.yc	$⊢ \underline{Ⅎ} y C$
8		ss2iundf.d	$⊢ \underline{Ⅎ} x D$
9		ss2iundf.g	$⊢ \underline{Ⅎ} y G$
10		ss2iundf.el	$⊢ (φ \land x \in A) \to Y \in C$
11		ss2iundf.sub	$⊢ (φ \land x \in A \land y = Y) \to D = G$
12		ss2iundf.ss	$⊢ (φ \land x \in A) \to B \subseteq G$
13		df-ral	$⊢ \forall y \in C \neg B \subseteq D \leftrightarrow \forall y (y \in C \to \neg B \subseteq D)$
14	4	nfcri	$⊢ Ⅎ y x \in A$
15	2 14	nfan	$⊢ Ⅎ y (φ \land x \in A)$
16		simpr	$⊢ ((φ \land x \in A) \land y = Y) \to y = Y$
17	16	eleq1d	$⊢ ((φ \land x \in A) \land y = Y) \to (y \in C \leftrightarrow Y \in C)$
18	17	biimprd	$⊢ ((φ \land x \in A) \land y = Y) \to (Y \in C \to y \in C)$
19	11	sseq2d	$⊢ (φ \land x \in A \land y = Y) \to (B \subseteq D \leftrightarrow B \subseteq G)$
20	19	3expa	$⊢ ((φ \land x \in A) \land y = Y) \to (B \subseteq D \leftrightarrow B \subseteq G)$
21	20	notbid	$⊢ ((φ \land x \in A) \land y = Y) \to (\neg B \subseteq D \leftrightarrow \neg B \subseteq G)$
22	21	biimpd	$⊢ ((φ \land x \in A) \land y = Y) \to (\neg B \subseteq D \to \neg B \subseteq G)$
23	18 22	imim12d	$⊢ ((φ \land x \in A) \land y = Y) \to ((y \in C \to \neg B \subseteq D) \to (Y \in C \to \neg B \subseteq G))$
24	23	ex	$⊢ (φ \land x \in A) \to (y = Y \to ((y \in C \to \neg B \subseteq D) \to (Y \in C \to \neg B \subseteq G)))$
25	15 24	alrimi	$⊢ (φ \land x \in A) \to \forall y (y = Y \to ((y \in C \to \neg B \subseteq D) \to (Y \in C \to \neg B \subseteq G)))$
26	3 7	nfel	$⊢ Ⅎ y Y \in C$
27	5 9	nfss	$⊢ Ⅎ y B \subseteq G$
28	27	nfn	$⊢ Ⅎ y \neg B \subseteq G$
29	26 28	nfim	$⊢ Ⅎ y (Y \in C \to \neg B \subseteq G)$
30	29 3	spcimgft	$⊢ \forall y (y = Y \to ((y \in C \to \neg B \subseteq D) \to (Y \in C \to \neg B \subseteq G))) \to (Y \in C \to (\forall y (y \in C \to \neg B \subseteq D) \to (Y \in C \to \neg B \subseteq G)))$
31	25 10 30	sylc	$⊢ (φ \land x \in A) \to (\forall y (y \in C \to \neg B \subseteq D) \to (Y \in C \to \neg B \subseteq G))$
32	10 31	mpid	$⊢ (φ \land x \in A) \to (\forall y (y \in C \to \neg B \subseteq D) \to \neg B \subseteq G)$
33	13 32	syl5bi	$⊢ (φ \land x \in A) \to (\forall y \in C \neg B \subseteq D \to \neg B \subseteq G)$
34	33	con2d	$⊢ (φ \land x \in A) \to (B \subseteq G \to \neg \forall y \in C \neg B \subseteq D)$
35		dfrex2	$⊢ \exists y \in C B \subseteq D \leftrightarrow \neg \forall y \in C \neg B \subseteq D$
36	34 35	syl6ibr	$⊢ (φ \land x \in A) \to (B \subseteq G \to \exists y \in C B \subseteq D)$
37	12 36	mpd	$⊢ (φ \land x \in A) \to \exists y \in C B \subseteq D$
38	37	ex	$⊢ φ \to (x \in A \to \exists y \in C B \subseteq D)$
39	1 38	ralrimi	$⊢ φ \to \forall x \in A \exists y \in C B \subseteq D$
40		ssel	$⊢ B \subseteq D \to (z \in B \to z \in D)$
41	40	reximi	$⊢ \exists y \in C B \subseteq D \to \exists y \in C (z \in B \to z \in D)$
42	5	nfcri	$⊢ Ⅎ y z \in B$
43	42	r19.37	$⊢ \exists y \in C (z \in B \to z \in D) \to (z \in B \to \exists y \in C z \in D)$
44	41 43	syl	$⊢ \exists y \in C B \subseteq D \to (z \in B \to \exists y \in C z \in D)$
45		eliun	$⊢ z \in ⋃_{y \in C} D \leftrightarrow \exists y \in C z \in D$
46	44 45	syl6ibr	$⊢ \exists y \in C B \subseteq D \to (z \in B \to z \in ⋃_{y \in C} D)$
47	46	ssrdv	$⊢ \exists y \in C B \subseteq D \to B \subseteq ⋃_{y \in C} D$
48	47	ralimi	$⊢ \forall x \in A \exists y \in C B \subseteq D \to \forall x \in A B \subseteq ⋃_{y \in C} D$
49		df-iun	$⊢ ⋃_{x \in A} B = \{z \| \exists x \in A z \in B\}$
50	49	sseq1i	$⊢ ⋃_{x \in A} B \subseteq ⋃_{y \in C} D \leftrightarrow \{z \| \exists x \in A z \in B\} \subseteq ⋃_{y \in C} D$
51		abss	$⊢ \{z \| \exists x \in A z \in B\} \subseteq ⋃_{y \in C} D \leftrightarrow \forall z (\exists x \in A z \in B \to z \in ⋃_{y \in C} D)$
52		dfss2	$⊢ B \subseteq ⋃_{y \in C} D \leftrightarrow \forall z (z \in B \to z \in ⋃_{y \in C} D)$
53	52	ralbii	$⊢ \forall x \in A B \subseteq ⋃_{y \in C} D \leftrightarrow \forall x \in A \forall z (z \in B \to z \in ⋃_{y \in C} D)$
54		ralcom4	$⊢ \forall x \in A \forall z (z \in B \to z \in ⋃_{y \in C} D) \leftrightarrow \forall z \forall x \in A (z \in B \to z \in ⋃_{y \in C} D)$
55	6 8	nfiun	$⊢ \underline{Ⅎ} x ⋃_{y \in C} D$
56	55	nfcri	$⊢ Ⅎ x z \in ⋃_{y \in C} D$
57	56	r19.23	$⊢ \forall x \in A (z \in B \to z \in ⋃_{y \in C} D) \leftrightarrow (\exists x \in A z \in B \to z \in ⋃_{y \in C} D)$
58	57	albii	$⊢ \forall z \forall x \in A (z \in B \to z \in ⋃_{y \in C} D) \leftrightarrow \forall z (\exists x \in A z \in B \to z \in ⋃_{y \in C} D)$
59	53 54 58	3bitrri	$⊢ \forall z (\exists x \in A z \in B \to z \in ⋃_{y \in C} D) \leftrightarrow \forall x \in A B \subseteq ⋃_{y \in C} D$
60	50 51 59	3bitri	$⊢ ⋃_{x \in A} B \subseteq ⋃_{y \in C} D \leftrightarrow \forall x \in A B \subseteq ⋃_{y \in C} D$
61	48 60	sylibr	$⊢ \forall x \in A \exists y \in C B \subseteq D \to ⋃_{x \in A} B \subseteq ⋃_{y \in C} D$
62	39 61	syl	$⊢ φ \to ⋃_{x \in A} B \subseteq ⋃_{y \in C} D$

Metamath Proof Explorer

Theorem ss2iundf

Proof