Theorem onfununi 7438

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 6985	. . . . . . . . . 10 ⊢ (𝑆 ⊆ On → Ord ∪ 𝑆)
2	1	ad2antrr 762	. . . . . . . . 9 ⊢ (((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) ∧ 𝑆 ≠ ∅) → Ord ∪ 𝑆)
3		nelneq 2725	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝑆 ∧ ¬ ∪ 𝑆 ∈ 𝑆) → ¬ 𝑥 = ∪ 𝑆)
4		elssuni 4467	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ 𝑆 → 𝑥 ⊆ ∪ 𝑆)
5	4	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → 𝑥 ⊆ ∪ 𝑆)
6		ssel 3597	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑆 ⊆ On → (𝑥 ∈ 𝑆 → 𝑥 ∈ On))
7		eloni 5733	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ On → Ord 𝑥)
8	6, 7	syl6 35	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑆 ⊆ On → (𝑥 ∈ 𝑆 → Ord 𝑥))
9	8	imp 445	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → Ord 𝑥)
10		ordsseleq 5752	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((Ord 𝑥 ∧ Ord ∪ 𝑆) → (𝑥 ⊆ ∪ 𝑆 ↔ (𝑥 ∈ ∪ 𝑆 ∨ 𝑥 = ∪ 𝑆)))
11	9, 1, 10	syl2an 494	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) ∧ 𝑆 ⊆ On) → (𝑥 ⊆ ∪ 𝑆 ↔ (𝑥 ∈ ∪ 𝑆 ∨ 𝑥 = ∪ 𝑆)))
12	11	anabss1 855	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → (𝑥 ⊆ ∪ 𝑆 ↔ (𝑥 ∈ ∪ 𝑆 ∨ 𝑥 = ∪ 𝑆)))
13	5, 12	mpbid 222	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → (𝑥 ∈ ∪ 𝑆 ∨ 𝑥 = ∪ 𝑆))
14	13	ord 392	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → (¬ 𝑥 ∈ ∪ 𝑆 → 𝑥 = ∪ 𝑆))
15	14	con1d 139	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → (¬ 𝑥 = ∪ 𝑆 → 𝑥 ∈ ∪ 𝑆))
16	3, 15	syl5 34	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → ((𝑥 ∈ 𝑆 ∧ ¬ ∪ 𝑆 ∈ 𝑆) → 𝑥 ∈ ∪ 𝑆))
17	16	exp4b 632	. . . . . . . . . . . . . 14 ⊢ (𝑆 ⊆ On → (𝑥 ∈ 𝑆 → (𝑥 ∈ 𝑆 → (¬ ∪ 𝑆 ∈ 𝑆 → 𝑥 ∈ ∪ 𝑆))))
18	17	pm2.43d 53	. . . . . . . . . . . . 13 ⊢ (𝑆 ⊆ On → (𝑥 ∈ 𝑆 → (¬ ∪ 𝑆 ∈ 𝑆 → 𝑥 ∈ ∪ 𝑆)))
19	18	com23 86	. . . . . . . . . . . 12 ⊢ (𝑆 ⊆ On → (¬ ∪ 𝑆 ∈ 𝑆 → (𝑥 ∈ 𝑆 → 𝑥 ∈ ∪ 𝑆)))
20	19	imp 445	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) → (𝑥 ∈ 𝑆 → 𝑥 ∈ ∪ 𝑆))
21	20	ssrdv 3609	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) → 𝑆 ⊆ ∪ 𝑆)
22		ssn0 3976	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ ∪ 𝑆 ∧ 𝑆 ≠ ∅) → ∪ 𝑆 ≠ ∅)
23	21, 22	sylan 488	. . . . . . . . 9 ⊢ (((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) ∧ 𝑆 ≠ ∅) → ∪ 𝑆 ≠ ∅)
24	21	unissd 4462	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) → ∪ 𝑆 ⊆ ∪ ∪ 𝑆)
25		orduniss 5821	. . . . . . . . . . . . 13 ⊢ (Ord ∪ 𝑆 → ∪ ∪ 𝑆 ⊆ ∪ 𝑆)
26	1, 25	syl 17	. . . . . . . . . . . 12 ⊢ (𝑆 ⊆ On → ∪ ∪ 𝑆 ⊆ ∪ 𝑆)
27	26	adantr 481	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) → ∪ ∪ 𝑆 ⊆ ∪ 𝑆)
28	24, 27	eqssd 3620	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) → ∪ 𝑆 = ∪ ∪ 𝑆)
29	28	adantr 481	. . . . . . . . 9 ⊢ (((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) ∧ 𝑆 ≠ ∅) → ∪ 𝑆 = ∪ ∪ 𝑆)
30		df-lim 5728	. . . . . . . . 9 ⊢ (Lim ∪ 𝑆 ↔ (Ord ∪ 𝑆 ∧ ∪ 𝑆 ≠ ∅ ∧ ∪ 𝑆 = ∪ ∪ 𝑆))
31	2, 23, 29, 30	syl3anbrc 1246	. . . . . . . 8 ⊢ (((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) ∧ 𝑆 ≠ ∅) → Lim ∪ 𝑆)
32	31	an32s 846	. . . . . . 7 ⊢ (((𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆 ∈ 𝑆) → Lim ∪ 𝑆)
33	32	3adantl1 1217	. . . . . 6 ⊢ (((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆 ∈ 𝑆) → Lim ∪ 𝑆)
34		ssonuni 6986	. . . . . . . . . 10 ⊢ (𝑆 ∈ 𝑇 → (𝑆 ⊆ On → ∪ 𝑆 ∈ On))
35		limeq 5735	. . . . . . . . . . . 12 ⊢ (𝑦 = ∪ 𝑆 → (Lim 𝑦 ↔ Lim ∪ 𝑆))
36		fveq2 6191	. . . . . . . . . . . . 13 ⊢ (𝑦 = ∪ 𝑆 → (𝐹‘𝑦) = (𝐹‘∪ 𝑆))
37		iuneq1 4534	. . . . . . . . . . . . 13 ⊢ (𝑦 = ∪ 𝑆 → ∪ 𝑥 ∈ 𝑦 (𝐹‘𝑥) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥))
38	36, 37	eqeq12d 2637	. . . . . . . . . . . 12 ⊢ (𝑦 = ∪ 𝑆 → ((𝐹‘𝑦) = ∪ 𝑥 ∈ 𝑦 (𝐹‘𝑥) ↔ (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥)))
39	35, 38	imbi12d 334	. . . . . . . . . . 11 ⊢ (𝑦 = ∪ 𝑆 → ((Lim 𝑦 → (𝐹‘𝑦) = ∪ 𝑥 ∈ 𝑦 (𝐹‘𝑥)) ↔ (Lim ∪ 𝑆 → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥))))
40		onfununi.1	. . . . . . . . . . 11 ⊢ (Lim 𝑦 → (𝐹‘𝑦) = ∪ 𝑥 ∈ 𝑦 (𝐹‘𝑥))
41	39, 40	vtoclg 3266	. . . . . . . . . 10 ⊢ (∪ 𝑆 ∈ On → (Lim ∪ 𝑆 → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥)))
42	34, 41	syl6 35	. . . . . . . . 9 ⊢ (𝑆 ∈ 𝑇 → (𝑆 ⊆ On → (Lim ∪ 𝑆 → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥))))
43	42	imp 445	. . . . . . . 8 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On) → (Lim ∪ 𝑆 → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥)))
44	43	3adant3 1081	. . . . . . 7 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (Lim ∪ 𝑆 → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥)))
45	44	adantr 481	. . . . . 6 ⊢ (((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆 ∈ 𝑆) → (Lim ∪ 𝑆 → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥)))
46	33, 45	mpd 15	. . . . 5 ⊢ (((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆 ∈ 𝑆) → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥))
47		eluni2 4440	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ∪ 𝑆 ↔ ∃𝑦 ∈ 𝑆 𝑥 ∈ 𝑦)
48		ssel 3597	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆 ⊆ On → (𝑦 ∈ 𝑆 → 𝑦 ∈ On))
49	48	anim1d 588	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → (𝑦 ∈ On ∧ 𝑥 ∈ 𝑦)))
50		onelon 5748	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ On)
51	49, 50	syl6 35	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ On))
52	48	adantrd 484	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → 𝑦 ∈ On))
53		eloni 5733	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ On → Ord 𝑦)
54	48, 53	syl6 35	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ⊆ On → (𝑦 ∈ 𝑆 → Ord 𝑦))
55		ordelss 5739	. . . . . . . . . . . . . . . . . 18 ⊢ ((Ord 𝑦 ∧ 𝑥 ∈ 𝑦) → 𝑥 ⊆ 𝑦)
56	55	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ⊆ On → ((Ord 𝑦 ∧ 𝑥 ∈ 𝑦) → 𝑥 ⊆ 𝑦))
57	54, 56	syland 498	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → 𝑥 ⊆ 𝑦))
58	51, 52, 57	3jcad 1243	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → (𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑥 ⊆ 𝑦)))
59		onfununi.2	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑥 ⊆ 𝑦) → (𝐹‘𝑥) ⊆ (𝐹‘𝑦))
60	58, 59	syl6 35	. . . . . . . . . . . . . 14 ⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → (𝐹‘𝑥) ⊆ (𝐹‘𝑦)))
61	60	expd 452	. . . . . . . . . . . . 13 ⊢ (𝑆 ⊆ On → (𝑦 ∈ 𝑆 → (𝑥 ∈ 𝑦 → (𝐹‘𝑥) ⊆ (𝐹‘𝑦))))
62	61	reximdvai 3015	. . . . . . . . . . . 12 ⊢ (𝑆 ⊆ On → (∃𝑦 ∈ 𝑆 𝑥 ∈ 𝑦 → ∃𝑦 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘𝑦)))
63	47, 62	syl5bi 232	. . . . . . . . . . 11 ⊢ (𝑆 ⊆ On → (𝑥 ∈ ∪ 𝑆 → ∃𝑦 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘𝑦)))
64		ssiun 4562	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘𝑦) → (𝐹‘𝑥) ⊆ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦))
65	63, 64	syl6 35	. . . . . . . . . 10 ⊢ (𝑆 ⊆ On → (𝑥 ∈ ∪ 𝑆 → (𝐹‘𝑥) ⊆ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦)))
66	65	ralrimiv 2965	. . . . . . . . 9 ⊢ (𝑆 ⊆ On → ∀𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦))
67		iunss 4561	. . . . . . . . 9 ⊢ (∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦) ↔ ∀𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦))
68	66, 67	sylibr 224	. . . . . . . 8 ⊢ (𝑆 ⊆ On → ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦))
69		fveq2 6191	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥))
70	69	cbviunv 4559	. . . . . . . 8 ⊢ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦) = ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥)
71	68, 70	syl6sseq 3651	. . . . . . 7 ⊢ (𝑆 ⊆ On → ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))
72	71	3ad2ant2 1083	. . . . . 6 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))
73	72	adantr 481	. . . . 5 ⊢ (((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆 ∈ 𝑆) → ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))
74	46, 73	eqsstrd 3639	. . . 4 ⊢ (((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆 ∈ 𝑆) → (𝐹‘∪ 𝑆) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))
75	74	ex 450	. . 3 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (¬ ∪ 𝑆 ∈ 𝑆 → (𝐹‘∪ 𝑆) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥)))
76		fveq2 6191	. . . 4 ⊢ (𝑥 = ∪ 𝑆 → (𝐹‘𝑥) = (𝐹‘∪ 𝑆))
77	76	ssiun2s 4564	. . 3 ⊢ (∪ 𝑆 ∈ 𝑆 → (𝐹‘∪ 𝑆) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))
78	75, 77	pm2.61d2 172	. 2 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝐹‘∪ 𝑆) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))
79	34	imp 445	. . . . . 6 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On) → ∪ 𝑆 ∈ On)
80	79	3adant3 1081	. . . . 5 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → ∪ 𝑆 ∈ On)
81	6	3ad2ant2 1083	. . . . . 6 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝑥 ∈ 𝑆 → 𝑥 ∈ On))
82	4	a1i 11	. . . . . 6 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝑥 ∈ 𝑆 → 𝑥 ⊆ ∪ 𝑆))
83	81, 82	jcad 555	. . . . 5 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝑥 ∈ 𝑆 → (𝑥 ∈ On ∧ 𝑥 ⊆ ∪ 𝑆)))
84		sseq2 3627	. . . . . . . 8 ⊢ (𝑦 = ∪ 𝑆 → (𝑥 ⊆ 𝑦 ↔ 𝑥 ⊆ ∪ 𝑆))
85	84	anbi2d 740	. . . . . . 7 ⊢ (𝑦 = ∪ 𝑆 → ((𝑥 ∈ On ∧ 𝑥 ⊆ 𝑦) ↔ (𝑥 ∈ On ∧ 𝑥 ⊆ ∪ 𝑆)))
86	36	sseq2d 3633	. . . . . . 7 ⊢ (𝑦 = ∪ 𝑆 → ((𝐹‘𝑥) ⊆ (𝐹‘𝑦) ↔ (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆)))
87	85, 86	imbi12d 334	. . . . . 6 ⊢ (𝑦 = ∪ 𝑆 → (((𝑥 ∈ On ∧ 𝑥 ⊆ 𝑦) → (𝐹‘𝑥) ⊆ (𝐹‘𝑦)) ↔ ((𝑥 ∈ On ∧ 𝑥 ⊆ ∪ 𝑆) → (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆))))
88	59	3com12 1269	. . . . . . 7 ⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ On ∧ 𝑥 ⊆ 𝑦) → (𝐹‘𝑥) ⊆ (𝐹‘𝑦))
89	88	3expib 1268	. . . . . 6 ⊢ (𝑦 ∈ On → ((𝑥 ∈ On ∧ 𝑥 ⊆ 𝑦) → (𝐹‘𝑥) ⊆ (𝐹‘𝑦)))
90	87, 89	vtoclga 3272	. . . . 5 ⊢ (∪ 𝑆 ∈ On → ((𝑥 ∈ On ∧ 𝑥 ⊆ ∪ 𝑆) → (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆)))
91	80, 83, 90	sylsyld 61	. . . 4 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝑥 ∈ 𝑆 → (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆)))
92	91	ralrimiv 2965	. . 3 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → ∀𝑥 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆))
93		iunss 4561	. . 3 ⊢ (∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆) ↔ ∀𝑥 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆))
94	92, 93	sylibr 224	. 2 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆))
95	78, 94	eqssd 3620	1 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384   ∧ w3a 1037   = wceq 1483   ∈ wcel 1990   ≠ wne 2794  ∀wral 2912  ∃wrex 2913   ⊆ wss 3574  ∅c0 3915  ∪ cuni 4436  ∪ ciun 4520  Ord word 5722  Oncon0 5723  Lim wlim 5724  ‘cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-tr 4753  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-ord 5726  df-on 5727  df-lim 5728  df-iota 5851  df-fv 5896

This theorem is referenced by:  onovuni  7439