Theorem onfununi 8292

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 7718	. . . . . . . . . 10 ⊢ (𝑆 ⊆ On → Ord ∪ 𝑆)
2	1	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) ∧ 𝑆 ≠ ∅) → Ord ∪ 𝑆)
3		nelneq 2856	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝑆 ∧ ¬ ∪ 𝑆 ∈ 𝑆) → ¬ 𝑥 = ∪ 𝑆)
4		elssuni 4903	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ 𝑆 → 𝑥 ⊆ ∪ 𝑆)
5	4	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → 𝑥 ⊆ ∪ 𝑆)
6		ssel 3940	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑆 ⊆ On → (𝑥 ∈ 𝑆 → 𝑥 ∈ On))
7		eloni 6332	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ On → Ord 𝑥)
8	6, 7	syl6 35	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑆 ⊆ On → (𝑥 ∈ 𝑆 → Ord 𝑥))
9	8	imp 407	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → Ord 𝑥)
10		ordsseleq 6351	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((Ord 𝑥 ∧ Ord ∪ 𝑆) → (𝑥 ⊆ ∪ 𝑆 ↔ (𝑥 ∈ ∪ 𝑆 ∨ 𝑥 = ∪ 𝑆)))
11	9, 1, 10	syl2an 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) ∧ 𝑆 ⊆ On) → (𝑥 ⊆ ∪ 𝑆 ↔ (𝑥 ∈ ∪ 𝑆 ∨ 𝑥 = ∪ 𝑆)))
12	11	anabss1 664	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → (𝑥 ⊆ ∪ 𝑆 ↔ (𝑥 ∈ ∪ 𝑆 ∨ 𝑥 = ∪ 𝑆)))
13	5, 12	mpbid 231	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → (𝑥 ∈ ∪ 𝑆 ∨ 𝑥 = ∪ 𝑆))
14	13	ord 862	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → (¬ 𝑥 ∈ ∪ 𝑆 → 𝑥 = ∪ 𝑆))
15	14	con1d 145	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → (¬ 𝑥 = ∪ 𝑆 → 𝑥 ∈ ∪ 𝑆))
16	3, 15	syl5 34	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → ((𝑥 ∈ 𝑆 ∧ ¬ ∪ 𝑆 ∈ 𝑆) → 𝑥 ∈ ∪ 𝑆))
17	16	exp4b 431	. . . . . . . . . . . . . 14 ⊢ (𝑆 ⊆ On → (𝑥 ∈ 𝑆 → (𝑥 ∈ 𝑆 → (¬ ∪ 𝑆 ∈ 𝑆 → 𝑥 ∈ ∪ 𝑆))))
18	17	pm2.43d 53	. . . . . . . . . . . . 13 ⊢ (𝑆 ⊆ On → (𝑥 ∈ 𝑆 → (¬ ∪ 𝑆 ∈ 𝑆 → 𝑥 ∈ ∪ 𝑆)))
19	18	com23 86	. . . . . . . . . . . 12 ⊢ (𝑆 ⊆ On → (¬ ∪ 𝑆 ∈ 𝑆 → (𝑥 ∈ 𝑆 → 𝑥 ∈ ∪ 𝑆)))
20	19	imp 407	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) → (𝑥 ∈ 𝑆 → 𝑥 ∈ ∪ 𝑆))
21	20	ssrdv 3953	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) → 𝑆 ⊆ ∪ 𝑆)
22		ssn0 4365	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ ∪ 𝑆 ∧ 𝑆 ≠ ∅) → ∪ 𝑆 ≠ ∅)
23	21, 22	sylan 580	. . . . . . . . 9 ⊢ (((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) ∧ 𝑆 ≠ ∅) → ∪ 𝑆 ≠ ∅)
24	21	unissd 4880	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) → ∪ 𝑆 ⊆ ∪ ∪ 𝑆)
25		orduniss 6419	. . . . . . . . . . . . 13 ⊢ (Ord ∪ 𝑆 → ∪ ∪ 𝑆 ⊆ ∪ 𝑆)
26	1, 25	syl 17	. . . . . . . . . . . 12 ⊢ (𝑆 ⊆ On → ∪ ∪ 𝑆 ⊆ ∪ 𝑆)
27	26	adantr 481	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) → ∪ ∪ 𝑆 ⊆ ∪ 𝑆)
28	24, 27	eqssd 3964	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) → ∪ 𝑆 = ∪ ∪ 𝑆)
29	28	adantr 481	. . . . . . . . 9 ⊢ (((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) ∧ 𝑆 ≠ ∅) → ∪ 𝑆 = ∪ ∪ 𝑆)
30		df-lim 6327	. . . . . . . . 9 ⊢ (Lim ∪ 𝑆 ↔ (Ord ∪ 𝑆 ∧ ∪ 𝑆 ≠ ∅ ∧ ∪ 𝑆 = ∪ ∪ 𝑆))
31	2, 23, 29, 30	syl3anbrc 1343	. . . . . . . 8 ⊢ (((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) ∧ 𝑆 ≠ ∅) → Lim ∪ 𝑆)
32	31	an32s 650	. . . . . . 7 ⊢ (((𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆 ∈ 𝑆) → Lim ∪ 𝑆)
33	32	3adantl1 1166	. . . . . 6 ⊢ (((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆 ∈ 𝑆) → Lim ∪ 𝑆)
34		ssonuni 7719	. . . . . . . . . 10 ⊢ (𝑆 ∈ 𝑇 → (𝑆 ⊆ On → ∪ 𝑆 ∈ On))
35		limeq 6334	. . . . . . . . . . . 12 ⊢ (𝑦 = ∪ 𝑆 → (Lim 𝑦 ↔ Lim ∪ 𝑆))
36		fveq2 6847	. . . . . . . . . . . . 13 ⊢ (𝑦 = ∪ 𝑆 → (𝐹‘𝑦) = (𝐹‘∪ 𝑆))
37		iuneq1 4975	. . . . . . . . . . . . 13 ⊢ (𝑦 = ∪ 𝑆 → ∪ 𝑥 ∈ 𝑦 (𝐹‘𝑥) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥))
38	36, 37	eqeq12d 2747	. . . . . . . . . . . 12 ⊢ (𝑦 = ∪ 𝑆 → ((𝐹‘𝑦) = ∪ 𝑥 ∈ 𝑦 (𝐹‘𝑥) ↔ (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥)))
39	35, 38	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑦 = ∪ 𝑆 → ((Lim 𝑦 → (𝐹‘𝑦) = ∪ 𝑥 ∈ 𝑦 (𝐹‘𝑥)) ↔ (Lim ∪ 𝑆 → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥))))
40		onfununi.1	. . . . . . . . . . 11 ⊢ (Lim 𝑦 → (𝐹‘𝑦) = ∪ 𝑥 ∈ 𝑦 (𝐹‘𝑥))
41	39, 40	vtoclg 3526	. . . . . . . . . 10 ⊢ (∪ 𝑆 ∈ On → (Lim ∪ 𝑆 → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥)))
42	34, 41	syl6 35	. . . . . . . . 9 ⊢ (𝑆 ∈ 𝑇 → (𝑆 ⊆ On → (Lim ∪ 𝑆 → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥))))
43	42	imp 407	. . . . . . . 8 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On) → (Lim ∪ 𝑆 → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥)))
44	43	3adant3 1132	. . . . . . 7 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (Lim ∪ 𝑆 → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥)))
45	44	adantr 481	. . . . . 6 ⊢ (((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆 ∈ 𝑆) → (Lim ∪ 𝑆 → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥)))
46	33, 45	mpd 15	. . . . 5 ⊢ (((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆 ∈ 𝑆) → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥))
47		eluni2 4874	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ∪ 𝑆 ↔ ∃𝑦 ∈ 𝑆 𝑥 ∈ 𝑦)
48		ssel 3940	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆 ⊆ On → (𝑦 ∈ 𝑆 → 𝑦 ∈ On))
49	48	anim1d 611	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → (𝑦 ∈ On ∧ 𝑥 ∈ 𝑦)))
50		onelon 6347	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ On)
51	49, 50	syl6 35	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ On))
52	48	adantrd 492	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → 𝑦 ∈ On))
53		eloni 6332	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ On → Ord 𝑦)
54	48, 53	syl6 35	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ⊆ On → (𝑦 ∈ 𝑆 → Ord 𝑦))
55		ordelss 6338	. . . . . . . . . . . . . . . . . 18 ⊢ ((Ord 𝑦 ∧ 𝑥 ∈ 𝑦) → 𝑥 ⊆ 𝑦)
56	55	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ⊆ On → ((Ord 𝑦 ∧ 𝑥 ∈ 𝑦) → 𝑥 ⊆ 𝑦))
57	54, 56	syland 603	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → 𝑥 ⊆ 𝑦))
58	51, 52, 57	3jcad 1129	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → (𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑥 ⊆ 𝑦)))
59		onfununi.2	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑥 ⊆ 𝑦) → (𝐹‘𝑥) ⊆ (𝐹‘𝑦))
60	58, 59	syl6 35	. . . . . . . . . . . . . 14 ⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → (𝐹‘𝑥) ⊆ (𝐹‘𝑦)))
61	60	expd 416	. . . . . . . . . . . . 13 ⊢ (𝑆 ⊆ On → (𝑦 ∈ 𝑆 → (𝑥 ∈ 𝑦 → (𝐹‘𝑥) ⊆ (𝐹‘𝑦))))
62	61	reximdvai 3158	. . . . . . . . . . . 12 ⊢ (𝑆 ⊆ On → (∃𝑦 ∈ 𝑆 𝑥 ∈ 𝑦 → ∃𝑦 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘𝑦)))
63	47, 62	biimtrid 241	. . . . . . . . . . 11 ⊢ (𝑆 ⊆ On → (𝑥 ∈ ∪ 𝑆 → ∃𝑦 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘𝑦)))
64		ssiun 5011	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘𝑦) → (𝐹‘𝑥) ⊆ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦))
65	63, 64	syl6 35	. . . . . . . . . 10 ⊢ (𝑆 ⊆ On → (𝑥 ∈ ∪ 𝑆 → (𝐹‘𝑥) ⊆ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦)))
66	65	ralrimiv 3138	. . . . . . . . 9 ⊢ (𝑆 ⊆ On → ∀𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦))
67		iunss 5010	. . . . . . . . 9 ⊢ (∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦) ↔ ∀𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦))
68	66, 67	sylibr 233	. . . . . . . 8 ⊢ (𝑆 ⊆ On → ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦))
69		fveq2 6847	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥))
70	69	cbviunv 5005	. . . . . . . 8 ⊢ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦) = ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥)
71	68, 70	sseqtrdi 3997	. . . . . . 7 ⊢ (𝑆 ⊆ On → ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))
72	71	3ad2ant2 1134	. . . . . 6 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))
73	72	adantr 481	. . . . 5 ⊢ (((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆 ∈ 𝑆) → ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))
74	46, 73	eqsstrd 3985	. . . 4 ⊢ (((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆 ∈ 𝑆) → (𝐹‘∪ 𝑆) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))
75	74	ex 413	. . 3 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (¬ ∪ 𝑆 ∈ 𝑆 → (𝐹‘∪ 𝑆) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥)))
76		fveq2 6847	. . . 4 ⊢ (𝑥 = ∪ 𝑆 → (𝐹‘𝑥) = (𝐹‘∪ 𝑆))
77	76	ssiun2s 5013	. . 3 ⊢ (∪ 𝑆 ∈ 𝑆 → (𝐹‘∪ 𝑆) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))
78	75, 77	pm2.61d2 181	. 2 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝐹‘∪ 𝑆) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))
79	34	imp 407	. . . . . 6 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On) → ∪ 𝑆 ∈ On)
80	79	3adant3 1132	. . . . 5 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → ∪ 𝑆 ∈ On)
81	6	3ad2ant2 1134	. . . . . 6 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝑥 ∈ 𝑆 → 𝑥 ∈ On))
82	81, 4	jca2 514	. . . . 5 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝑥 ∈ 𝑆 → (𝑥 ∈ On ∧ 𝑥 ⊆ ∪ 𝑆)))
83		sseq2 3973	. . . . . . . 8 ⊢ (𝑦 = ∪ 𝑆 → (𝑥 ⊆ 𝑦 ↔ 𝑥 ⊆ ∪ 𝑆))
84	83	anbi2d 629	. . . . . . 7 ⊢ (𝑦 = ∪ 𝑆 → ((𝑥 ∈ On ∧ 𝑥 ⊆ 𝑦) ↔ (𝑥 ∈ On ∧ 𝑥 ⊆ ∪ 𝑆)))
85	36	sseq2d 3979	. . . . . . 7 ⊢ (𝑦 = ∪ 𝑆 → ((𝐹‘𝑥) ⊆ (𝐹‘𝑦) ↔ (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆)))
86	84, 85	imbi12d 344	. . . . . 6 ⊢ (𝑦 = ∪ 𝑆 → (((𝑥 ∈ On ∧ 𝑥 ⊆ 𝑦) → (𝐹‘𝑥) ⊆ (𝐹‘𝑦)) ↔ ((𝑥 ∈ On ∧ 𝑥 ⊆ ∪ 𝑆) → (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆))))
87	59	3com12 1123	. . . . . . 7 ⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ On ∧ 𝑥 ⊆ 𝑦) → (𝐹‘𝑥) ⊆ (𝐹‘𝑦))
88	87	3expib 1122	. . . . . 6 ⊢ (𝑦 ∈ On → ((𝑥 ∈ On ∧ 𝑥 ⊆ 𝑦) → (𝐹‘𝑥) ⊆ (𝐹‘𝑦)))
89	86, 88	vtoclga 3535	. . . . 5 ⊢ (∪ 𝑆 ∈ On → ((𝑥 ∈ On ∧ 𝑥 ⊆ ∪ 𝑆) → (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆)))
90	80, 82, 89	sylsyld 61	. . . 4 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝑥 ∈ 𝑆 → (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆)))
91	90	ralrimiv 3138	. . 3 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → ∀𝑥 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆))
92		iunss 5010	. . 3 ⊢ (∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆) ↔ ∀𝑥 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆))
93	91, 92	sylibr 233	. 2 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆))
94	78, 93	eqssd 3964	1 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   ≠ wne 2939  ∀wral 3060  ∃wrex 3069   ⊆ wss 3913  ∅c0 4287  ∪ cuni 4870  ∪ ciun 4959  Ord word 6321  Oncon0 6322  Lim wlim 6323  ‘cfv 6501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389  ax-un 7677

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-tr 5228  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-ord 6325  df-on 6326  df-lim 6327  df-iota 6453  df-fv 6509

This theorem is referenced by:  onovuni  8293