Theorem onfununi 7784

Description: A property of functions on ordinal numbers. Generalization of Theorem Schema 8E of [Enderton] p. 218. (Contributed by Eric Schmidt, 26-May-2009.)

Hypotheses

Ref	Expression
onfununi.1	⊢ (Lim 𝑦 → (𝐹‘𝑦) = ∪ 𝑥 ∈ 𝑦 (𝐹‘𝑥))
onfununi.2	⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑥 ⊆ 𝑦) → (𝐹‘𝑥) ⊆ (𝐹‘𝑦))

Assertion

Ref	Expression
onfununi	⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))

Distinct variable groups:   𝑥,𝑦,𝑆   𝑥,𝐹,𝑦   𝑥,𝑇

Allowed substitution hint:   𝑇(𝑦)

Proof of Theorem onfununi

Step	Hyp	Ref	Expression
1		ssorduni 7318	. . . . . . . . . 10 ⊢ (𝑆 ⊆ On → Ord ∪ 𝑆)
2	1	ad2antrr 713	. . . . . . . . 9 ⊢ (((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) ∧ 𝑆 ≠ ∅) → Ord ∪ 𝑆)
3		nelneq 2890	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝑆 ∧ ¬ ∪ 𝑆 ∈ 𝑆) → ¬ 𝑥 = ∪ 𝑆)
4		elssuni 4742	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ 𝑆 → 𝑥 ⊆ ∪ 𝑆)
5	4	adantl 474	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → 𝑥 ⊆ ∪ 𝑆)
6		ssel 3854	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑆 ⊆ On → (𝑥 ∈ 𝑆 → 𝑥 ∈ On))
7		eloni 6041	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ On → Ord 𝑥)
8	6, 7	syl6 35	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑆 ⊆ On → (𝑥 ∈ 𝑆 → Ord 𝑥))
9	8	imp 398	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → Ord 𝑥)
10		ordsseleq 6060	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((Ord 𝑥 ∧ Ord ∪ 𝑆) → (𝑥 ⊆ ∪ 𝑆 ↔ (𝑥 ∈ ∪ 𝑆 ∨ 𝑥 = ∪ 𝑆)))
11	9, 1, 10	syl2an 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) ∧ 𝑆 ⊆ On) → (𝑥 ⊆ ∪ 𝑆 ↔ (𝑥 ∈ ∪ 𝑆 ∨ 𝑥 = ∪ 𝑆)))
12	11	anabss1 653	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → (𝑥 ⊆ ∪ 𝑆 ↔ (𝑥 ∈ ∪ 𝑆 ∨ 𝑥 = ∪ 𝑆)))
13	5, 12	mpbid 224	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → (𝑥 ∈ ∪ 𝑆 ∨ 𝑥 = ∪ 𝑆))
14	13	ord 850	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → (¬ 𝑥 ∈ ∪ 𝑆 → 𝑥 = ∪ 𝑆))
15	14	con1d 142	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → (¬ 𝑥 = ∪ 𝑆 → 𝑥 ∈ ∪ 𝑆))
16	3, 15	syl5 34	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → ((𝑥 ∈ 𝑆 ∧ ¬ ∪ 𝑆 ∈ 𝑆) → 𝑥 ∈ ∪ 𝑆))
17	16	exp4b 423	. . . . . . . . . . . . . 14 ⊢ (𝑆 ⊆ On → (𝑥 ∈ 𝑆 → (𝑥 ∈ 𝑆 → (¬ ∪ 𝑆 ∈ 𝑆 → 𝑥 ∈ ∪ 𝑆))))
18	17	pm2.43d 53	. . . . . . . . . . . . 13 ⊢ (𝑆 ⊆ On → (𝑥 ∈ 𝑆 → (¬ ∪ 𝑆 ∈ 𝑆 → 𝑥 ∈ ∪ 𝑆)))
19	18	com23 86	. . . . . . . . . . . 12 ⊢ (𝑆 ⊆ On → (¬ ∪ 𝑆 ∈ 𝑆 → (𝑥 ∈ 𝑆 → 𝑥 ∈ ∪ 𝑆)))
20	19	imp 398	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) → (𝑥 ∈ 𝑆 → 𝑥 ∈ ∪ 𝑆))
21	20	ssrdv 3866	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) → 𝑆 ⊆ ∪ 𝑆)
22		ssn0 4241	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ ∪ 𝑆 ∧ 𝑆 ≠ ∅) → ∪ 𝑆 ≠ ∅)
23	21, 22	sylan 572	. . . . . . . . 9 ⊢ (((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) ∧ 𝑆 ≠ ∅) → ∪ 𝑆 ≠ ∅)
24	21	unissd 4737	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) → ∪ 𝑆 ⊆ ∪ ∪ 𝑆)
25		orduniss 6125	. . . . . . . . . . . . 13 ⊢ (Ord ∪ 𝑆 → ∪ ∪ 𝑆 ⊆ ∪ 𝑆)
26	1, 25	syl 17	. . . . . . . . . . . 12 ⊢ (𝑆 ⊆ On → ∪ ∪ 𝑆 ⊆ ∪ 𝑆)
27	26	adantr 473	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) → ∪ ∪ 𝑆 ⊆ ∪ 𝑆)
28	24, 27	eqssd 3877	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) → ∪ 𝑆 = ∪ ∪ 𝑆)
29	28	adantr 473	. . . . . . . . 9 ⊢ (((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) ∧ 𝑆 ≠ ∅) → ∪ 𝑆 = ∪ ∪ 𝑆)
30		df-lim 6036	. . . . . . . . 9 ⊢ (Lim ∪ 𝑆 ↔ (Ord ∪ 𝑆 ∧ ∪ 𝑆 ≠ ∅ ∧ ∪ 𝑆 = ∪ ∪ 𝑆))
31	2, 23, 29, 30	syl3anbrc 1323	. . . . . . . 8 ⊢ (((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) ∧ 𝑆 ≠ ∅) → Lim ∪ 𝑆)
32	31	an32s 639	. . . . . . 7 ⊢ (((𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆 ∈ 𝑆) → Lim ∪ 𝑆)
33	32	3adantl1 1146	. . . . . 6 ⊢ (((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆 ∈ 𝑆) → Lim ∪ 𝑆)
34		ssonuni 7319	. . . . . . . . . 10 ⊢ (𝑆 ∈ 𝑇 → (𝑆 ⊆ On → ∪ 𝑆 ∈ On))
35		limeq 6043	. . . . . . . . . . . 12 ⊢ (𝑦 = ∪ 𝑆 → (Lim 𝑦 ↔ Lim ∪ 𝑆))
36		fveq2 6501	. . . . . . . . . . . . 13 ⊢ (𝑦 = ∪ 𝑆 → (𝐹‘𝑦) = (𝐹‘∪ 𝑆))
37		iuneq1 4808	. . . . . . . . . . . . 13 ⊢ (𝑦 = ∪ 𝑆 → ∪ 𝑥 ∈ 𝑦 (𝐹‘𝑥) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥))
38	36, 37	eqeq12d 2793	. . . . . . . . . . . 12 ⊢ (𝑦 = ∪ 𝑆 → ((𝐹‘𝑦) = ∪ 𝑥 ∈ 𝑦 (𝐹‘𝑥) ↔ (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥)))
39	35, 38	imbi12d 337	. . . . . . . . . . 11 ⊢ (𝑦 = ∪ 𝑆 → ((Lim 𝑦 → (𝐹‘𝑦) = ∪ 𝑥 ∈ 𝑦 (𝐹‘𝑥)) ↔ (Lim ∪ 𝑆 → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥))))
40		onfununi.1	. . . . . . . . . . 11 ⊢ (Lim 𝑦 → (𝐹‘𝑦) = ∪ 𝑥 ∈ 𝑦 (𝐹‘𝑥))
41	39, 40	vtoclg 3486	. . . . . . . . . 10 ⊢ (∪ 𝑆 ∈ On → (Lim ∪ 𝑆 → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥)))
42	34, 41	syl6 35	. . . . . . . . 9 ⊢ (𝑆 ∈ 𝑇 → (𝑆 ⊆ On → (Lim ∪ 𝑆 → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥))))
43	42	imp 398	. . . . . . . 8 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On) → (Lim ∪ 𝑆 → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥)))
44	43	3adant3 1112	. . . . . . 7 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (Lim ∪ 𝑆 → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥)))
45	44	adantr 473	. . . . . 6 ⊢ (((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆 ∈ 𝑆) → (Lim ∪ 𝑆 → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥)))
46	33, 45	mpd 15	. . . . 5 ⊢ (((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆 ∈ 𝑆) → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥))
47		eluni2 4717	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ∪ 𝑆 ↔ ∃𝑦 ∈ 𝑆 𝑥 ∈ 𝑦)
48		ssel 3854	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆 ⊆ On → (𝑦 ∈ 𝑆 → 𝑦 ∈ On))
49	48	anim1d 601	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → (𝑦 ∈ On ∧ 𝑥 ∈ 𝑦)))
50		onelon 6056	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ On)
51	49, 50	syl6 35	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ On))
52	48	adantrd 484	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → 𝑦 ∈ On))
53		eloni 6041	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ On → Ord 𝑦)
54	48, 53	syl6 35	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ⊆ On → (𝑦 ∈ 𝑆 → Ord 𝑦))
55		ordelss 6047	. . . . . . . . . . . . . . . . . 18 ⊢ ((Ord 𝑦 ∧ 𝑥 ∈ 𝑦) → 𝑥 ⊆ 𝑦)
56	55	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ⊆ On → ((Ord 𝑦 ∧ 𝑥 ∈ 𝑦) → 𝑥 ⊆ 𝑦))
57	54, 56	syland 593	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → 𝑥 ⊆ 𝑦))
58	51, 52, 57	3jcad 1109	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → (𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑥 ⊆ 𝑦)))
59		onfununi.2	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑥 ⊆ 𝑦) → (𝐹‘𝑥) ⊆ (𝐹‘𝑦))
60	58, 59	syl6 35	. . . . . . . . . . . . . 14 ⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → (𝐹‘𝑥) ⊆ (𝐹‘𝑦)))
61	60	expd 408	. . . . . . . . . . . . 13 ⊢ (𝑆 ⊆ On → (𝑦 ∈ 𝑆 → (𝑥 ∈ 𝑦 → (𝐹‘𝑥) ⊆ (𝐹‘𝑦))))
62	61	reximdvai 3217	. . . . . . . . . . . 12 ⊢ (𝑆 ⊆ On → (∃𝑦 ∈ 𝑆 𝑥 ∈ 𝑦 → ∃𝑦 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘𝑦)))
63	47, 62	syl5bi 234	. . . . . . . . . . 11 ⊢ (𝑆 ⊆ On → (𝑥 ∈ ∪ 𝑆 → ∃𝑦 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘𝑦)))
64		ssiun 4837	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘𝑦) → (𝐹‘𝑥) ⊆ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦))
65	63, 64	syl6 35	. . . . . . . . . 10 ⊢ (𝑆 ⊆ On → (𝑥 ∈ ∪ 𝑆 → (𝐹‘𝑥) ⊆ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦)))
66	65	ralrimiv 3131	. . . . . . . . 9 ⊢ (𝑆 ⊆ On → ∀𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦))
67		iunss 4836	. . . . . . . . 9 ⊢ (∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦) ↔ ∀𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦))
68	66, 67	sylibr 226	. . . . . . . 8 ⊢ (𝑆 ⊆ On → ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦))
69		fveq2 6501	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥))
70	69	cbviunv 4834	. . . . . . . 8 ⊢ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦) = ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥)
71	68, 70	syl6sseq 3909	. . . . . . 7 ⊢ (𝑆 ⊆ On → ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))
72	71	3ad2ant2 1114	. . . . . 6 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))
73	72	adantr 473	. . . . 5 ⊢ (((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆 ∈ 𝑆) → ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))
74	46, 73	eqsstrd 3897	. . . 4 ⊢ (((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆 ∈ 𝑆) → (𝐹‘∪ 𝑆) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))
75	74	ex 405	. . 3 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (¬ ∪ 𝑆 ∈ 𝑆 → (𝐹‘∪ 𝑆) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥)))
76		fveq2 6501	. . . 4 ⊢ (𝑥 = ∪ 𝑆 → (𝐹‘𝑥) = (𝐹‘∪ 𝑆))
77	76	ssiun2s 4839	. . 3 ⊢ (∪ 𝑆 ∈ 𝑆 → (𝐹‘∪ 𝑆) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))
78	75, 77	pm2.61d2 174	. 2 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝐹‘∪ 𝑆) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))
79	34	imp 398	. . . . . 6 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On) → ∪ 𝑆 ∈ On)
80	79	3adant3 1112	. . . . 5 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → ∪ 𝑆 ∈ On)
81	6	3ad2ant2 1114	. . . . . 6 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝑥 ∈ 𝑆 → 𝑥 ∈ On))
82	81, 4	jca2 506	. . . . 5 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝑥 ∈ 𝑆 → (𝑥 ∈ On ∧ 𝑥 ⊆ ∪ 𝑆)))
83		sseq2 3885	. . . . . . . 8 ⊢ (𝑦 = ∪ 𝑆 → (𝑥 ⊆ 𝑦 ↔ 𝑥 ⊆ ∪ 𝑆))
84	83	anbi2d 619	. . . . . . 7 ⊢ (𝑦 = ∪ 𝑆 → ((𝑥 ∈ On ∧ 𝑥 ⊆ 𝑦) ↔ (𝑥 ∈ On ∧ 𝑥 ⊆ ∪ 𝑆)))
85	36	sseq2d 3891	. . . . . . 7 ⊢ (𝑦 = ∪ 𝑆 → ((𝐹‘𝑥) ⊆ (𝐹‘𝑦) ↔ (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆)))
86	84, 85	imbi12d 337	. . . . . 6 ⊢ (𝑦 = ∪ 𝑆 → (((𝑥 ∈ On ∧ 𝑥 ⊆ 𝑦) → (𝐹‘𝑥) ⊆ (𝐹‘𝑦)) ↔ ((𝑥 ∈ On ∧ 𝑥 ⊆ ∪ 𝑆) → (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆))))
87	59	3com12 1103	. . . . . . 7 ⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ On ∧ 𝑥 ⊆ 𝑦) → (𝐹‘𝑥) ⊆ (𝐹‘𝑦))
88	87	3expib 1102	. . . . . 6 ⊢ (𝑦 ∈ On → ((𝑥 ∈ On ∧ 𝑥 ⊆ 𝑦) → (𝐹‘𝑥) ⊆ (𝐹‘𝑦)))
89	86, 88	vtoclga 3493	. . . . 5 ⊢ (∪ 𝑆 ∈ On → ((𝑥 ∈ On ∧ 𝑥 ⊆ ∪ 𝑆) → (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆)))
90	80, 82, 89	sylsyld 61	. . . 4 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝑥 ∈ 𝑆 → (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆)))
91	90	ralrimiv 3131	. . 3 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → ∀𝑥 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆))
92		iunss 4836	. . 3 ⊢ (∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆) ↔ ∀𝑥 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆))
93	91, 92	sylibr 226	. 2 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆))
94	78, 93	eqssd 3877	1 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 387   ∨ wo 833   ∧ w3a 1068   = wceq 1507   ∈ wcel 2050   ≠ wne 2967  ∀wral 3088  ∃wrex 3089   ⊆ wss 3831  ∅c0 4180  ∪ cuni 4713  ∪ ciun 4793  Ord word 6030  Oncon0 6031  Lim wlim 6032  ‘cfv 6190

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5061  ax-nul 5068  ax-pr 5187  ax-un 7281

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2583  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-sbc 3684  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-pss 3847  df-nul 4181  df-if 4352  df-sn 4443  df-pr 4445  df-tp 4447  df-op 4449  df-uni 4714  df-iun 4795  df-br 4931  df-opab 4993  df-tr 5032  df-eprel 5318  df-po 5327  df-so 5328  df-fr 5367  df-we 5369  df-ord 6034  df-on 6035  df-lim 6036  df-iota 6154  df-fv 6198

This theorem is referenced by:  onovuni  7785