Step | Hyp | Ref
| Expression |
1 | | eliun 4895 |
. . . . . . 7
⊢ (𝑥 ∈ ∪ 𝑛 ∈ (𝑀...𝑁)(𝐹‘𝑛) ↔ ∃𝑛 ∈ (𝑀...𝑁)𝑥 ∈ (𝐹‘𝑛)) |
2 | 1 | biimpi 219 |
. . . . . 6
⊢ (𝑥 ∈ ∪ 𝑛 ∈ (𝑀...𝑁)(𝐹‘𝑛) → ∃𝑛 ∈ (𝑀...𝑁)𝑥 ∈ (𝐹‘𝑛)) |
3 | 2 | adantl 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ (𝑀...𝑁)(𝐹‘𝑛)) → ∃𝑛 ∈ (𝑀...𝑁)𝑥 ∈ (𝐹‘𝑛)) |
4 | | elfzuz3 13008 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝑛)) |
5 | 4 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) → 𝑁 ∈ (ℤ≥‘𝑛)) |
6 | | simpll 767 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) ∧ 𝑚 ∈ (𝑛..^𝑁)) → 𝜑) |
7 | | elfzuz 13007 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (𝑀...𝑁) → 𝑛 ∈ (ℤ≥‘𝑀)) |
8 | | fzoss1 13168 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → (𝑛..^𝑁) ⊆ (𝑀..^𝑁)) |
9 | 7, 8 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ (𝑀...𝑁) → (𝑛..^𝑁) ⊆ (𝑀..^𝑁)) |
10 | 9 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ (𝑀...𝑁) ∧ 𝑚 ∈ (𝑛..^𝑁)) → (𝑛..^𝑁) ⊆ (𝑀..^𝑁)) |
11 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ (𝑀...𝑁) ∧ 𝑚 ∈ (𝑛..^𝑁)) → 𝑚 ∈ (𝑛..^𝑁)) |
12 | 10, 11 | sseldd 3888 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ (𝑀...𝑁) ∧ 𝑚 ∈ (𝑛..^𝑁)) → 𝑚 ∈ (𝑀..^𝑁)) |
13 | 12 | adantll 714 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) ∧ 𝑚 ∈ (𝑛..^𝑁)) → 𝑚 ∈ (𝑀..^𝑁)) |
14 | | eleq1w 2816 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → (𝑛 ∈ (𝑀..^𝑁) ↔ 𝑚 ∈ (𝑀..^𝑁))) |
15 | 14 | anbi2d 632 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) ↔ (𝜑 ∧ 𝑚 ∈ (𝑀..^𝑁)))) |
16 | | fveq2 6687 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → (𝐹‘𝑛) = (𝐹‘𝑚)) |
17 | | fvoveq1 7206 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → (𝐹‘(𝑛 + 1)) = (𝐹‘(𝑚 + 1))) |
18 | 16, 17 | sseq12d 3920 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → ((𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)) ↔ (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 + 1)))) |
19 | 15, 18 | imbi12d 348 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → (((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ↔ ((𝜑 ∧ 𝑚 ∈ (𝑀..^𝑁)) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 + 1))))) |
20 | | iunincfi.2 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) |
21 | 19, 20 | chvarvv 2010 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀..^𝑁)) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 + 1))) |
22 | 6, 13, 21 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) ∧ 𝑚 ∈ (𝑛..^𝑁)) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 + 1))) |
23 | 5, 22 | ssinc 42216 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) → (𝐹‘𝑛) ⊆ (𝐹‘𝑁)) |
24 | 23 | 3adant3 1133 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁) ∧ 𝑥 ∈ (𝐹‘𝑛)) → (𝐹‘𝑛) ⊆ (𝐹‘𝑁)) |
25 | | simp3 1139 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁) ∧ 𝑥 ∈ (𝐹‘𝑛)) → 𝑥 ∈ (𝐹‘𝑛)) |
26 | 24, 25 | sseldd 3888 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁) ∧ 𝑥 ∈ (𝐹‘𝑛)) → 𝑥 ∈ (𝐹‘𝑁)) |
27 | 26 | 3exp 1120 |
. . . . . . 7
⊢ (𝜑 → (𝑛 ∈ (𝑀...𝑁) → (𝑥 ∈ (𝐹‘𝑛) → 𝑥 ∈ (𝐹‘𝑁)))) |
28 | 27 | rexlimdv 3194 |
. . . . . 6
⊢ (𝜑 → (∃𝑛 ∈ (𝑀...𝑁)𝑥 ∈ (𝐹‘𝑛) → 𝑥 ∈ (𝐹‘𝑁))) |
29 | 28 | imp 410 |
. . . . 5
⊢ ((𝜑 ∧ ∃𝑛 ∈ (𝑀...𝑁)𝑥 ∈ (𝐹‘𝑛)) → 𝑥 ∈ (𝐹‘𝑁)) |
30 | 3, 29 | syldan 594 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ (𝑀...𝑁)(𝐹‘𝑛)) → 𝑥 ∈ (𝐹‘𝑁)) |
31 | 30 | ralrimiva 3097 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ ∪
𝑛 ∈ (𝑀...𝑁)(𝐹‘𝑛)𝑥 ∈ (𝐹‘𝑁)) |
32 | | dfss3 3875 |
. . 3
⊢ (∪ 𝑛 ∈ (𝑀...𝑁)(𝐹‘𝑛) ⊆ (𝐹‘𝑁) ↔ ∀𝑥 ∈ ∪
𝑛 ∈ (𝑀...𝑁)(𝐹‘𝑛)𝑥 ∈ (𝐹‘𝑁)) |
33 | 31, 32 | sylibr 237 |
. 2
⊢ (𝜑 → ∪ 𝑛 ∈ (𝑀...𝑁)(𝐹‘𝑛) ⊆ (𝐹‘𝑁)) |
34 | | iunincfi.1 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
35 | | eluzfz2 13019 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁)) |
36 | 34, 35 | syl 17 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁)) |
37 | | fveq2 6687 |
. . . 4
⊢ (𝑛 = 𝑁 → (𝐹‘𝑛) = (𝐹‘𝑁)) |
38 | 37 | ssiun2s 4944 |
. . 3
⊢ (𝑁 ∈ (𝑀...𝑁) → (𝐹‘𝑁) ⊆ ∪ 𝑛 ∈ (𝑀...𝑁)(𝐹‘𝑛)) |
39 | 36, 38 | syl 17 |
. 2
⊢ (𝜑 → (𝐹‘𝑁) ⊆ ∪ 𝑛 ∈ (𝑀...𝑁)(𝐹‘𝑛)) |
40 | 33, 39 | eqssd 3904 |
1
⊢ (𝜑 → ∪ 𝑛 ∈ (𝑀...𝑁)(𝐹‘𝑛) = (𝐹‘𝑁)) |