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	spcimgft	⊢ ( ∀ 𝑦 ( 𝑦 = 𝑌 → ( ( 𝑦 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐷 ) → ( 𝑌 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐺 ) ) ) → ( 𝑌 ∈ 𝐶 → ( ∀ 𝑦 ( 𝑦 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐷 ) → ( 𝑌 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐺 ) ) ) )
31	25 10 30	sylc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ( 𝑦 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐷 ) → ( 𝑌 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐺 ) ) )
32	10 31	mpid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ( 𝑦 ∈ 𝐶 → ¬ 𝐵 ⊆ 𝐷 ) → ¬ 𝐵 ⊆ 𝐺 ) )
33	13 32	syl5bi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐶 ¬ 𝐵 ⊆ 𝐷 → ¬ 𝐵 ⊆ 𝐺 ) )
34	33	con2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ⊆ 𝐺 → ¬ ∀ 𝑦 ∈ 𝐶 ¬ 𝐵 ⊆ 𝐷 ) )
35		dfrex2	⊢ ( ∃ 𝑦 ∈ 𝐶 𝐵 ⊆ 𝐷 ↔ ¬ ∀ 𝑦 ∈ 𝐶 ¬ 𝐵 ⊆ 𝐷 )
36	34 35	syl6ibr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ⊆ 𝐺 → ∃ 𝑦 ∈ 𝐶 𝐵 ⊆ 𝐷 ) )
37	12 36	mpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝐶 𝐵 ⊆ 𝐷 )
38	37	ex	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ∃ 𝑦 ∈ 𝐶 𝐵 ⊆ 𝐷 ) )
39	1 38	ralrimi	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝐵 ⊆ 𝐷 )
40		ssel	⊢ ( 𝐵 ⊆ 𝐷 → ( 𝑧 ∈ 𝐵 → 𝑧 ∈ 𝐷 ) )
41	40	reximi	⊢ ( ∃ 𝑦 ∈ 𝐶 𝐵 ⊆ 𝐷 → ∃ 𝑦 ∈ 𝐶 ( 𝑧 ∈ 𝐵 → 𝑧 ∈ 𝐷 ) )
42	5	nfcri	⊢ Ⅎ 𝑦 𝑧 ∈ 𝐵
43	42	r19.37	⊢ ( ∃ 𝑦 ∈ 𝐶 ( 𝑧 ∈ 𝐵 → 𝑧 ∈ 𝐷 ) → ( 𝑧 ∈ 𝐵 → ∃ 𝑦 ∈ 𝐶 𝑧 ∈ 𝐷 ) )
44	41 43	syl	⊢ ( ∃ 𝑦 ∈ 𝐶 𝐵 ⊆ 𝐷 → ( 𝑧 ∈ 𝐵 → ∃ 𝑦 ∈ 𝐶 𝑧 ∈ 𝐷 ) )
45		eliun	⊢ ( 𝑧 ∈ ∪ 𝑦 ∈ 𝐶 𝐷 ↔ ∃ 𝑦 ∈ 𝐶 𝑧 ∈ 𝐷 )
46	44 45	syl6ibr	⊢ ( ∃ 𝑦 ∈ 𝐶 𝐵 ⊆ 𝐷 → ( 𝑧 ∈ 𝐵 → 𝑧 ∈ ∪ 𝑦 ∈ 𝐶 𝐷 ) )
47	46	ssrdv	⊢ ( ∃ 𝑦 ∈ 𝐶 𝐵 ⊆ 𝐷 → 𝐵 ⊆ ∪ 𝑦 ∈ 𝐶 𝐷 )
48	47	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝐵 ⊆ 𝐷 → ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑦 ∈ 𝐶 𝐷 )
49		df-iun	⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 }
50	49	sseq1i	⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑦 ∈ 𝐶 𝐷 ↔ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 } ⊆ ∪ 𝑦 ∈ 𝐶 𝐷 )
51		abss	⊢ ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 } ⊆ ∪ 𝑦 ∈ 𝐶 𝐷 ↔ ∀ 𝑧 ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 → 𝑧 ∈ ∪ 𝑦 ∈ 𝐶 𝐷 ) )
52		dfss2	⊢ ( 𝐵 ⊆ ∪ 𝑦 ∈ 𝐶 𝐷 ↔ ∀ 𝑧 ( 𝑧 ∈ 𝐵 → 𝑧 ∈ ∪ 𝑦 ∈ 𝐶 𝐷 ) )
53	52	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑦 ∈ 𝐶 𝐷 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ( 𝑧 ∈ 𝐵 → 𝑧 ∈ ∪ 𝑦 ∈ 𝐶 𝐷 ) )
54		ralcom4	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ( 𝑧 ∈ 𝐵 → 𝑧 ∈ ∪ 𝑦 ∈ 𝐶 𝐷 ) ↔ ∀ 𝑧 ∀ 𝑥 ∈ 𝐴 ( 𝑧 ∈ 𝐵 → 𝑧 ∈ ∪ 𝑦 ∈ 𝐶 𝐷 ) )
55	6 8	nfiun	⊢ Ⅎ 𝑥 ∪ 𝑦 ∈ 𝐶 𝐷
56	55	nfcri	⊢ Ⅎ 𝑥 𝑧 ∈ ∪ 𝑦 ∈ 𝐶 𝐷
57	56	r19.23	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑧 ∈ 𝐵 → 𝑧 ∈ ∪ 𝑦 ∈ 𝐶 𝐷 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 → 𝑧 ∈ ∪ 𝑦 ∈ 𝐶 𝐷 ) )
58	57	albii	⊢ ( ∀ 𝑧 ∀ 𝑥 ∈ 𝐴 ( 𝑧 ∈ 𝐵 → 𝑧 ∈ ∪ 𝑦 ∈ 𝐶 𝐷 ) ↔ ∀ 𝑧 ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 → 𝑧 ∈ ∪ 𝑦 ∈ 𝐶 𝐷 ) )
59	53 54 58	3bitrri	⊢ ( ∀ 𝑧 ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 → 𝑧 ∈ ∪ 𝑦 ∈ 𝐶 𝐷 ) ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑦 ∈ 𝐶 𝐷 )
60	50 51 59	3bitri	⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑦 ∈ 𝐶 𝐷 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑦 ∈ 𝐶 𝐷 )
61	48 60	sylibr	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝐵 ⊆ 𝐷 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑦 ∈ 𝐶 𝐷 )
62	39 61	syl	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ∪ 𝑦 ∈ 𝐶 𝐷 )