Theorem onfununi 7325

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 6877	. . . . . . . . . 10 ⊢ (𝑆 ⊆ On → Ord ∪ 𝑆)
2	1	ad2antrr 758	. . . . . . . . 9 ⊢ (((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) ∧ 𝑆 ≠ ∅) → Ord ∪ 𝑆)
3		nelneq 2712	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝑆 ∧ ¬ ∪ 𝑆 ∈ 𝑆) → ¬ 𝑥 = ∪ 𝑆)
4		elssuni 4403	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ 𝑆 → 𝑥 ⊆ ∪ 𝑆)
5	4	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → 𝑥 ⊆ ∪ 𝑆)
6		ssel 3562	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑆 ⊆ On → (𝑥 ∈ 𝑆 → 𝑥 ∈ On))
7		eloni 5650	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ On → Ord 𝑥)
8	6, 7	syl6 34	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑆 ⊆ On → (𝑥 ∈ 𝑆 → Ord 𝑥))
9	8	imp 444	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → Ord 𝑥)
10		ordsseleq 5669	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((Ord 𝑥 ∧ Ord ∪ 𝑆) → (𝑥 ⊆ ∪ 𝑆 ↔ (𝑥 ∈ ∪ 𝑆 ∨ 𝑥 = ∪ 𝑆)))
11	9, 1, 10	syl2an 493	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) ∧ 𝑆 ⊆ On) → (𝑥 ⊆ ∪ 𝑆 ↔ (𝑥 ∈ ∪ 𝑆 ∨ 𝑥 = ∪ 𝑆)))
12	11	anabss1 851	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → (𝑥 ⊆ ∪ 𝑆 ↔ (𝑥 ∈ ∪ 𝑆 ∨ 𝑥 = ∪ 𝑆)))
13	5, 12	mpbid 221	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → (𝑥 ∈ ∪ 𝑆 ∨ 𝑥 = ∪ 𝑆))
14	13	ord 391	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → (¬ 𝑥 ∈ ∪ 𝑆 → 𝑥 = ∪ 𝑆))
15	14	con1d 138	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → (¬ 𝑥 = ∪ 𝑆 → 𝑥 ∈ ∪ 𝑆))
16	3, 15	syl5 33	. . . . . . . . . . . . . . 15 ⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → ((𝑥 ∈ 𝑆 ∧ ¬ ∪ 𝑆 ∈ 𝑆) → 𝑥 ∈ ∪ 𝑆))
17	16	exp4b 630	. . . . . . . . . . . . . 14 ⊢ (𝑆 ⊆ On → (𝑥 ∈ 𝑆 → (𝑥 ∈ 𝑆 → (¬ ∪ 𝑆 ∈ 𝑆 → 𝑥 ∈ ∪ 𝑆))))
18	17	pm2.43d 51	. . . . . . . . . . . . 13 ⊢ (𝑆 ⊆ On → (𝑥 ∈ 𝑆 → (¬ ∪ 𝑆 ∈ 𝑆 → 𝑥 ∈ ∪ 𝑆)))
19	18	com23 84	. . . . . . . . . . . 12 ⊢ (𝑆 ⊆ On → (¬ ∪ 𝑆 ∈ 𝑆 → (𝑥 ∈ 𝑆 → 𝑥 ∈ ∪ 𝑆)))
20	19	imp 444	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) → (𝑥 ∈ 𝑆 → 𝑥 ∈ ∪ 𝑆))
21	20	ssrdv 3574	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) → 𝑆 ⊆ ∪ 𝑆)
22		ssn0 3928	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ ∪ 𝑆 ∧ 𝑆 ≠ ∅) → ∪ 𝑆 ≠ ∅)
23	21, 22	sylan 487	. . . . . . . . 9 ⊢ (((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) ∧ 𝑆 ≠ ∅) → ∪ 𝑆 ≠ ∅)
24	21	unissd 4398	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) → ∪ 𝑆 ⊆ ∪ ∪ 𝑆)
25		orduniss 5738	. . . . . . . . . . . . 13 ⊢ (Ord ∪ 𝑆 → ∪ ∪ 𝑆 ⊆ ∪ 𝑆)
26	1, 25	syl 17	. . . . . . . . . . . 12 ⊢ (𝑆 ⊆ On → ∪ ∪ 𝑆 ⊆ ∪ 𝑆)
27	26	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) → ∪ ∪ 𝑆 ⊆ ∪ 𝑆)
28	24, 27	eqssd 3585	. . . . . . . . . 10 ⊢ ((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) → ∪ 𝑆 = ∪ ∪ 𝑆)
29	28	adantr 480	. . . . . . . . 9 ⊢ (((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) ∧ 𝑆 ≠ ∅) → ∪ 𝑆 = ∪ ∪ 𝑆)
30		df-lim 5645	. . . . . . . . 9 ⊢ (Lim ∪ 𝑆 ↔ (Ord ∪ 𝑆 ∧ ∪ 𝑆 ≠ ∅ ∧ ∪ 𝑆 = ∪ ∪ 𝑆))
31	2, 23, 29, 30	syl3anbrc 1239	. . . . . . . 8 ⊢ (((𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆) ∧ 𝑆 ≠ ∅) → Lim ∪ 𝑆)
32	31	an32s 842	. . . . . . 7 ⊢ (((𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆 ∈ 𝑆) → Lim ∪ 𝑆)
33	32	3adantl1 1210	. . . . . 6 ⊢ (((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆 ∈ 𝑆) → Lim ∪ 𝑆)
34		ssonuni 6878	. . . . . . . . . 10 ⊢ (𝑆 ∈ 𝑇 → (𝑆 ⊆ On → ∪ 𝑆 ∈ On))
35		limeq 5652	. . . . . . . . . . . 12 ⊢ (𝑦 = ∪ 𝑆 → (Lim 𝑦 ↔ Lim ∪ 𝑆))
36		fveq2 6103	. . . . . . . . . . . . 13 ⊢ (𝑦 = ∪ 𝑆 → (𝐹‘𝑦) = (𝐹‘∪ 𝑆))
37		iuneq1 4470	. . . . . . . . . . . . 13 ⊢ (𝑦 = ∪ 𝑆 → ∪ 𝑥 ∈ 𝑦 (𝐹‘𝑥) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥))
38	36, 37	eqeq12d 2625	. . . . . . . . . . . 12 ⊢ (𝑦 = ∪ 𝑆 → ((𝐹‘𝑦) = ∪ 𝑥 ∈ 𝑦 (𝐹‘𝑥) ↔ (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥)))
39	35, 38	imbi12d 333	. . . . . . . . . . 11 ⊢ (𝑦 = ∪ 𝑆 → ((Lim 𝑦 → (𝐹‘𝑦) = ∪ 𝑥 ∈ 𝑦 (𝐹‘𝑥)) ↔ (Lim ∪ 𝑆 → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥))))
40		onfununi.1	. . . . . . . . . . 11 ⊢ (Lim 𝑦 → (𝐹‘𝑦) = ∪ 𝑥 ∈ 𝑦 (𝐹‘𝑥))
41	39, 40	vtoclg 3239	. . . . . . . . . 10 ⊢ (∪ 𝑆 ∈ On → (Lim ∪ 𝑆 → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥)))
42	34, 41	syl6 34	. . . . . . . . 9 ⊢ (𝑆 ∈ 𝑇 → (𝑆 ⊆ On → (Lim ∪ 𝑆 → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥))))
43	42	imp 444	. . . . . . . 8 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On) → (Lim ∪ 𝑆 → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥)))
44	43	3adant3 1074	. . . . . . 7 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (Lim ∪ 𝑆 → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥)))
45	44	adantr 480	. . . . . 6 ⊢ (((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆 ∈ 𝑆) → (Lim ∪ 𝑆 → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥)))
46	33, 45	mpd 15	. . . . 5 ⊢ (((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆 ∈ 𝑆) → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥))
47		eluni2 4376	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ∪ 𝑆 ↔ ∃𝑦 ∈ 𝑆 𝑥 ∈ 𝑦)
48		ssel 3562	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆 ⊆ On → (𝑦 ∈ 𝑆 → 𝑦 ∈ On))
49	48	anim1d 586	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → (𝑦 ∈ On ∧ 𝑥 ∈ 𝑦)))
50		onelon 5665	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ On)
51	49, 50	syl6 34	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ On))
52	48	adantrd 483	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → 𝑦 ∈ On))
53		eloni 5650	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ On → Ord 𝑦)
54	48, 53	syl6 34	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ⊆ On → (𝑦 ∈ 𝑆 → Ord 𝑦))
55		ordelss 5656	. . . . . . . . . . . . . . . . . 18 ⊢ ((Ord 𝑦 ∧ 𝑥 ∈ 𝑦) → 𝑥 ⊆ 𝑦)
56	55	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑆 ⊆ On → ((Ord 𝑦 ∧ 𝑥 ∈ 𝑦) → 𝑥 ⊆ 𝑦))
57	54, 56	syland 497	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → 𝑥 ⊆ 𝑦))
58	51, 52, 57	3jcad 1236	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → (𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑥 ⊆ 𝑦)))
59		onfununi.2	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑥 ⊆ 𝑦) → (𝐹‘𝑥) ⊆ (𝐹‘𝑦))
60	58, 59	syl6 34	. . . . . . . . . . . . . 14 ⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → (𝐹‘𝑥) ⊆ (𝐹‘𝑦)))
61	60	expd 451	. . . . . . . . . . . . 13 ⊢ (𝑆 ⊆ On → (𝑦 ∈ 𝑆 → (𝑥 ∈ 𝑦 → (𝐹‘𝑥) ⊆ (𝐹‘𝑦))))
62	61	reximdvai 2998	. . . . . . . . . . . 12 ⊢ (𝑆 ⊆ On → (∃𝑦 ∈ 𝑆 𝑥 ∈ 𝑦 → ∃𝑦 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘𝑦)))
63	47, 62	syl5bi 231	. . . . . . . . . . 11 ⊢ (𝑆 ⊆ On → (𝑥 ∈ ∪ 𝑆 → ∃𝑦 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘𝑦)))
64		ssiun 4498	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘𝑦) → (𝐹‘𝑥) ⊆ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦))
65	63, 64	syl6 34	. . . . . . . . . 10 ⊢ (𝑆 ⊆ On → (𝑥 ∈ ∪ 𝑆 → (𝐹‘𝑥) ⊆ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦)))
66	65	ralrimiv 2948	. . . . . . . . 9 ⊢ (𝑆 ⊆ On → ∀𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦))
67		iunss 4497	. . . . . . . . 9 ⊢ (∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦) ↔ ∀𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦))
68	66, 67	sylibr 223	. . . . . . . 8 ⊢ (𝑆 ⊆ On → ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦))
69		fveq2 6103	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥))
70	69	cbviunv 4495	. . . . . . . 8 ⊢ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦) = ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥)
71	68, 70	syl6sseq 3614	. . . . . . 7 ⊢ (𝑆 ⊆ On → ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))
72	71	3ad2ant2 1076	. . . . . 6 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))
73	72	adantr 480	. . . . 5 ⊢ (((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆 ∈ 𝑆) → ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))
74	46, 73	eqsstrd 3602	. . . 4 ⊢ (((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆 ∈ 𝑆) → (𝐹‘∪ 𝑆) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))
75	74	ex 449	. . 3 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (¬ ∪ 𝑆 ∈ 𝑆 → (𝐹‘∪ 𝑆) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥)))
76		fveq2 6103	. . . 4 ⊢ (𝑥 = ∪ 𝑆 → (𝐹‘𝑥) = (𝐹‘∪ 𝑆))
77	76	ssiun2s 4500	. . 3 ⊢ (∪ 𝑆 ∈ 𝑆 → (𝐹‘∪ 𝑆) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))
78	75, 77	pm2.61d2 171	. 2 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝐹‘∪ 𝑆) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))
79	34	imp 444	. . . . . 6 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On) → ∪ 𝑆 ∈ On)
80	79	3adant3 1074	. . . . 5 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → ∪ 𝑆 ∈ On)
81	6	3ad2ant2 1076	. . . . . 6 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝑥 ∈ 𝑆 → 𝑥 ∈ On))
82	4	a1i 11	. . . . . 6 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝑥 ∈ 𝑆 → 𝑥 ⊆ ∪ 𝑆))
83	81, 82	jcad 554	. . . . 5 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝑥 ∈ 𝑆 → (𝑥 ∈ On ∧ 𝑥 ⊆ ∪ 𝑆)))
84		sseq2 3590	. . . . . . . 8 ⊢ (𝑦 = ∪ 𝑆 → (𝑥 ⊆ 𝑦 ↔ 𝑥 ⊆ ∪ 𝑆))
85	84	anbi2d 736	. . . . . . 7 ⊢ (𝑦 = ∪ 𝑆 → ((𝑥 ∈ On ∧ 𝑥 ⊆ 𝑦) ↔ (𝑥 ∈ On ∧ 𝑥 ⊆ ∪ 𝑆)))
86	36	sseq2d 3596	. . . . . . 7 ⊢ (𝑦 = ∪ 𝑆 → ((𝐹‘𝑥) ⊆ (𝐹‘𝑦) ↔ (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆)))
87	85, 86	imbi12d 333	. . . . . 6 ⊢ (𝑦 = ∪ 𝑆 → (((𝑥 ∈ On ∧ 𝑥 ⊆ 𝑦) → (𝐹‘𝑥) ⊆ (𝐹‘𝑦)) ↔ ((𝑥 ∈ On ∧ 𝑥 ⊆ ∪ 𝑆) → (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆))))
88	59	3com12 1261	. . . . . . 7 ⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ On ∧ 𝑥 ⊆ 𝑦) → (𝐹‘𝑥) ⊆ (𝐹‘𝑦))
89	88	3expib 1260	. . . . . 6 ⊢ (𝑦 ∈ On → ((𝑥 ∈ On ∧ 𝑥 ⊆ 𝑦) → (𝐹‘𝑥) ⊆ (𝐹‘𝑦)))
90	87, 89	vtoclga 3245	. . . . 5 ⊢ (∪ 𝑆 ∈ On → ((𝑥 ∈ On ∧ 𝑥 ⊆ ∪ 𝑆) → (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆)))
91	80, 83, 90	sylsyld 59	. . . 4 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝑥 ∈ 𝑆 → (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆)))
92	91	ralrimiv 2948	. . 3 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → ∀𝑥 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆))
93		iunss 4497	. . 3 ⊢ (∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆) ↔ ∀𝑥 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆))
94	92, 93	sylibr 223	. 2 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆))
95	78, 94	eqssd 3585	1 ⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897   ⊆ wss 3540  ∅c0 3874  ∪ cuni 4372  ∪ ciun 4455  Ord word 5639  Oncon0 5640  Lim wlim 5641  ‘cfv 5804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-tr 4681  df-eprel 4949  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-ord 5643  df-on 5644  df-lim 5645  df-iota 5768  df-fv 5812

This theorem is referenced by:  onovuni  7326