Step | Hyp | Ref
| Expression |
1 | | oveq2 6658 |
. . . . . 6
⊢ (𝑗 = 1 → (1...𝑗) = (1...1)) |
2 | 1 | iuneq1d 4545 |
. . . . 5
⊢ (𝑗 = 1 → ∪ 𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = ∪ 𝑛 ∈ (1...1)(𝐹‘𝑛)) |
3 | | fveq2 6191 |
. . . . 5
⊢ (𝑗 = 1 → (𝐹‘𝑗) = (𝐹‘1)) |
4 | 2, 3 | eqeq12d 2637 |
. . . 4
⊢ (𝑗 = 1 → (∪ 𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = (𝐹‘𝑗) ↔ ∪
𝑛 ∈ (1...1)(𝐹‘𝑛) = (𝐹‘1))) |
5 | 4 | imbi2d 330 |
. . 3
⊢ (𝑗 = 1 → ((𝜑 → ∪
𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = (𝐹‘𝑗)) ↔ (𝜑 → ∪
𝑛 ∈ (1...1)(𝐹‘𝑛) = (𝐹‘1)))) |
6 | | oveq2 6658 |
. . . . . 6
⊢ (𝑗 = 𝑘 → (1...𝑗) = (1...𝑘)) |
7 | 6 | iuneq1d 4545 |
. . . . 5
⊢ (𝑗 = 𝑘 → ∪
𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛)) |
8 | | fveq2 6191 |
. . . . 5
⊢ (𝑗 = 𝑘 → (𝐹‘𝑗) = (𝐹‘𝑘)) |
9 | 7, 8 | eqeq12d 2637 |
. . . 4
⊢ (𝑗 = 𝑘 → (∪
𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = (𝐹‘𝑗) ↔ ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘))) |
10 | 9 | imbi2d 330 |
. . 3
⊢ (𝑗 = 𝑘 → ((𝜑 → ∪
𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = (𝐹‘𝑗)) ↔ (𝜑 → ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘)))) |
11 | | oveq2 6658 |
. . . . . 6
⊢ (𝑗 = (𝑘 + 1) → (1...𝑗) = (1...(𝑘 + 1))) |
12 | 11 | iuneq1d 4545 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → ∪ 𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛)) |
13 | | fveq2 6191 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → (𝐹‘𝑗) = (𝐹‘(𝑘 + 1))) |
14 | 12, 13 | eqeq12d 2637 |
. . . 4
⊢ (𝑗 = (𝑘 + 1) → (∪ 𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = (𝐹‘𝑗) ↔ ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) = (𝐹‘(𝑘 + 1)))) |
15 | 14 | imbi2d 330 |
. . 3
⊢ (𝑗 = (𝑘 + 1) → ((𝜑 → ∪
𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = (𝐹‘𝑗)) ↔ (𝜑 → ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) = (𝐹‘(𝑘 + 1))))) |
16 | | oveq2 6658 |
. . . . . 6
⊢ (𝑗 = 𝑖 → (1...𝑗) = (1...𝑖)) |
17 | 16 | iuneq1d 4545 |
. . . . 5
⊢ (𝑗 = 𝑖 → ∪
𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = ∪ 𝑛 ∈ (1...𝑖)(𝐹‘𝑛)) |
18 | | fveq2 6191 |
. . . . 5
⊢ (𝑗 = 𝑖 → (𝐹‘𝑗) = (𝐹‘𝑖)) |
19 | 17, 18 | eqeq12d 2637 |
. . . 4
⊢ (𝑗 = 𝑖 → (∪
𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = (𝐹‘𝑗) ↔ ∪
𝑛 ∈ (1...𝑖)(𝐹‘𝑛) = (𝐹‘𝑖))) |
20 | 19 | imbi2d 330 |
. . 3
⊢ (𝑗 = 𝑖 → ((𝜑 → ∪
𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = (𝐹‘𝑗)) ↔ (𝜑 → ∪
𝑛 ∈ (1...𝑖)(𝐹‘𝑛) = (𝐹‘𝑖)))) |
21 | | 1z 11407 |
. . . . . . 7
⊢ 1 ∈
ℤ |
22 | | fzsn 12383 |
. . . . . . 7
⊢ (1 ∈
ℤ → (1...1) = {1}) |
23 | 21, 22 | ax-mp 5 |
. . . . . 6
⊢ (1...1) =
{1} |
24 | | iuneq1 4534 |
. . . . . 6
⊢ ((1...1)
= {1} → ∪ 𝑛 ∈ (1...1)(𝐹‘𝑛) = ∪ 𝑛 ∈ {1} (𝐹‘𝑛)) |
25 | 23, 24 | ax-mp 5 |
. . . . 5
⊢ ∪ 𝑛 ∈ (1...1)(𝐹‘𝑛) = ∪ 𝑛 ∈ {1} (𝐹‘𝑛) |
26 | | 1ex 10035 |
. . . . . 6
⊢ 1 ∈
V |
27 | | fveq2 6191 |
. . . . . 6
⊢ (𝑛 = 1 → (𝐹‘𝑛) = (𝐹‘1)) |
28 | 26, 27 | iunxsn 4603 |
. . . . 5
⊢ ∪ 𝑛 ∈ {1} (𝐹‘𝑛) = (𝐹‘1) |
29 | 25, 28 | eqtri 2644 |
. . . 4
⊢ ∪ 𝑛 ∈ (1...1)(𝐹‘𝑛) = (𝐹‘1) |
30 | 29 | a1i 11 |
. . 3
⊢ (𝜑 → ∪ 𝑛 ∈ (1...1)(𝐹‘𝑛) = (𝐹‘1)) |
31 | | simpll 790 |
. . . . . . 7
⊢ (((𝑘 ∈ ℕ ∧ 𝜑) ∧ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘)) → 𝑘 ∈ ℕ) |
32 | | elnnuz 11724 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ ↔ 𝑘 ∈
(ℤ≥‘1)) |
33 | | fzsuc 12388 |
. . . . . . . . . 10
⊢ (𝑘 ∈
(ℤ≥‘1) → (1...(𝑘 + 1)) = ((1...𝑘) ∪ {(𝑘 + 1)})) |
34 | 32, 33 | sylbi 207 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ →
(1...(𝑘 + 1)) = ((1...𝑘) ∪ {(𝑘 + 1)})) |
35 | 34 | iuneq1d 4545 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) = ∪ 𝑛 ∈ ((1...𝑘) ∪ {(𝑘 + 1)})(𝐹‘𝑛)) |
36 | | iunxun 4605 |
. . . . . . . . 9
⊢ ∪ 𝑛 ∈ ((1...𝑘) ∪ {(𝑘 + 1)})(𝐹‘𝑛) = (∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∪ ∪
𝑛 ∈ {(𝑘 + 1)} (𝐹‘𝑛)) |
37 | | ovex 6678 |
. . . . . . . . . . 11
⊢ (𝑘 + 1) ∈ V |
38 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝑘 + 1) → (𝐹‘𝑛) = (𝐹‘(𝑘 + 1))) |
39 | 37, 38 | iunxsn 4603 |
. . . . . . . . . 10
⊢ ∪ 𝑛 ∈ {(𝑘 + 1)} (𝐹‘𝑛) = (𝐹‘(𝑘 + 1)) |
40 | 39 | uneq2i 3764 |
. . . . . . . . 9
⊢ (∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∪ ∪
𝑛 ∈ {(𝑘 + 1)} (𝐹‘𝑛)) = (∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∪ (𝐹‘(𝑘 + 1))) |
41 | 36, 40 | eqtri 2644 |
. . . . . . . 8
⊢ ∪ 𝑛 ∈ ((1...𝑘) ∪ {(𝑘 + 1)})(𝐹‘𝑛) = (∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∪ (𝐹‘(𝑘 + 1))) |
42 | 35, 41 | syl6eq 2672 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) = (∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∪ (𝐹‘(𝑘 + 1)))) |
43 | 31, 42 | syl 17 |
. . . . . 6
⊢ (((𝑘 ∈ ℕ ∧ 𝜑) ∧ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘)) → ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) = (∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∪ (𝐹‘(𝑘 + 1)))) |
44 | | simpr 477 |
. . . . . . 7
⊢ (((𝑘 ∈ ℕ ∧ 𝜑) ∧ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘)) → ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘)) |
45 | 44 | uneq1d 3766 |
. . . . . 6
⊢ (((𝑘 ∈ ℕ ∧ 𝜑) ∧ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘)) → (∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∪ (𝐹‘(𝑘 + 1))) = ((𝐹‘𝑘) ∪ (𝐹‘(𝑘 + 1)))) |
46 | | simplr 792 |
. . . . . . 7
⊢ (((𝑘 ∈ ℕ ∧ 𝜑) ∧ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘)) → 𝜑) |
47 | | iuninc.2 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) |
48 | 47 | sbt 2419 |
. . . . . . . . 9
⊢ [𝑘 / 𝑛]((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) |
49 | | sbim 2395 |
. . . . . . . . . 10
⊢ ([𝑘 / 𝑛]((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ↔ ([𝑘 / 𝑛](𝜑 ∧ 𝑛 ∈ ℕ) → [𝑘 / 𝑛](𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)))) |
50 | | sban 2399 |
. . . . . . . . . . . 12
⊢ ([𝑘 / 𝑛](𝜑 ∧ 𝑛 ∈ ℕ) ↔ ([𝑘 / 𝑛]𝜑 ∧ [𝑘 / 𝑛]𝑛 ∈ ℕ)) |
51 | | nfv 1843 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛𝜑 |
52 | 51 | sbf 2380 |
. . . . . . . . . . . . 13
⊢ ([𝑘 / 𝑛]𝜑 ↔ 𝜑) |
53 | | clelsb3 2729 |
. . . . . . . . . . . . 13
⊢ ([𝑘 / 𝑛]𝑛 ∈ ℕ ↔ 𝑘 ∈ ℕ) |
54 | 52, 53 | anbi12i 733 |
. . . . . . . . . . . 12
⊢ (([𝑘 / 𝑛]𝜑 ∧ [𝑘 / 𝑛]𝑛 ∈ ℕ) ↔ (𝜑 ∧ 𝑘 ∈ ℕ)) |
55 | 50, 54 | bitr2i 265 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) ↔ [𝑘 / 𝑛](𝜑 ∧ 𝑛 ∈ ℕ)) |
56 | | sbsbc 3439 |
. . . . . . . . . . . 12
⊢ ([𝑘 / 𝑛](𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)) ↔ [𝑘 / 𝑛](𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) |
57 | | vex 3203 |
. . . . . . . . . . . . 13
⊢ 𝑘 ∈ V |
58 | | sbcssg 4085 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ V → ([𝑘 / 𝑛](𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)) ↔ ⦋𝑘 / 𝑛⦌(𝐹‘𝑛) ⊆ ⦋𝑘 / 𝑛⦌(𝐹‘(𝑛 + 1)))) |
59 | 57, 58 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
([𝑘 / 𝑛](𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)) ↔ ⦋𝑘 / 𝑛⦌(𝐹‘𝑛) ⊆ ⦋𝑘 / 𝑛⦌(𝐹‘(𝑛 + 1))) |
60 | | csbfv 6233 |
. . . . . . . . . . . . 13
⊢
⦋𝑘 /
𝑛⦌(𝐹‘𝑛) = (𝐹‘𝑘) |
61 | | csbfv2g 6232 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ V →
⦋𝑘 / 𝑛⦌(𝐹‘(𝑛 + 1)) = (𝐹‘⦋𝑘 / 𝑛⦌(𝑛 + 1))) |
62 | 57, 61 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
⦋𝑘 /
𝑛⦌(𝐹‘(𝑛 + 1)) = (𝐹‘⦋𝑘 / 𝑛⦌(𝑛 + 1)) |
63 | | csbov1g 6690 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ V →
⦋𝑘 / 𝑛⦌(𝑛 + 1) = (⦋𝑘 / 𝑛⦌𝑛 + 1)) |
64 | 57, 63 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
⦋𝑘 /
𝑛⦌(𝑛 + 1) = (⦋𝑘 / 𝑛⦌𝑛 + 1) |
65 | 64 | fveq2i 6194 |
. . . . . . . . . . . . . 14
⊢ (𝐹‘⦋𝑘 / 𝑛⦌(𝑛 + 1)) = (𝐹‘(⦋𝑘 / 𝑛⦌𝑛 + 1)) |
66 | | csbvarg 4003 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ V →
⦋𝑘 / 𝑛⦌𝑛 = 𝑘) |
67 | 57, 66 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
⦋𝑘 /
𝑛⦌𝑛 = 𝑘 |
68 | 67 | oveq1i 6660 |
. . . . . . . . . . . . . . 15
⊢
(⦋𝑘 /
𝑛⦌𝑛 + 1) = (𝑘 + 1) |
69 | 68 | fveq2i 6194 |
. . . . . . . . . . . . . 14
⊢ (𝐹‘(⦋𝑘 / 𝑛⦌𝑛 + 1)) = (𝐹‘(𝑘 + 1)) |
70 | 62, 65, 69 | 3eqtri 2648 |
. . . . . . . . . . . . 13
⊢
⦋𝑘 /
𝑛⦌(𝐹‘(𝑛 + 1)) = (𝐹‘(𝑘 + 1)) |
71 | 60, 70 | sseq12i 3631 |
. . . . . . . . . . . 12
⊢
(⦋𝑘 /
𝑛⦌(𝐹‘𝑛) ⊆ ⦋𝑘 / 𝑛⦌(𝐹‘(𝑛 + 1)) ↔ (𝐹‘𝑘) ⊆ (𝐹‘(𝑘 + 1))) |
72 | 56, 59, 71 | 3bitrri 287 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑘) ⊆ (𝐹‘(𝑘 + 1)) ↔ [𝑘 / 𝑛](𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) |
73 | 55, 72 | imbi12i 340 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ⊆ (𝐹‘(𝑘 + 1))) ↔ ([𝑘 / 𝑛](𝜑 ∧ 𝑛 ∈ ℕ) → [𝑘 / 𝑛](𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)))) |
74 | 49, 73 | bitr4i 267 |
. . . . . . . . 9
⊢ ([𝑘 / 𝑛]((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ↔ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ⊆ (𝐹‘(𝑘 + 1)))) |
75 | 48, 74 | mpbi 220 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ⊆ (𝐹‘(𝑘 + 1))) |
76 | | ssequn1 3783 |
. . . . . . . 8
⊢ ((𝐹‘𝑘) ⊆ (𝐹‘(𝑘 + 1)) ↔ ((𝐹‘𝑘) ∪ (𝐹‘(𝑘 + 1))) = (𝐹‘(𝑘 + 1))) |
77 | 75, 76 | sylib 208 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘) ∪ (𝐹‘(𝑘 + 1))) = (𝐹‘(𝑘 + 1))) |
78 | 46, 31, 77 | syl2anc 693 |
. . . . . 6
⊢ (((𝑘 ∈ ℕ ∧ 𝜑) ∧ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘)) → ((𝐹‘𝑘) ∪ (𝐹‘(𝑘 + 1))) = (𝐹‘(𝑘 + 1))) |
79 | 43, 45, 78 | 3eqtrd 2660 |
. . . . 5
⊢ (((𝑘 ∈ ℕ ∧ 𝜑) ∧ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘)) → ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) = (𝐹‘(𝑘 + 1))) |
80 | 79 | exp31 630 |
. . . 4
⊢ (𝑘 ∈ ℕ → (𝜑 → (∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘) → ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) = (𝐹‘(𝑘 + 1))))) |
81 | 80 | a2d 29 |
. . 3
⊢ (𝑘 ∈ ℕ → ((𝜑 → ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘)) → (𝜑 → ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) = (𝐹‘(𝑘 + 1))))) |
82 | 5, 10, 15, 20, 30, 81 | nnind 11038 |
. 2
⊢ (𝑖 ∈ ℕ → (𝜑 → ∪ 𝑛 ∈ (1...𝑖)(𝐹‘𝑛) = (𝐹‘𝑖))) |
83 | 82 | impcom 446 |
1
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ∪ 𝑛 ∈ (1...𝑖)(𝐹‘𝑛) = (𝐹‘𝑖)) |