Metamath Proof Explorer

Theorem onfununi

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

Ref Expression
Hypotheses onfununi.1 ⊢ ( Lim 𝑦 → ( 𝐹 ‘ 𝑦 ) = ∪ 𝑥 ∈ 𝑦 ( 𝐹 ‘ 𝑥 ) )
onfununi.2 ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑥 ⊆ 𝑦 ) → ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑦 ) )
Assertion onfununi ( ( 𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅ ) → ( 𝐹 ‘ ∪ 𝑆 ) = ∪ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 onfununi.1 ⊢ ( Lim 𝑦 → ( 𝐹 ‘ 𝑦 ) = ∪ 𝑥 ∈ 𝑦 ( 𝐹 ‘ 𝑥 ) )
2 onfununi.2 ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑥 ⊆ 𝑦 ) → ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑦 ) )
3 ssorduni ⊢ ( 𝑆 ⊆ On → Ord ∪ 𝑆 )
4 3 ad2antrr ⊢ ( ( ( 𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆 ) ∧ 𝑆 ≠ ∅ ) → Ord ∪ 𝑆 )
5 nelneq ⊢ ( ( 𝑥 ∈ 𝑆 ∧ ¬ ∪ 𝑆 ∈ 𝑆 ) → ¬ 𝑥 = ∪ 𝑆 )
6 elssuni ⊢ ( 𝑥 ∈ 𝑆 → 𝑥 ⊆ ∪ 𝑆 )
7 6 adantl ⊢ ( ( 𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ⊆ ∪ 𝑆 )
8 ssel ⊢ ( 𝑆 ⊆ On → ( 𝑥 ∈ 𝑆 → 𝑥 ∈ On ) )
9 eloni ⊢ ( 𝑥 ∈ On → Ord 𝑥 )
10 8 9 syl6 ⊢ ( 𝑆 ⊆ On → ( 𝑥 ∈ 𝑆 → Ord 𝑥 ) )
11 10 imp ⊢ ( ( 𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆 ) → Ord 𝑥 )
12 ordsseleq ⊢ ( ( Ord 𝑥 ∧ Ord ∪ 𝑆 ) → ( 𝑥 ⊆ ∪ 𝑆 ↔ ( 𝑥 ∈ ∪ 𝑆 ∨ 𝑥 = ∪ 𝑆 ) ) )
13 11 3 12 syl2an ⊢ ( ( ( 𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑆 ⊆ On ) → ( 𝑥 ⊆ ∪ 𝑆 ↔ ( 𝑥 ∈ ∪ 𝑆 ∨ 𝑥 = ∪ 𝑆 ) ) )
14 13 anabss1 ⊢ ( ( 𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ⊆ ∪ 𝑆 ↔ ( 𝑥 ∈ ∪ 𝑆 ∨ 𝑥 = ∪ 𝑆 ) ) )
15 7 14 mpbid ⊢ ( ( 𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ∈ ∪ 𝑆 ∨ 𝑥 = ∪ 𝑆 ) )
16 15 ord ⊢ ( ( 𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆 ) → ( ¬ 𝑥 ∈ ∪ 𝑆 → 𝑥 = ∪ 𝑆 ) )
17 16 con1d ⊢ ( ( 𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆 ) → ( ¬ 𝑥 = ∪ 𝑆 → 𝑥 ∈ ∪ 𝑆 ) )
18 5 17 syl5 ⊢ ( ( 𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑥 ∈ 𝑆 ∧ ¬ ∪ 𝑆 ∈ 𝑆 ) → 𝑥 ∈ ∪ 𝑆 ) )
19 18 exp4b ⊢ ( 𝑆 ⊆ On → ( 𝑥 ∈ 𝑆 → ( 𝑥 ∈ 𝑆 → ( ¬ ∪ 𝑆 ∈ 𝑆 → 𝑥 ∈ ∪ 𝑆 ) ) ) )
20 19 pm2.43d ⊢ ( 𝑆 ⊆ On → ( 𝑥 ∈ 𝑆 → ( ¬ ∪ 𝑆 ∈ 𝑆 → 𝑥 ∈ ∪ 𝑆 ) ) )
21 20 com23 ⊢ ( 𝑆 ⊆ On → ( ¬ ∪ 𝑆 ∈ 𝑆 → ( 𝑥 ∈ 𝑆 → 𝑥 ∈ ∪ 𝑆 ) ) )
22 21 imp ⊢ ( ( 𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆 ) → ( 𝑥 ∈ 𝑆 → 𝑥 ∈ ∪ 𝑆 ) )
23 22 ssrdv ⊢ ( ( 𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆 ) → 𝑆 ⊆ ∪ 𝑆 )
24 ssn0 ⊢ ( ( 𝑆 ⊆ ∪ 𝑆 ∧ 𝑆 ≠ ∅ ) → ∪ 𝑆 ≠ ∅ )
25 23 24 sylan ⊢ ( ( ( 𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆 ) ∧ 𝑆 ≠ ∅ ) → ∪ 𝑆 ≠ ∅ )
26 23 unissd ⊢ ( ( 𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆 ) → ∪ 𝑆 ⊆ ∪ ∪ 𝑆 )
27 orduniss ⊢ ( Ord ∪ 𝑆 → ∪ ∪ 𝑆 ⊆ ∪ 𝑆 )
28 3 27 syl ⊢ ( 𝑆 ⊆ On → ∪ ∪ 𝑆 ⊆ ∪ 𝑆 )
29 28 adantr ⊢ ( ( 𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆 ) → ∪ ∪ 𝑆 ⊆ ∪ 𝑆 )
30 26 29 eqssd ⊢ ( ( 𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆 ) → ∪ 𝑆 = ∪ ∪ 𝑆 )
31 30 adantr ⊢ ( ( ( 𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆 ) ∧ 𝑆 ≠ ∅ ) → ∪ 𝑆 = ∪ ∪ 𝑆 )
32 df-lim ⊢ ( Lim ∪ 𝑆 ↔ ( Ord ∪ 𝑆 ∧ ∪ 𝑆 ≠ ∅ ∧ ∪ 𝑆 = ∪ ∪ 𝑆 ) )
33 4 25 31 32 syl3anbrc ⊢ ( ( ( 𝑆 ⊆ On ∧ ¬ ∪ 𝑆 ∈ 𝑆 ) ∧ 𝑆 ≠ ∅ ) → Lim ∪ 𝑆 )
34 33 an32s ⊢ ( ( ( 𝑆 ⊆ On ∧ 𝑆 ≠ ∅ ) ∧ ¬ ∪ 𝑆 ∈ 𝑆 ) → Lim ∪ 𝑆 )
35 34 3adantl1 ⊢ ( ( ( 𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅ ) ∧ ¬ ∪ 𝑆 ∈ 𝑆 ) → Lim ∪ 𝑆 )
36 ssonuni ⊢ ( 𝑆 ∈ 𝑇 → ( 𝑆 ⊆ On → ∪ 𝑆 ∈ On ) )
37 limeq ⊢ ( 𝑦 = ∪ 𝑆 → ( Lim 𝑦 ↔ Lim ∪ 𝑆 ) )
38 fveq2 ⊢ ( 𝑦 = ∪ 𝑆 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ∪ 𝑆 ) )
39 iuneq1 ⊢ ( 𝑦 = ∪ 𝑆 → ∪ 𝑥 ∈ 𝑦 ( 𝐹 ‘ 𝑥 ) = ∪ 𝑥 ∈ ∪ 𝑆 ( 𝐹 ‘ 𝑥 ) )
40 38 39 eqeq12d ⊢ ( 𝑦 = ∪ 𝑆 → ( ( 𝐹 ‘ 𝑦 ) = ∪ 𝑥 ∈ 𝑦 ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ ∪ 𝑆 ) = ∪ 𝑥 ∈ ∪ 𝑆 ( 𝐹 ‘ 𝑥 ) ) )
41 37 40 imbi12d ⊢ ( 𝑦 = ∪ 𝑆 → ( ( Lim 𝑦 → ( 𝐹 ‘ 𝑦 ) = ∪ 𝑥 ∈ 𝑦 ( 𝐹 ‘ 𝑥 ) ) ↔ ( Lim ∪ 𝑆 → ( 𝐹 ‘ ∪ 𝑆 ) = ∪ 𝑥 ∈ ∪ 𝑆 ( 𝐹 ‘ 𝑥 ) ) ) )
42 41 1 vtoclg ⊢ ( ∪ 𝑆 ∈ On → ( Lim ∪ 𝑆 → ( 𝐹 ‘ ∪ 𝑆 ) = ∪ 𝑥 ∈ ∪ 𝑆 ( 𝐹 ‘ 𝑥 ) ) )
43 36 42 syl6 ⊢ ( 𝑆 ∈ 𝑇 → ( 𝑆 ⊆ On → ( Lim ∪ 𝑆 → ( 𝐹 ‘ ∪ 𝑆 ) = ∪ 𝑥 ∈ ∪ 𝑆 ( 𝐹 ‘ 𝑥 ) ) ) )
44 43 imp ⊢ ( ( 𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ) → ( Lim ∪ 𝑆 → ( 𝐹 ‘ ∪ 𝑆 ) = ∪ 𝑥 ∈ ∪ 𝑆 ( 𝐹 ‘ 𝑥 ) ) )
45 44 3adant3 ⊢ ( ( 𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅ ) → ( Lim ∪ 𝑆 → ( 𝐹 ‘ ∪ 𝑆 ) = ∪ 𝑥 ∈ ∪ 𝑆 ( 𝐹 ‘ 𝑥 ) ) )
46 45 adantr ⊢ ( ( ( 𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅ ) ∧ ¬ ∪ 𝑆 ∈ 𝑆 ) → ( Lim ∪ 𝑆 → ( 𝐹 ‘ ∪ 𝑆 ) = ∪ 𝑥 ∈ ∪ 𝑆 ( 𝐹 ‘ 𝑥 ) ) )
47 35 46 mpd ⊢ ( ( ( 𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅ ) ∧ ¬ ∪ 𝑆 ∈ 𝑆 ) → ( 𝐹 ‘ ∪ 𝑆 ) = ∪ 𝑥 ∈ ∪ 𝑆 ( 𝐹 ‘ 𝑥 ) )
48 eluni2 ⊢ ( 𝑥 ∈ ∪ 𝑆 ↔ ∃ 𝑦 ∈ 𝑆 𝑥 ∈ 𝑦 )
49 ssel ⊢ ( 𝑆 ⊆ On → ( 𝑦 ∈ 𝑆 → 𝑦 ∈ On ) )
50 49 anim1d ⊢ ( 𝑆 ⊆ On → ( ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦 ) → ( 𝑦 ∈ On ∧ 𝑥 ∈ 𝑦 ) ) )
51 onelon ⊢ ( ( 𝑦 ∈ On ∧ 𝑥 ∈ 𝑦 ) → 𝑥 ∈ On )
52 50 51 syl6 ⊢ ( 𝑆 ⊆ On → ( ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦 ) → 𝑥 ∈ On ) )
53 49 adantrd ⊢ ( 𝑆 ⊆ On → ( ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦 ) → 𝑦 ∈ On ) )
54 eloni ⊢ ( 𝑦 ∈ On → Ord 𝑦 )
55 49 54 syl6 ⊢ ( 𝑆 ⊆ On → ( 𝑦 ∈ 𝑆 → Ord 𝑦 ) )
56 ordelss ⊢ ( ( Ord 𝑦 ∧ 𝑥 ∈ 𝑦 ) → 𝑥 ⊆ 𝑦 )
57 56 a1i ⊢ ( 𝑆 ⊆ On → ( ( Ord 𝑦 ∧ 𝑥 ∈ 𝑦 ) → 𝑥 ⊆ 𝑦 ) )
58 55 57 syland ⊢ ( 𝑆 ⊆ On → ( ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦 ) → 𝑥 ⊆ 𝑦 ) )
59 52 53 58 3jcad ⊢ ( 𝑆 ⊆ On → ( ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦 ) → ( 𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑥 ⊆ 𝑦 ) ) )
60 59 2 syl6 ⊢ ( 𝑆 ⊆ On → ( ( 𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦 ) → ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑦 ) ) )
61 60 expd ⊢ ( 𝑆 ⊆ On → ( 𝑦 ∈ 𝑆 → ( 𝑥 ∈ 𝑦 → ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑦 ) ) ) )
62 61 reximdvai ⊢ ( 𝑆 ⊆ On → ( ∃ 𝑦 ∈ 𝑆 𝑥 ∈ 𝑦 → ∃ 𝑦 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑦 ) ) )
63 48 62 biimtrid ⊢ ( 𝑆 ⊆ On → ( 𝑥 ∈ ∪ 𝑆 → ∃ 𝑦 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑦 ) ) )
64 ssiun ⊢ ( ∃ 𝑦 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑦 ) → ( 𝐹 ‘ 𝑥 ) ⊆ ∪ 𝑦 ∈ 𝑆 ( 𝐹 ‘ 𝑦 ) )
65 63 64 syl6 ⊢ ( 𝑆 ⊆ On → ( 𝑥 ∈ ∪ 𝑆 → ( 𝐹 ‘ 𝑥 ) ⊆ ∪ 𝑦 ∈ 𝑆 ( 𝐹 ‘ 𝑦 ) ) )
66 65 ralrimiv ⊢ ( 𝑆 ⊆ On → ∀ 𝑥 ∈ ∪ 𝑆 ( 𝐹 ‘ 𝑥 ) ⊆ ∪ 𝑦 ∈ 𝑆 ( 𝐹 ‘ 𝑦 ) )
67 iunss ⊢ ( ∪ 𝑥 ∈ ∪ 𝑆 ( 𝐹 ‘ 𝑥 ) ⊆ ∪ 𝑦 ∈ 𝑆 ( 𝐹 ‘ 𝑦 ) ↔ ∀ 𝑥 ∈ ∪ 𝑆 ( 𝐹 ‘ 𝑥 ) ⊆ ∪ 𝑦 ∈ 𝑆 ( 𝐹 ‘ 𝑦 ) )
68 66 67 sylibr ⊢ ( 𝑆 ⊆ On → ∪ 𝑥 ∈ ∪ 𝑆 ( 𝐹 ‘ 𝑥 ) ⊆ ∪ 𝑦 ∈ 𝑆 ( 𝐹 ‘ 𝑦 ) )
69 fveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
70 69 cbviunv ⊢ ∪ 𝑦 ∈ 𝑆 ( 𝐹 ‘ 𝑦 ) = ∪ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 )
71 68 70 sseqtrdi ⊢ ( 𝑆 ⊆ On → ∪ 𝑥 ∈ ∪ 𝑆 ( 𝐹 ‘ 𝑥 ) ⊆ ∪ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) )
72 71 3ad2ant2 ⊢ ( ( 𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅ ) → ∪ 𝑥 ∈ ∪ 𝑆 ( 𝐹 ‘ 𝑥 ) ⊆ ∪ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) )
73 72 adantr ⊢ ( ( ( 𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅ ) ∧ ¬ ∪ 𝑆 ∈ 𝑆 ) → ∪ 𝑥 ∈ ∪ 𝑆 ( 𝐹 ‘ 𝑥 ) ⊆ ∪ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) )
74 47 73 eqsstrd ⊢ ( ( ( 𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅ ) ∧ ¬ ∪ 𝑆 ∈ 𝑆 ) → ( 𝐹 ‘ ∪ 𝑆 ) ⊆ ∪ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) )
75 74 ex ⊢ ( ( 𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅ ) → ( ¬ ∪ 𝑆 ∈ 𝑆 → ( 𝐹 ‘ ∪ 𝑆 ) ⊆ ∪ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) ) )
76 fveq2 ⊢ ( 𝑥 = ∪ 𝑆 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ∪ 𝑆 ) )
77 76 ssiun2s ⊢ ( ∪ 𝑆 ∈ 𝑆 → ( 𝐹 ‘ ∪ 𝑆 ) ⊆ ∪ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) )
78 75 77 pm2.61d2 ⊢ ( ( 𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅ ) → ( 𝐹 ‘ ∪ 𝑆 ) ⊆ ∪ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) )
79 36 imp ⊢ ( ( 𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ) → ∪ 𝑆 ∈ On )
80 79 3adant3 ⊢ ( ( 𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅ ) → ∪ 𝑆 ∈ On )
81 8 3ad2ant2 ⊢ ( ( 𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅ ) → ( 𝑥 ∈ 𝑆 → 𝑥 ∈ On ) )
82 81 6 jca2 ⊢ ( ( 𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅ ) → ( 𝑥 ∈ 𝑆 → ( 𝑥 ∈ On ∧ 𝑥 ⊆ ∪ 𝑆 ) ) )
83 sseq2 ⊢ ( 𝑦 = ∪ 𝑆 → ( 𝑥 ⊆ 𝑦 ↔ 𝑥 ⊆ ∪ 𝑆 ) )
84 83 anbi2d ⊢ ( 𝑦 = ∪ 𝑆 → ( ( 𝑥 ∈ On ∧ 𝑥 ⊆ 𝑦 ) ↔ ( 𝑥 ∈ On ∧ 𝑥 ⊆ ∪ 𝑆 ) ) )
85 38 sseq2d ⊢ ( 𝑦 = ∪ 𝑆 → ( ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ∪ 𝑆 ) ) )
86 84 85 imbi12d ⊢ ( 𝑦 = ∪ 𝑆 → ( ( ( 𝑥 ∈ On ∧ 𝑥 ⊆ 𝑦 ) → ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑦 ) ) ↔ ( ( 𝑥 ∈ On ∧ 𝑥 ⊆ ∪ 𝑆 ) → ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ∪ 𝑆 ) ) ) )
87 2 3com12 ⊢ ( ( 𝑦 ∈ On ∧ 𝑥 ∈ On ∧ 𝑥 ⊆ 𝑦 ) → ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑦 ) )
88 87 3expib ⊢ ( 𝑦 ∈ On → ( ( 𝑥 ∈ On ∧ 𝑥 ⊆ 𝑦 ) → ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑦 ) ) )
89 86 88 vtoclga ⊢ ( ∪ 𝑆 ∈ On → ( ( 𝑥 ∈ On ∧ 𝑥 ⊆ ∪ 𝑆 ) → ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ∪ 𝑆 ) ) )
90 80 82 89 sylsyld ⊢ ( ( 𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅ ) → ( 𝑥 ∈ 𝑆 → ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ∪ 𝑆 ) ) )
91 90 ralrimiv ⊢ ( ( 𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅ ) → ∀ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ∪ 𝑆 ) )
92 iunss ⊢ ( ∪ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ∪ 𝑆 ) ↔ ∀ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ∪ 𝑆 ) )
93 91 92 sylibr ⊢ ( ( 𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅ ) → ∪ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ∪ 𝑆 ) )
94 78 93 eqssd ⊢ ( ( 𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅ ) → ( 𝐹 ‘ ∪ 𝑆 ) = ∪ 𝑥 ∈ 𝑆 ( 𝐹 ‘ 𝑥 ) )