Step | Hyp | Ref
| Expression |
1 | | eliun 4460 |
. . . . . . 7
⊢ (𝑥 ∈ ∪ 𝑛 ∈ (𝑀...𝑁)(𝐹‘𝑛) ↔ ∃𝑛 ∈ (𝑀...𝑁)𝑥 ∈ (𝐹‘𝑛)) |
2 | 1 | biimpi 205 |
. . . . . 6
⊢ (𝑥 ∈ ∪ 𝑛 ∈ (𝑀...𝑁)(𝐹‘𝑛) → ∃𝑛 ∈ (𝑀...𝑁)𝑥 ∈ (𝐹‘𝑛)) |
3 | 2 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ (𝑀...𝑁)(𝐹‘𝑛)) → ∃𝑛 ∈ (𝑀...𝑁)𝑥 ∈ (𝐹‘𝑛)) |
4 | | elfzuz3 12210 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝑛)) |
5 | 4 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) → 𝑁 ∈ (ℤ≥‘𝑛)) |
6 | | simpll 786 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) ∧ 𝑚 ∈ (𝑛..^𝑁)) → 𝜑) |
7 | | elfzuz 12209 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (𝑀...𝑁) → 𝑛 ∈ (ℤ≥‘𝑀)) |
8 | | fzoss1 12364 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈
(ℤ≥‘𝑀) → (𝑛..^𝑁) ⊆ (𝑀..^𝑁)) |
9 | 7, 8 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ (𝑀...𝑁) → (𝑛..^𝑁) ⊆ (𝑀..^𝑁)) |
10 | 9 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ (𝑀...𝑁) ∧ 𝑚 ∈ (𝑛..^𝑁)) → (𝑛..^𝑁) ⊆ (𝑀..^𝑁)) |
11 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ (𝑀...𝑁) ∧ 𝑚 ∈ (𝑛..^𝑁)) → 𝑚 ∈ (𝑛..^𝑁)) |
12 | 10, 11 | sseldd 3569 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ (𝑀...𝑁) ∧ 𝑚 ∈ (𝑛..^𝑁)) → 𝑚 ∈ (𝑀..^𝑁)) |
13 | 12 | adantll 746 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) ∧ 𝑚 ∈ (𝑛..^𝑁)) → 𝑚 ∈ (𝑀..^𝑁)) |
14 | | eleq1 2676 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → (𝑛 ∈ (𝑀..^𝑁) ↔ 𝑚 ∈ (𝑀..^𝑁))) |
15 | 14 | anbi2d 736 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) ↔ (𝜑 ∧ 𝑚 ∈ (𝑀..^𝑁)))) |
16 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → (𝐹‘𝑛) = (𝐹‘𝑚)) |
17 | | oveq1 6556 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → (𝑛 + 1) = (𝑚 + 1)) |
18 | 17 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → (𝐹‘(𝑛 + 1)) = (𝐹‘(𝑚 + 1))) |
19 | 16, 18 | sseq12d 3597 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → ((𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)) ↔ (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 + 1)))) |
20 | 15, 19 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → (((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ↔ ((𝜑 ∧ 𝑚 ∈ (𝑀..^𝑁)) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 + 1))))) |
21 | | iunincfi.2 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) |
22 | 20, 21 | chvarv 2251 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (𝑀..^𝑁)) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 + 1))) |
23 | 6, 13, 22 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) ∧ 𝑚 ∈ (𝑛..^𝑁)) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 + 1))) |
24 | 5, 23 | ssinc 38292 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁)) → (𝐹‘𝑛) ⊆ (𝐹‘𝑁)) |
25 | 24 | 3adant3 1074 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁) ∧ 𝑥 ∈ (𝐹‘𝑛)) → (𝐹‘𝑛) ⊆ (𝐹‘𝑁)) |
26 | | simp3 1056 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁) ∧ 𝑥 ∈ (𝐹‘𝑛)) → 𝑥 ∈ (𝐹‘𝑛)) |
27 | 25, 26 | sseldd 3569 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑁) ∧ 𝑥 ∈ (𝐹‘𝑛)) → 𝑥 ∈ (𝐹‘𝑁)) |
28 | 27 | 3exp 1256 |
. . . . . . 7
⊢ (𝜑 → (𝑛 ∈ (𝑀...𝑁) → (𝑥 ∈ (𝐹‘𝑛) → 𝑥 ∈ (𝐹‘𝑁)))) |
29 | 28 | rexlimdv 3012 |
. . . . . 6
⊢ (𝜑 → (∃𝑛 ∈ (𝑀...𝑁)𝑥 ∈ (𝐹‘𝑛) → 𝑥 ∈ (𝐹‘𝑁))) |
30 | 29 | imp 444 |
. . . . 5
⊢ ((𝜑 ∧ ∃𝑛 ∈ (𝑀...𝑁)𝑥 ∈ (𝐹‘𝑛)) → 𝑥 ∈ (𝐹‘𝑁)) |
31 | 3, 30 | syldan 486 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ (𝑀...𝑁)(𝐹‘𝑛)) → 𝑥 ∈ (𝐹‘𝑁)) |
32 | 31 | ralrimiva 2949 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ ∪
𝑛 ∈ (𝑀...𝑁)(𝐹‘𝑛)𝑥 ∈ (𝐹‘𝑁)) |
33 | | dfss3 3558 |
. . 3
⊢ (∪ 𝑛 ∈ (𝑀...𝑁)(𝐹‘𝑛) ⊆ (𝐹‘𝑁) ↔ ∀𝑥 ∈ ∪
𝑛 ∈ (𝑀...𝑁)(𝐹‘𝑛)𝑥 ∈ (𝐹‘𝑁)) |
34 | 32, 33 | sylibr 223 |
. 2
⊢ (𝜑 → ∪ 𝑛 ∈ (𝑀...𝑁)(𝐹‘𝑛) ⊆ (𝐹‘𝑁)) |
35 | | iunincfi.1 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
36 | | eluzfz2 12220 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁)) |
37 | 35, 36 | syl 17 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁)) |
38 | | fveq2 6103 |
. . . 4
⊢ (𝑛 = 𝑁 → (𝐹‘𝑛) = (𝐹‘𝑁)) |
39 | 38 | ssiun2s 4500 |
. . 3
⊢ (𝑁 ∈ (𝑀...𝑁) → (𝐹‘𝑁) ⊆ ∪ 𝑛 ∈ (𝑀...𝑁)(𝐹‘𝑛)) |
40 | 37, 39 | syl 17 |
. 2
⊢ (𝜑 → (𝐹‘𝑁) ⊆ ∪ 𝑛 ∈ (𝑀...𝑁)(𝐹‘𝑛)) |
41 | 34, 40 | eqssd 3585 |
1
⊢ (𝜑 → ∪ 𝑛 ∈ (𝑀...𝑁)(𝐹‘𝑛) = (𝐹‘𝑁)) |