Theorem onfununi 8380

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 7798	. . . . . . . . . 10 ⊢ (𝑆 ⊆ On → Ord ∪ 𝑆)
2	1	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) ∧ 𝑆 ≠ ∅) → Ord ∪ 𝑆)
3		nelneq 2863	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝑆 ∧ ¬ ∪ 𝑆 ∈ 𝑆) → ¬ 𝑥 = ∪ 𝑆)
4		elssuni 4942	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ 𝑆 → 𝑥 ⊆ ∪ 𝑆)
5	4	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → 𝑥 ⊆ ∪ 𝑆)
6		ssel 3989	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑆 ⊆ On → (𝑥 ∈ 𝑆 → 𝑥 ∈ On))
7		eloni 6396	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ On → Ord 𝑥)
8	6, 7	syl6 35	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑆 ⊆ On → (𝑥 ∈ 𝑆 → Ord 𝑥))
9	8	imp 406	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → Ord 𝑥)
10		ordsseleq 6415	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((Ord 𝑥 ∧ Ord ∪ 𝑆) → (𝑥 ⊆ ∪ 𝑆 ↔ (𝑥 ∈ ∪ 𝑆 ∨ 𝑥 = ∪ 𝑆)))
11	9, 1, 10	syl2an 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) ∧ 𝑆 ⊆ On) → (𝑥 ⊆ ∪ 𝑆 ↔ (𝑥 ∈ ∪ 𝑆 ∨ 𝑥 = ∪ 𝑆)))
12	11	anabss1 666	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → (𝑥 ⊆ ∪ 𝑆 ↔ (𝑥 ∈ ∪ 𝑆 ∨ 𝑥 = ∪ 𝑆)))
13	5, 12	mpbid 232	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → (𝑥 ∈ ∪ 𝑆 ∨ 𝑥 = ∪ 𝑆))
14	13	ord 864	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → (¬ 𝑥 ∈ ∪ 𝑆 → 𝑥 = ∪ 𝑆))
15	14	con1d 145	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → (¬ 𝑥 = ∪ 𝑆 → 𝑥 ∈ ∪ 𝑆))
16	3, 15	syl5 34	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → ((𝑥 ∈ 𝑆 ∧ ¬ ∪ 𝑆 ∈ 𝑆) → 𝑥 ∈ ∪ 𝑆))
17	16	exp4b 430	. . . . . . . . . . . . . 14 ⊢ (𝑆 ⊆ On → (𝑥 ∈ 𝑆 → (𝑥 ∈ 𝑆 → (¬ ∪ 𝑆 ∈ 𝑆 → 𝑥 ∈ ∪ 𝑆))))
18	17	pm2.43d 53	. . . . . . . . . . . . 13 ⊢ (𝑆 ⊆ On → (𝑥 ∈ 𝑆 → (¬ ∪ 𝑆 ∈ 𝑆 → 𝑥 ∈ ∪ 𝑆)))
19	18	com23 86	. . . . . . . . . . . 12 ⊢ (𝑆 ⊆ On → (¬ ∪ 𝑆 ∈ 𝑆 → (𝑥 ∈ 𝑆 → 𝑥 ∈ ∪ 𝑆)))
20	19	imp 406	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) → (𝑥 ∈ 𝑆 → 𝑥 ∈ ∪ 𝑆))
21	20	ssrdv 4001	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) → 𝑆 ⊆ ∪ 𝑆)
22		ssn0 4410	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ ∪ 𝑆 ∧ 𝑆 ≠ ∅) → ∪ 𝑆 ≠ ∅)
23	21, 22	sylan 580	. . . . . . . . 9 ⊢ (((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) ∧ 𝑆 ≠ ∅) → ∪ 𝑆 ≠ ∅)
24	21	unissd 4922	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) → ∪ 𝑆 ⊆ ∪ ∪ 𝑆)
25		orduniss 6483	. . . . . . . . . . . . 13 ⊢ (Ord ∪ 𝑆 → ∪ ∪ 𝑆 ⊆ ∪ 𝑆)
26	1, 25	syl 17	. . . . . . . . . . . 12 ⊢ (𝑆 ⊆ On → ∪ ∪ 𝑆 ⊆ ∪ 𝑆)
27	26	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) → ∪ ∪ 𝑆 ⊆ ∪ 𝑆)
28	24, 27	eqssd 4013	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) → ∪ 𝑆 = ∪ ∪ 𝑆)
29	28	adantr 480	. . . . . . . . 9 ⊢ (((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) ∧ 𝑆 ≠ ∅) → ∪ 𝑆 = ∪ ∪ 𝑆)
30		df-lim 6391	. . . . . . . . 9 ⊢ (Lim ∪ 𝑆 ↔ (Ord ∪ 𝑆 ∧ ∪ 𝑆 ≠ ∅ ∧ ∪ 𝑆 = ∪ ∪ 𝑆))
31	2, 23, 29, 30	syl3anbrc 1342	. . . . . . . 8 ⊢ (((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) ∧ 𝑆 ≠ ∅) → Lim ∪ 𝑆)
32	31	an32s 652	. . . . . . 7 ⊢ (((𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆 ∈ 𝑆) → Lim ∪ 𝑆)
33	32	3adantl1 1165	. . . . . 6 ⊢ (((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆 ∈ 𝑆) → Lim ∪ 𝑆)
34		ssonuni 7799	. . . . . . . . . 10 ⊢ (𝑆 ∈ 𝑇 → (𝑆 ⊆ On → ∪ 𝑆 ∈ On))
35		limeq 6398	. . . . . . . . . . . 12 ⊢ (𝑦 = ∪ 𝑆 → (Lim 𝑦 ↔ Lim ∪ 𝑆))
36		fveq2 6907	. . . . . . . . . . . . 13 ⊢ (𝑦 = ∪ 𝑆 → (𝐹‘𝑦) = (𝐹‘∪ 𝑆))
37		iuneq1 5013	. . . . . . . . . . . . 13 ⊢ (𝑦 = ∪ 𝑆 → ∪ 𝑥 ∈ 𝑦 (𝐹‘𝑥) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥))
38	36, 37	eqeq12d 2751	. . . . . . . . . . . 12 ⊢ (𝑦 = ∪ 𝑆 → ((𝐹‘𝑦) = ∪ 𝑥 ∈ 𝑦 (𝐹‘𝑥) ↔ (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥)))
39	35, 38	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑦 = ∪ 𝑆 → ((Lim 𝑦 → (𝐹‘𝑦) = ∪ 𝑥 ∈ 𝑦 (𝐹‘𝑥)) ↔ (Lim ∪ 𝑆 → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥))))
40		onfununi.1	. . . . . . . . . . 11 ⊢ (Lim 𝑦 → (𝐹‘𝑦) = ∪ 𝑥 ∈ 𝑦 (𝐹‘𝑥))
41	39, 40	vtoclg 3554	. . . . . . . . . 10 ⊢ (∪ 𝑆 ∈ On → (Lim ∪ 𝑆 → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥)))
42	34, 41	syl6 35	. . . . . . . . 9 ⊢ (𝑆 ∈ 𝑇 → (𝑆 ⊆ On → (Lim ∪ 𝑆 → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥))))
43	42	imp 406	. . . . . . . 8 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On) → (Lim ∪ 𝑆 → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥)))
44	43	3adant3 1131	. . . . . . 7 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (Lim ∪ 𝑆 → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥)))
45	44	adantr 480	. . . . . 6 ⊢ (((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆 ∈ 𝑆) → (Lim ∪ 𝑆 → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥)))
46	33, 45	mpd 15	. . . . 5 ⊢ (((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆 ∈ 𝑆) → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥))
47		eluni2 4916	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ∪ 𝑆 ↔ ∃𝑦 ∈ 𝑆 𝑥 ∈ 𝑦)
48		ssel 3989	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆 ⊆ On → (𝑦 ∈ 𝑆 → 𝑦 ∈ On))
49	48	anim1d 611	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → (𝑦 ∈ On ∧ 𝑥 ∈ 𝑦)))
50		onelon 6411	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ On)
51	49, 50	syl6 35	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ On))
52	48	adantrd 491	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → 𝑦 ∈ On))
53		eloni 6396	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ On → Ord 𝑦)
54	48, 53	syl6 35	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ⊆ On → (𝑦 ∈ 𝑆 → Ord 𝑦))
55		ordelss 6402	. . . . . . . . . . . . . . . . . 18 ⊢ ((Ord 𝑦 ∧ 𝑥 ∈ 𝑦) → 𝑥 ⊆ 𝑦)
56	55	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ⊆ On → ((Ord 𝑦 ∧ 𝑥 ∈ 𝑦) → 𝑥 ⊆ 𝑦))
57	54, 56	syland 603	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → 𝑥 ⊆ 𝑦))
58	51, 52, 57	3jcad 1128	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → (𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑥 ⊆ 𝑦)))
59		onfununi.2	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑥 ⊆ 𝑦) → (𝐹‘𝑥) ⊆ (𝐹‘𝑦))
60	58, 59	syl6 35	. . . . . . . . . . . . . 14 ⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → (𝐹‘𝑥) ⊆ (𝐹‘𝑦)))
61	60	expd 415	. . . . . . . . . . . . 13 ⊢ (𝑆 ⊆ On → (𝑦 ∈ 𝑆 → (𝑥 ∈ 𝑦 → (𝐹‘𝑥) ⊆ (𝐹‘𝑦))))
62	61	reximdvai 3163	. . . . . . . . . . . 12 ⊢ (𝑆 ⊆ On → (∃𝑦 ∈ 𝑆 𝑥 ∈ 𝑦 → ∃𝑦 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘𝑦)))
63	47, 62	biimtrid 242	. . . . . . . . . . 11 ⊢ (𝑆 ⊆ On → (𝑥 ∈ ∪ 𝑆 → ∃𝑦 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘𝑦)))
64		ssiun 5051	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘𝑦) → (𝐹‘𝑥) ⊆ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦))
65	63, 64	syl6 35	. . . . . . . . . 10 ⊢ (𝑆 ⊆ On → (𝑥 ∈ ∪ 𝑆 → (𝐹‘𝑥) ⊆ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦)))
66	65	ralrimiv 3143	. . . . . . . . 9 ⊢ (𝑆 ⊆ On → ∀𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦))
67		iunss 5050	. . . . . . . . 9 ⊢ (∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦) ↔ ∀𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦))
68	66, 67	sylibr 234	. . . . . . . 8 ⊢ (𝑆 ⊆ On → ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦))
69		fveq2 6907	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥))
70	69	cbviunv 5045	. . . . . . . 8 ⊢ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦) = ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥)
71	68, 70	sseqtrdi 4046	. . . . . . 7 ⊢ (𝑆 ⊆ On → ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))
72	71	3ad2ant2 1133	. . . . . 6 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))
73	72	adantr 480	. . . . 5 ⊢ (((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆 ∈ 𝑆) → ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))
74	46, 73	eqsstrd 4034	. . . 4 ⊢ (((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆 ∈ 𝑆) → (𝐹‘∪ 𝑆) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))
75	74	ex 412	. . 3 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (¬ ∪ 𝑆 ∈ 𝑆 → (𝐹‘∪ 𝑆) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥)))
76		fveq2 6907	. . . 4 ⊢ (𝑥 = ∪ 𝑆 → (𝐹‘𝑥) = (𝐹‘∪ 𝑆))
77	76	ssiun2s 5053	. . 3 ⊢ (∪ 𝑆 ∈ 𝑆 → (𝐹‘∪ 𝑆) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))
78	75, 77	pm2.61d2 181	. 2 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝐹‘∪ 𝑆) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))
79	34	imp 406	. . . . . 6 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On) → ∪ 𝑆 ∈ On)
80	79	3adant3 1131	. . . . 5 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → ∪ 𝑆 ∈ On)
81	6	3ad2ant2 1133	. . . . . 6 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝑥 ∈ 𝑆 → 𝑥 ∈ On))
82	81, 4	jca2 513	. . . . 5 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝑥 ∈ 𝑆 → (𝑥 ∈ On ∧ 𝑥 ⊆ ∪ 𝑆)))
83		sseq2 4022	. . . . . . . 8 ⊢ (𝑦 = ∪ 𝑆 → (𝑥 ⊆ 𝑦 ↔ 𝑥 ⊆ ∪ 𝑆))
84	83	anbi2d 630	. . . . . . 7 ⊢ (𝑦 = ∪ 𝑆 → ((𝑥 ∈ On ∧ 𝑥 ⊆ 𝑦) ↔ (𝑥 ∈ On ∧ 𝑥 ⊆ ∪ 𝑆)))
85	36	sseq2d 4028	. . . . . . 7 ⊢ (𝑦 = ∪ 𝑆 → ((𝐹‘𝑥) ⊆ (𝐹‘𝑦) ↔ (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆)))
86	84, 85	imbi12d 344	. . . . . 6 ⊢ (𝑦 = ∪ 𝑆 → (((𝑥 ∈ On ∧ 𝑥 ⊆ 𝑦) → (𝐹‘𝑥) ⊆ (𝐹‘𝑦)) ↔ ((𝑥 ∈ On ∧ 𝑥 ⊆ ∪ 𝑆) → (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆))))
87	59	3com12 1122	. . . . . . 7 ⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ On ∧ 𝑥 ⊆ 𝑦) → (𝐹‘𝑥) ⊆ (𝐹‘𝑦))
88	87	3expib 1121	. . . . . 6 ⊢ (𝑦 ∈ On → ((𝑥 ∈ On ∧ 𝑥 ⊆ 𝑦) → (𝐹‘𝑥) ⊆ (𝐹‘𝑦)))
89	86, 88	vtoclga 3577	. . . . 5 ⊢ (∪ 𝑆 ∈ On → ((𝑥 ∈ On ∧ 𝑥 ⊆ ∪ 𝑆) → (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆)))
90	80, 82, 89	sylsyld 61	. . . 4 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝑥 ∈ 𝑆 → (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆)))
91	90	ralrimiv 3143	. . 3 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → ∀𝑥 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆))
92		iunss 5050	. . 3 ⊢ (∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆) ↔ ∀𝑥 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆))
93	91, 92	sylibr 234	. 2 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆))
94	78, 93	eqssd 4013	1 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1537   ∈ wcel 2106   ≠ wne 2938  ∀wral 3059  ∃wrex 3068   ⊆ wss 3963  ∅c0 4339  ∪ cuni 4912  ∪ ciun 4996  Ord word 6385  Oncon0 6386  Lim wlim 6387  ‘cfv 6563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-tr 5266  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-ord 6389  df-on 6390  df-lim 6391  df-iota 6516  df-fv 6571

This theorem is referenced by:  onovuni  8381