Proof of Theorem onfununi
| Step | Hyp | Ref
| Expression |
| 1 | | ssorduni 7799 |
. . . . . . . . . 10
⊢ (𝑆 ⊆ On → Ord ∪ 𝑆) |
| 2 | 1 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝑆 ⊆ On ∧ ¬ ∪ 𝑆
∈ 𝑆) ∧ 𝑆 ≠ ∅) → Ord ∪ 𝑆) |
| 3 | | nelneq 2865 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝑆 ∧ ¬ ∪
𝑆 ∈ 𝑆) → ¬ 𝑥 = ∪ 𝑆) |
| 4 | | elssuni 4937 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ 𝑆 → 𝑥 ⊆ ∪ 𝑆) |
| 5 | 4 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → 𝑥 ⊆ ∪ 𝑆) |
| 6 | | ssel 3977 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑆 ⊆ On → (𝑥 ∈ 𝑆 → 𝑥 ∈ On)) |
| 7 | | eloni 6394 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ On → Ord 𝑥) |
| 8 | 6, 7 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑆 ⊆ On → (𝑥 ∈ 𝑆 → Ord 𝑥)) |
| 9 | 8 | imp 406 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑆 ⊆ On ∧ 𝑥 ∈ 𝑆) → Ord 𝑥) |
| 10 | | ordsseleq 6413 |
. . . . . . . . . . . . . . . . . . . . 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 865 |
. . . . . . . . . . . . . . . . 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 3989 |
. . . . . . . . . 10
⊢ ((𝑆 ⊆ On ∧ ¬ ∪ 𝑆
∈ 𝑆) → 𝑆 ⊆ ∪ 𝑆) |
| 22 | | ssn0 4404 |
. . . . . . . . . 10
⊢ ((𝑆 ⊆ ∪ 𝑆
∧ 𝑆 ≠ ∅)
→ ∪ 𝑆 ≠ ∅) |
| 23 | 21, 22 | sylan 580 |
. . . . . . . . 9
⊢ (((𝑆 ⊆ On ∧ ¬ ∪ 𝑆
∈ 𝑆) ∧ 𝑆 ≠ ∅) → ∪ 𝑆
≠ ∅) |
| 24 | 21 | unissd 4917 |
. . . . . . . . . . 11
⊢ ((𝑆 ⊆ On ∧ ¬ ∪ 𝑆
∈ 𝑆) → ∪ 𝑆
⊆ ∪ ∪ 𝑆) |
| 25 | | orduniss 6481 |
. . . . . . . . . . . . 13
⊢ (Ord
∪ 𝑆 → ∪ ∪ 𝑆
⊆ ∪ 𝑆) |
| 26 | 1, 25 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑆 ⊆ On → ∪ ∪ 𝑆 ⊆ ∪ 𝑆) |
| 27 | 26 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑆 ⊆ On ∧ ¬ ∪ 𝑆
∈ 𝑆) → ∪ ∪ 𝑆 ⊆ ∪ 𝑆) |
| 28 | 24, 27 | eqssd 4001 |
. . . . . . . . . 10
⊢ ((𝑆 ⊆ On ∧ ¬ ∪ 𝑆
∈ 𝑆) → ∪ 𝑆 =
∪ ∪ 𝑆) |
| 29 | 28 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑆 ⊆ On ∧ ¬ ∪ 𝑆
∈ 𝑆) ∧ 𝑆 ≠ ∅) → ∪ 𝑆 =
∪ ∪ 𝑆) |
| 30 | | df-lim 6389 |
. . . . . . . . 9
⊢ (Lim
∪ 𝑆 ↔ (Ord ∪
𝑆 ∧ ∪ 𝑆
≠ ∅ ∧ ∪ 𝑆 = ∪ ∪ 𝑆)) |
| 31 | 2, 23, 29, 30 | syl3anbrc 1344 |
. . . . . . . 8
⊢ (((𝑆 ⊆ On ∧ ¬ ∪ 𝑆
∈ 𝑆) ∧ 𝑆 ≠ ∅) → Lim ∪ 𝑆) |
| 32 | 31 | an32s 652 |
. . . . . . 7
⊢ (((𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆
∈ 𝑆) → Lim ∪ 𝑆) |
| 33 | 32 | 3adantl1 1167 |
. . . . . 6
⊢ (((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆
∈ 𝑆) → Lim ∪ 𝑆) |
| 34 | | ssonuni 7800 |
. . . . . . . . . 10
⊢ (𝑆 ∈ 𝑇 → (𝑆 ⊆ On → ∪ 𝑆
∈ On)) |
| 35 | | limeq 6396 |
. . . . . . . . . . . 12
⊢ (𝑦 = ∪
𝑆 → (Lim 𝑦 ↔ Lim ∪ 𝑆)) |
| 36 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ∪
𝑆 → (𝐹‘𝑦) = (𝐹‘∪ 𝑆)) |
| 37 | | iuneq1 5008 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ∪
𝑆 → ∪ 𝑥 ∈ 𝑦 (𝐹‘𝑥) = ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥)) |
| 38 | 36, 37 | eqeq12d 2753 |
. . . . . . . . . . . 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 1133 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (Lim ∪ 𝑆
→ (𝐹‘∪ 𝑆) =
∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥))) |
| 45 | 44 | adantr 480 |
. . . . . 6
⊢ (((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆
∈ 𝑆) → (Lim ∪ 𝑆
→ (𝐹‘∪ 𝑆) =
∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥))) |
| 46 | 33, 45 | mpd 15 |
. . . . 5
⊢ (((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆
∈ 𝑆) → (𝐹‘∪ 𝑆) =
∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥)) |
| 47 | | eluni2 4911 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ∪ 𝑆
↔ ∃𝑦 ∈
𝑆 𝑥 ∈ 𝑦) |
| 48 | | ssel 3977 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑆 ⊆ On → (𝑦 ∈ 𝑆 → 𝑦 ∈ On)) |
| 49 | 48 | anim1d 611 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → (𝑦 ∈ On ∧ 𝑥 ∈ 𝑦))) |
| 50 | | onelon 6409 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ On) |
| 51 | 49, 50 | syl6 35 |
. . . . . . . . . . . . . . . 16
⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ On)) |
| 52 | 48 | adantrd 491 |
. . . . . . . . . . . . . . . 16
⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → 𝑦 ∈ On)) |
| 53 | | eloni 6394 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ On → Ord 𝑦) |
| 54 | 48, 53 | syl6 35 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑆 ⊆ On → (𝑦 ∈ 𝑆 → Ord 𝑦)) |
| 55 | | ordelss 6400 |
. . . . . . . . . . . . . . . . . 18
⊢ ((Ord
𝑦 ∧ 𝑥 ∈ 𝑦) → 𝑥 ⊆ 𝑦) |
| 56 | 55 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑆 ⊆ On → ((Ord 𝑦 ∧ 𝑥 ∈ 𝑦) → 𝑥 ⊆ 𝑦)) |
| 57 | 54, 56 | syland 603 |
. . . . . . . . . . . . . . . 16
⊢ (𝑆 ⊆ On → ((𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑦) → 𝑥 ⊆ 𝑦)) |
| 58 | 51, 52, 57 | 3jcad 1130 |
. . . . . . . . . . . . . . 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 3165 |
. . . . . . . . . . . 12
⊢ (𝑆 ⊆ On → (∃𝑦 ∈ 𝑆 𝑥 ∈ 𝑦 → ∃𝑦 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘𝑦))) |
| 63 | 47, 62 | biimtrid 242 |
. . . . . . . . . . 11
⊢ (𝑆 ⊆ On → (𝑥 ∈ ∪ 𝑆
→ ∃𝑦 ∈
𝑆 (𝐹‘𝑥) ⊆ (𝐹‘𝑦))) |
| 64 | | ssiun 5046 |
. . . . . . . . . . 11
⊢
(∃𝑦 ∈
𝑆 (𝐹‘𝑥) ⊆ (𝐹‘𝑦) → (𝐹‘𝑥) ⊆ ∪
𝑦 ∈ 𝑆 (𝐹‘𝑦)) |
| 65 | 63, 64 | syl6 35 |
. . . . . . . . . 10
⊢ (𝑆 ⊆ On → (𝑥 ∈ ∪ 𝑆
→ (𝐹‘𝑥) ⊆ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦))) |
| 66 | 65 | ralrimiv 3145 |
. . . . . . . . 9
⊢ (𝑆 ⊆ On → ∀𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪
𝑦 ∈ 𝑆 (𝐹‘𝑦)) |
| 67 | | iunss 5045 |
. . . . . . . . 9
⊢ (∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪
𝑦 ∈ 𝑆 (𝐹‘𝑦) ↔ ∀𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪
𝑦 ∈ 𝑆 (𝐹‘𝑦)) |
| 68 | 66, 67 | sylibr 234 |
. . . . . . . 8
⊢ (𝑆 ⊆ On → ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪
𝑦 ∈ 𝑆 (𝐹‘𝑦)) |
| 69 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥)) |
| 70 | 69 | cbviunv 5040 |
. . . . . . . 8
⊢ ∪ 𝑦 ∈ 𝑆 (𝐹‘𝑦) = ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥) |
| 71 | 68, 70 | sseqtrdi 4024 |
. . . . . . 7
⊢ (𝑆 ⊆ On → ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪
𝑥 ∈ 𝑆 (𝐹‘𝑥)) |
| 72 | 71 | 3ad2ant2 1135 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪
𝑥 ∈ 𝑆 (𝐹‘𝑥)) |
| 73 | 72 | adantr 480 |
. . . . 5
⊢ (((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆
∈ 𝑆) → ∪ 𝑥 ∈ ∪ 𝑆(𝐹‘𝑥) ⊆ ∪
𝑥 ∈ 𝑆 (𝐹‘𝑥)) |
| 74 | 46, 73 | eqsstrd 4018 |
. . . 4
⊢ (((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) ∧ ¬ ∪ 𝑆
∈ 𝑆) → (𝐹‘∪ 𝑆)
⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥)) |
| 75 | 74 | ex 412 |
. . 3
⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (¬ ∪ 𝑆
∈ 𝑆 → (𝐹‘∪ 𝑆)
⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥))) |
| 76 | | fveq2 6906 |
. . . 4
⊢ (𝑥 = ∪
𝑆 → (𝐹‘𝑥) = (𝐹‘∪ 𝑆)) |
| 77 | 76 | ssiun2s 5048 |
. . 3
⊢ (∪ 𝑆
∈ 𝑆 → (𝐹‘∪ 𝑆)
⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥)) |
| 78 | 75, 77 | pm2.61d2 181 |
. 2
⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝐹‘∪ 𝑆) ⊆ ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥)) |
| 79 | 34 | imp 406 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On) → ∪ 𝑆
∈ On) |
| 80 | 79 | 3adant3 1133 |
. . . . 5
⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → ∪ 𝑆
∈ On) |
| 81 | 6 | 3ad2ant2 1135 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝑥 ∈ 𝑆 → 𝑥 ∈ On)) |
| 82 | 81, 4 | jca2 513 |
. . . . 5
⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝑥 ∈ 𝑆 → (𝑥 ∈ On ∧ 𝑥 ⊆ ∪ 𝑆))) |
| 83 | | sseq2 4010 |
. . . . . . . 8
⊢ (𝑦 = ∪
𝑆 → (𝑥 ⊆ 𝑦 ↔ 𝑥 ⊆ ∪ 𝑆)) |
| 84 | 83 | anbi2d 630 |
. . . . . . 7
⊢ (𝑦 = ∪
𝑆 → ((𝑥 ∈ On ∧ 𝑥 ⊆ 𝑦) ↔ (𝑥 ∈ On ∧ 𝑥 ⊆ ∪ 𝑆))) |
| 85 | 36 | sseq2d 4016 |
. . . . . . 7
⊢ (𝑦 = ∪
𝑆 → ((𝐹‘𝑥) ⊆ (𝐹‘𝑦) ↔ (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆))) |
| 86 | 84, 85 | imbi12d 344 |
. . . . . 6
⊢ (𝑦 = ∪
𝑆 → (((𝑥 ∈ On ∧ 𝑥 ⊆ 𝑦) → (𝐹‘𝑥) ⊆ (𝐹‘𝑦)) ↔ ((𝑥 ∈ On ∧ 𝑥 ⊆ ∪ 𝑆) → (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆)))) |
| 87 | 59 | 3com12 1124 |
. . . . . . 7
⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ On ∧ 𝑥 ⊆ 𝑦) → (𝐹‘𝑥) ⊆ (𝐹‘𝑦)) |
| 88 | 87 | 3expib 1123 |
. . . . . 6
⊢ (𝑦 ∈ On → ((𝑥 ∈ On ∧ 𝑥 ⊆ 𝑦) → (𝐹‘𝑥) ⊆ (𝐹‘𝑦))) |
| 89 | 86, 88 | vtoclga 3577 |
. . . . 5
⊢ (∪ 𝑆
∈ On → ((𝑥 ∈
On ∧ 𝑥 ⊆ ∪ 𝑆)
→ (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆))) |
| 90 | 80, 82, 89 | sylsyld 61 |
. . . 4
⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝑥 ∈ 𝑆 → (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆))) |
| 91 | 90 | ralrimiv 3145 |
. . 3
⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → ∀𝑥 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆)) |
| 92 | | iunss 5045 |
. . 3
⊢ (∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆) ↔ ∀𝑥 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆)) |
| 93 | 91, 92 | sylibr 234 |
. 2
⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥) ⊆ (𝐹‘∪ 𝑆)) |
| 94 | 78, 93 | eqssd 4001 |
1
⊢ ((𝑆 ∈ 𝑇 ∧ 𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → (𝐹‘∪ 𝑆) = ∪ 𝑥 ∈ 𝑆 (𝐹‘𝑥)) |