Theorem ss2iundf

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

	Ref	Expression
Hypotheses	ss2iundf.xph	⊢ Ⅎ 𝑥 𝜑
	ss2iundf.yph	⊢ Ⅎ 𝑦 𝜑
	ss2iundf.y	⊢ Ⅎ 𝑦 𝑌
	ss2iundf.a	⊢ Ⅎ 𝑦 𝐴
	ss2iundf.b	⊢ Ⅎ 𝑦 𝐵
	ss2iundf.xc	⊢ Ⅎ 𝑥 𝐶
	ss2iundf.yc	⊢ Ⅎ 𝑦 𝐶
	ss2iundf.d	⊢ Ⅎ 𝑥 𝐷
	ss2iundf.g	⊢ Ⅎ 𝑦 𝐺
	ss2iundf.el	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑌 ∈ 𝐶 )
	ss2iundf.sub	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑌 ) → 𝐷 = 𝐺 )
	ss2iundf.ss	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ⊆ 𝐺 )
Assertion	ss2iundf	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑦 ∈ 𝐶 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		ss2iundf.xph	⊢ Ⅎ 𝑥 𝜑
2		ss2iundf.yph	⊢ Ⅎ 𝑦 𝜑
3		ss2iundf.y	⊢ Ⅎ 𝑦 𝑌
4		ss2iundf.a	⊢ Ⅎ 𝑦 𝐴
5		ss2iundf.b	⊢ Ⅎ 𝑦 𝐵
6		ss2iundf.xc	⊢ Ⅎ 𝑥 𝐶
7		ss2iundf.yc	⊢ Ⅎ 𝑦 𝐶
8		ss2iundf.d	⊢ Ⅎ 𝑥 𝐷
9		ss2iundf.g	⊢ Ⅎ 𝑦 𝐺
10		ss2iundf.el	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑌 ∈ 𝐶 )
11		ss2iundf.sub	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑌 ) → 𝐷 = 𝐺 )
12		ss2iundf.ss	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ⊆ 𝐺 )
13		df-ral	⊢ ( ∀ 𝑦 ∈ 𝐶 ¬ 𝐵 ⊆ 𝐷 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐷 ) )
14	4	nfcri	⊢ Ⅎ 𝑦 𝑥 ∈ 𝐴
15	2 14	nfan	⊢ Ⅎ 𝑦 ( 𝜑 ∧ 𝑥 ∈ 𝐴 )
16		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 = 𝑌 ) → 𝑦 = 𝑌 )
17	16	eleq1d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 = 𝑌 ) → ( 𝑦 ∈ 𝐶 ↔ 𝑌 ∈ 𝐶 ) )
18	17	biimprd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 = 𝑌 ) → ( 𝑌 ∈ 𝐶 → 𝑦 ∈ 𝐶 ) )
19	11	sseq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑌 ) → ( 𝐵 ⊆ 𝐷 ↔ 𝐵 ⊆ 𝐺 ) )
20	19	3expa	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 = 𝑌 ) → ( 𝐵 ⊆ 𝐷 ↔ 𝐵 ⊆ 𝐺 ) )
21	20	notbid	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 = 𝑌 ) → ( ¬ 𝐵 ⊆ 𝐷 ↔ ¬ 𝐵 ⊆ 𝐺 ) )
22	21	biimpd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 = 𝑌 ) → ( ¬ 𝐵 ⊆ 𝐷 → ¬ 𝐵 ⊆ 𝐺 ) )
23	18 22	imim12d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 = 𝑌 ) → ( ( 𝑦 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐷 ) → ( 𝑌 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐺 ) ) )
24	23	ex	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 = 𝑌 → ( ( 𝑦 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐷 ) → ( 𝑌 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐺 ) ) ) )
25	15 24	alrimi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑦 ( 𝑦 = 𝑌 → ( ( 𝑦 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐷 ) → ( 𝑌 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐺 ) ) ) )
26	3 7	nfel	⊢ Ⅎ 𝑦 𝑌 ∈ 𝐶
27	5 9	nfss	⊢ Ⅎ 𝑦 𝐵 ⊆ 𝐺
28	27	nfn	⊢ Ⅎ 𝑦 ¬ 𝐵 ⊆ 𝐺
29	26 28	nfim	⊢ Ⅎ 𝑦 ( 𝑌 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐺 )
30	29 3	spcimgfi1	⊢ ( ∀ 𝑦 ( 𝑦 = 𝑌 → ( ( 𝑦 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐷 ) → ( 𝑌 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐺 ) ) ) → ( 𝑌 ∈ 𝐶 → ( ∀ 𝑦 ( 𝑦 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐷 ) → ( 𝑌 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐺 ) ) ) )
31	25 10 30	sylc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ( 𝑦 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐷 ) → ( 𝑌 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐺 ) ) )
32	10 31	mpid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ( 𝑦 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐷 ) → ¬ 𝐵 ⊆ 𝐺 ) )
33	13 32	biimtrid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐶 ¬ 𝐵 ⊆ 𝐷 → ¬ 𝐵 ⊆ 𝐺 ) )
34	33	con2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ⊆ 𝐺 → ¬ ∀ 𝑦 ∈ 𝐶 ¬ 𝐵 ⊆ 𝐷 ) )
35		dfrex2	⊢ ( ∃ 𝑦 ∈ 𝐶 𝐵 ⊆ 𝐷 ↔ ¬ ∀ 𝑦 ∈ 𝐶 ¬ 𝐵 ⊆ 𝐷 )
36	34 35	imbitrrdi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ⊆ 𝐺 → ∃ 𝑦 ∈ 𝐶 𝐵 ⊆ 𝐷 ) )
37	12 36	mpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝐶 𝐵 ⊆ 𝐷 )
38	1 37	ralrimia	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝐵 ⊆ 𝐷 )
39		ssel	⊢ ( 𝐵 ⊆ 𝐷 → ( 𝑧 ∈ 𝐵 → 𝑧 ∈ 𝐷 ) )
40	39	reximi	⊢ ( ∃ 𝑦 ∈ 𝐶 𝐵 ⊆ 𝐷 → ∃ 𝑦 ∈ 𝐶 ( 𝑧 ∈ 𝐵 → 𝑧 ∈ 𝐷 ) )
41	5	nfcri	⊢ Ⅎ 𝑦 𝑧 ∈ 𝐵
42	41	r19.37	⊢ ( ∃ 𝑦 ∈ 𝐶 ( 𝑧 ∈ 𝐵 → 𝑧 ∈ 𝐷 ) → ( 𝑧 ∈ 𝐵 → ∃ 𝑦 ∈ 𝐶 𝑧 ∈ 𝐷 ) )
43	40 42	syl	⊢ ( ∃ 𝑦 ∈ 𝐶 𝐵 ⊆ 𝐷 → ( 𝑧 ∈ 𝐵 → ∃ 𝑦 ∈ 𝐶 𝑧 ∈ 𝐷 ) )
44		eliun	⊢ ( 𝑧 ∈ ∪ 𝑦 ∈ 𝐶 𝐷 ↔ ∃ 𝑦 ∈ 𝐶 𝑧 ∈ 𝐷 )
45	43 44	imbitrrdi	⊢ ( ∃ 𝑦 ∈ 𝐶 𝐵 ⊆ 𝐷 → ( 𝑧 ∈ 𝐵 → 𝑧 ∈ ∪ 𝑦 ∈ 𝐶 𝐷 ) )
46	45	ssrdv	⊢ ( ∃ 𝑦 ∈ 𝐶 𝐵 ⊆ 𝐷 → 𝐵 ⊆ ∪ 𝑦 ∈ 𝐶 𝐷 )
47	46	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝐵 ⊆ 𝐷 → ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑦 ∈ 𝐶 𝐷 )
48	6 8	nfiun	⊢ Ⅎ 𝑥 ∪ 𝑦 ∈ 𝐶 𝐷
49	48	iunssf	⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑦 ∈ 𝐶 𝐷 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑦 ∈ 𝐶 𝐷 )
50	47 49	sylibr	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝐵 ⊆ 𝐷 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑦 ∈ 𝐶 𝐷 )
51	38 50	syl	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑦 ∈ 𝐶 𝐷 )