Step | Hyp | Ref
| Expression |
1 | | oveq2 7279 |
. . . . . 6
⊢ (𝑗 = 1 → (1...𝑗) = (1...1)) |
2 | 1 | iuneq1d 4957 |
. . . . 5
⊢ (𝑗 = 1 → ∪ 𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = ∪ 𝑛 ∈ (1...1)(𝐹‘𝑛)) |
3 | | fveq2 6771 |
. . . . 5
⊢ (𝑗 = 1 → (𝐹‘𝑗) = (𝐹‘1)) |
4 | 2, 3 | eqeq12d 2756 |
. . . 4
⊢ (𝑗 = 1 → (∪ 𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = (𝐹‘𝑗) ↔ ∪
𝑛 ∈ (1...1)(𝐹‘𝑛) = (𝐹‘1))) |
5 | 4 | imbi2d 341 |
. . 3
⊢ (𝑗 = 1 → ((𝜑 → ∪
𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = (𝐹‘𝑗)) ↔ (𝜑 → ∪
𝑛 ∈ (1...1)(𝐹‘𝑛) = (𝐹‘1)))) |
6 | | oveq2 7279 |
. . . . . 6
⊢ (𝑗 = 𝑘 → (1...𝑗) = (1...𝑘)) |
7 | 6 | iuneq1d 4957 |
. . . . 5
⊢ (𝑗 = 𝑘 → ∪
𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛)) |
8 | | fveq2 6771 |
. . . . 5
⊢ (𝑗 = 𝑘 → (𝐹‘𝑗) = (𝐹‘𝑘)) |
9 | 7, 8 | eqeq12d 2756 |
. . . 4
⊢ (𝑗 = 𝑘 → (∪
𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = (𝐹‘𝑗) ↔ ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘))) |
10 | 9 | imbi2d 341 |
. . 3
⊢ (𝑗 = 𝑘 → ((𝜑 → ∪
𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = (𝐹‘𝑗)) ↔ (𝜑 → ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘)))) |
11 | | oveq2 7279 |
. . . . . 6
⊢ (𝑗 = (𝑘 + 1) → (1...𝑗) = (1...(𝑘 + 1))) |
12 | 11 | iuneq1d 4957 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → ∪ 𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛)) |
13 | | fveq2 6771 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → (𝐹‘𝑗) = (𝐹‘(𝑘 + 1))) |
14 | 12, 13 | eqeq12d 2756 |
. . . 4
⊢ (𝑗 = (𝑘 + 1) → (∪ 𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = (𝐹‘𝑗) ↔ ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) = (𝐹‘(𝑘 + 1)))) |
15 | 14 | imbi2d 341 |
. . 3
⊢ (𝑗 = (𝑘 + 1) → ((𝜑 → ∪
𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = (𝐹‘𝑗)) ↔ (𝜑 → ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) = (𝐹‘(𝑘 + 1))))) |
16 | | oveq2 7279 |
. . . . . 6
⊢ (𝑗 = 𝑖 → (1...𝑗) = (1...𝑖)) |
17 | 16 | iuneq1d 4957 |
. . . . 5
⊢ (𝑗 = 𝑖 → ∪
𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = ∪ 𝑛 ∈ (1...𝑖)(𝐹‘𝑛)) |
18 | | fveq2 6771 |
. . . . 5
⊢ (𝑗 = 𝑖 → (𝐹‘𝑗) = (𝐹‘𝑖)) |
19 | 17, 18 | eqeq12d 2756 |
. . . 4
⊢ (𝑗 = 𝑖 → (∪
𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = (𝐹‘𝑗) ↔ ∪
𝑛 ∈ (1...𝑖)(𝐹‘𝑛) = (𝐹‘𝑖))) |
20 | 19 | imbi2d 341 |
. . 3
⊢ (𝑗 = 𝑖 → ((𝜑 → ∪
𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = (𝐹‘𝑗)) ↔ (𝜑 → ∪
𝑛 ∈ (1...𝑖)(𝐹‘𝑛) = (𝐹‘𝑖)))) |
21 | | 1z 12350 |
. . . . . 6
⊢ 1 ∈
ℤ |
22 | | fzsn 13297 |
. . . . . 6
⊢ (1 ∈
ℤ → (1...1) = {1}) |
23 | | iuneq1 4946 |
. . . . . 6
⊢ ((1...1)
= {1} → ∪ 𝑛 ∈ (1...1)(𝐹‘𝑛) = ∪ 𝑛 ∈ {1} (𝐹‘𝑛)) |
24 | 21, 22, 23 | mp2b 10 |
. . . . 5
⊢ ∪ 𝑛 ∈ (1...1)(𝐹‘𝑛) = ∪ 𝑛 ∈ {1} (𝐹‘𝑛) |
25 | | 1ex 10972 |
. . . . . 6
⊢ 1 ∈
V |
26 | | fveq2 6771 |
. . . . . 6
⊢ (𝑛 = 1 → (𝐹‘𝑛) = (𝐹‘1)) |
27 | 25, 26 | iunxsn 5025 |
. . . . 5
⊢ ∪ 𝑛 ∈ {1} (𝐹‘𝑛) = (𝐹‘1) |
28 | 24, 27 | eqtri 2768 |
. . . 4
⊢ ∪ 𝑛 ∈ (1...1)(𝐹‘𝑛) = (𝐹‘1) |
29 | 28 | a1i 11 |
. . 3
⊢ (𝜑 → ∪ 𝑛 ∈ (1...1)(𝐹‘𝑛) = (𝐹‘1)) |
30 | | simpll 764 |
. . . . . . 7
⊢ (((𝑘 ∈ ℕ ∧ 𝜑) ∧ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘)) → 𝑘 ∈ ℕ) |
31 | | elnnuz 12621 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ ↔ 𝑘 ∈
(ℤ≥‘1)) |
32 | | fzsuc 13302 |
. . . . . . . . . 10
⊢ (𝑘 ∈
(ℤ≥‘1) → (1...(𝑘 + 1)) = ((1...𝑘) ∪ {(𝑘 + 1)})) |
33 | 31, 32 | sylbi 216 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ →
(1...(𝑘 + 1)) = ((1...𝑘) ∪ {(𝑘 + 1)})) |
34 | 33 | iuneq1d 4957 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) = ∪ 𝑛 ∈ ((1...𝑘) ∪ {(𝑘 + 1)})(𝐹‘𝑛)) |
35 | | iunxun 5028 |
. . . . . . . . 9
⊢ ∪ 𝑛 ∈ ((1...𝑘) ∪ {(𝑘 + 1)})(𝐹‘𝑛) = (∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∪ ∪
𝑛 ∈ {(𝑘 + 1)} (𝐹‘𝑛)) |
36 | | ovex 7304 |
. . . . . . . . . . 11
⊢ (𝑘 + 1) ∈ V |
37 | | fveq2 6771 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝑘 + 1) → (𝐹‘𝑛) = (𝐹‘(𝑘 + 1))) |
38 | 36, 37 | iunxsn 5025 |
. . . . . . . . . 10
⊢ ∪ 𝑛 ∈ {(𝑘 + 1)} (𝐹‘𝑛) = (𝐹‘(𝑘 + 1)) |
39 | 38 | uneq2i 4099 |
. . . . . . . . 9
⊢ (∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∪ ∪
𝑛 ∈ {(𝑘 + 1)} (𝐹‘𝑛)) = (∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∪ (𝐹‘(𝑘 + 1))) |
40 | 35, 39 | eqtri 2768 |
. . . . . . . 8
⊢ ∪ 𝑛 ∈ ((1...𝑘) ∪ {(𝑘 + 1)})(𝐹‘𝑛) = (∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∪ (𝐹‘(𝑘 + 1))) |
41 | 34, 40 | eqtrdi 2796 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) = (∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∪ (𝐹‘(𝑘 + 1)))) |
42 | 30, 41 | syl 17 |
. . . . . 6
⊢ (((𝑘 ∈ ℕ ∧ 𝜑) ∧ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘)) → ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) = (∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∪ (𝐹‘(𝑘 + 1)))) |
43 | | simpr 485 |
. . . . . . 7
⊢ (((𝑘 ∈ ℕ ∧ 𝜑) ∧ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘)) → ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘)) |
44 | 43 | uneq1d 4101 |
. . . . . 6
⊢ (((𝑘 ∈ ℕ ∧ 𝜑) ∧ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘)) → (∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∪ (𝐹‘(𝑘 + 1))) = ((𝐹‘𝑘) ∪ (𝐹‘(𝑘 + 1)))) |
45 | | simplr 766 |
. . . . . . 7
⊢ (((𝑘 ∈ ℕ ∧ 𝜑) ∧ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘)) → 𝜑) |
46 | | iuninc.2 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) |
47 | 46 | sbt 2073 |
. . . . . . . . 9
⊢ [𝑘 / 𝑛]((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) |
48 | | sbim 2304 |
. . . . . . . . . 10
⊢ ([𝑘 / 𝑛]((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ↔ ([𝑘 / 𝑛](𝜑 ∧ 𝑛 ∈ ℕ) → [𝑘 / 𝑛](𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)))) |
49 | | sban 2087 |
. . . . . . . . . . . 12
⊢ ([𝑘 / 𝑛](𝜑 ∧ 𝑛 ∈ ℕ) ↔ ([𝑘 / 𝑛]𝜑 ∧ [𝑘 / 𝑛]𝑛 ∈ ℕ)) |
50 | | sbv 2095 |
. . . . . . . . . . . . 13
⊢ ([𝑘 / 𝑛]𝜑 ↔ 𝜑) |
51 | | clelsb1 2868 |
. . . . . . . . . . . . 13
⊢ ([𝑘 / 𝑛]𝑛 ∈ ℕ ↔ 𝑘 ∈ ℕ) |
52 | 50, 51 | anbi12i 627 |
. . . . . . . . . . . 12
⊢ (([𝑘 / 𝑛]𝜑 ∧ [𝑘 / 𝑛]𝑛 ∈ ℕ) ↔ (𝜑 ∧ 𝑘 ∈ ℕ)) |
53 | 49, 52 | bitr2i 275 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) ↔ [𝑘 / 𝑛](𝜑 ∧ 𝑛 ∈ ℕ)) |
54 | | sbsbc 3724 |
. . . . . . . . . . . 12
⊢ ([𝑘 / 𝑛](𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)) ↔ [𝑘 / 𝑛](𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) |
55 | | sbcssg 4460 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ V → ([𝑘 / 𝑛](𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)) ↔ ⦋𝑘 / 𝑛⦌(𝐹‘𝑛) ⊆ ⦋𝑘 / 𝑛⦌(𝐹‘(𝑛 + 1)))) |
56 | 55 | elv 3437 |
. . . . . . . . . . . 12
⊢
([𝑘 / 𝑛](𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)) ↔ ⦋𝑘 / 𝑛⦌(𝐹‘𝑛) ⊆ ⦋𝑘 / 𝑛⦌(𝐹‘(𝑛 + 1))) |
57 | | csbfv 6816 |
. . . . . . . . . . . . 13
⊢
⦋𝑘 /
𝑛⦌(𝐹‘𝑛) = (𝐹‘𝑘) |
58 | | csbfv2g 6815 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ V →
⦋𝑘 / 𝑛⦌(𝐹‘(𝑛 + 1)) = (𝐹‘⦋𝑘 / 𝑛⦌(𝑛 + 1))) |
59 | 58 | elv 3437 |
. . . . . . . . . . . . . 14
⊢
⦋𝑘 /
𝑛⦌(𝐹‘(𝑛 + 1)) = (𝐹‘⦋𝑘 / 𝑛⦌(𝑛 + 1)) |
60 | | csbov1g 7316 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ V →
⦋𝑘 / 𝑛⦌(𝑛 + 1) = (⦋𝑘 / 𝑛⦌𝑛 + 1)) |
61 | 60 | elv 3437 |
. . . . . . . . . . . . . . 15
⊢
⦋𝑘 /
𝑛⦌(𝑛 + 1) = (⦋𝑘 / 𝑛⦌𝑛 + 1) |
62 | 61 | fveq2i 6774 |
. . . . . . . . . . . . . 14
⊢ (𝐹‘⦋𝑘 / 𝑛⦌(𝑛 + 1)) = (𝐹‘(⦋𝑘 / 𝑛⦌𝑛 + 1)) |
63 | | vex 3435 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑘 ∈ V |
64 | 63 | csbvargi 4372 |
. . . . . . . . . . . . . . . 16
⊢
⦋𝑘 /
𝑛⦌𝑛 = 𝑘 |
65 | 64 | oveq1i 7281 |
. . . . . . . . . . . . . . 15
⊢
(⦋𝑘 /
𝑛⦌𝑛 + 1) = (𝑘 + 1) |
66 | 65 | fveq2i 6774 |
. . . . . . . . . . . . . 14
⊢ (𝐹‘(⦋𝑘 / 𝑛⦌𝑛 + 1)) = (𝐹‘(𝑘 + 1)) |
67 | 59, 62, 66 | 3eqtri 2772 |
. . . . . . . . . . . . 13
⊢
⦋𝑘 /
𝑛⦌(𝐹‘(𝑛 + 1)) = (𝐹‘(𝑘 + 1)) |
68 | 57, 67 | sseq12i 3956 |
. . . . . . . . . . . 12
⊢
(⦋𝑘 /
𝑛⦌(𝐹‘𝑛) ⊆ ⦋𝑘 / 𝑛⦌(𝐹‘(𝑛 + 1)) ↔ (𝐹‘𝑘) ⊆ (𝐹‘(𝑘 + 1))) |
69 | 54, 56, 68 | 3bitrri 298 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑘) ⊆ (𝐹‘(𝑘 + 1)) ↔ [𝑘 / 𝑛](𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) |
70 | 53, 69 | imbi12i 351 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ⊆ (𝐹‘(𝑘 + 1))) ↔ ([𝑘 / 𝑛](𝜑 ∧ 𝑛 ∈ ℕ) → [𝑘 / 𝑛](𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)))) |
71 | 48, 70 | bitr4i 277 |
. . . . . . . . 9
⊢ ([𝑘 / 𝑛]((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ↔ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ⊆ (𝐹‘(𝑘 + 1)))) |
72 | 47, 71 | mpbi 229 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ⊆ (𝐹‘(𝑘 + 1))) |
73 | | ssequn1 4119 |
. . . . . . . 8
⊢ ((𝐹‘𝑘) ⊆ (𝐹‘(𝑘 + 1)) ↔ ((𝐹‘𝑘) ∪ (𝐹‘(𝑘 + 1))) = (𝐹‘(𝑘 + 1))) |
74 | 72, 73 | sylib 217 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘) ∪ (𝐹‘(𝑘 + 1))) = (𝐹‘(𝑘 + 1))) |
75 | 45, 30, 74 | syl2anc 584 |
. . . . . 6
⊢ (((𝑘 ∈ ℕ ∧ 𝜑) ∧ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘)) → ((𝐹‘𝑘) ∪ (𝐹‘(𝑘 + 1))) = (𝐹‘(𝑘 + 1))) |
76 | 42, 44, 75 | 3eqtrd 2784 |
. . . . 5
⊢ (((𝑘 ∈ ℕ ∧ 𝜑) ∧ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘)) → ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) = (𝐹‘(𝑘 + 1))) |
77 | 76 | exp31 420 |
. . . 4
⊢ (𝑘 ∈ ℕ → (𝜑 → (∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘) → ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) = (𝐹‘(𝑘 + 1))))) |
78 | 77 | a2d 29 |
. . 3
⊢ (𝑘 ∈ ℕ → ((𝜑 → ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘)) → (𝜑 → ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) = (𝐹‘(𝑘 + 1))))) |
79 | 5, 10, 15, 20, 29, 78 | nnind 11991 |
. 2
⊢ (𝑖 ∈ ℕ → (𝜑 → ∪ 𝑛 ∈ (1...𝑖)(𝐹‘𝑛) = (𝐹‘𝑖))) |
80 | 79 | impcom 408 |
1
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ∪ 𝑛 ∈ (1...𝑖)(𝐹‘𝑛) = (𝐹‘𝑖)) |