| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq2 7440 | . . . . . 6
⊢ (𝑗 = 1 → (1...𝑗) = (1...1)) | 
| 2 | 1 | iuneq1d 5018 | . . . . 5
⊢ (𝑗 = 1 → ∪ 𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = ∪ 𝑛 ∈ (1...1)(𝐹‘𝑛)) | 
| 3 |  | fveq2 6905 | . . . . 5
⊢ (𝑗 = 1 → (𝐹‘𝑗) = (𝐹‘1)) | 
| 4 | 2, 3 | eqeq12d 2752 | . . . 4
⊢ (𝑗 = 1 → (∪ 𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = (𝐹‘𝑗) ↔ ∪
𝑛 ∈ (1...1)(𝐹‘𝑛) = (𝐹‘1))) | 
| 5 | 4 | imbi2d 340 | . . 3
⊢ (𝑗 = 1 → ((𝜑 → ∪
𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = (𝐹‘𝑗)) ↔ (𝜑 → ∪
𝑛 ∈ (1...1)(𝐹‘𝑛) = (𝐹‘1)))) | 
| 6 |  | oveq2 7440 | . . . . . 6
⊢ (𝑗 = 𝑘 → (1...𝑗) = (1...𝑘)) | 
| 7 | 6 | iuneq1d 5018 | . . . . 5
⊢ (𝑗 = 𝑘 → ∪
𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛)) | 
| 8 |  | fveq2 6905 | . . . . 5
⊢ (𝑗 = 𝑘 → (𝐹‘𝑗) = (𝐹‘𝑘)) | 
| 9 | 7, 8 | eqeq12d 2752 | . . . 4
⊢ (𝑗 = 𝑘 → (∪
𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = (𝐹‘𝑗) ↔ ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘))) | 
| 10 | 9 | imbi2d 340 | . . 3
⊢ (𝑗 = 𝑘 → ((𝜑 → ∪
𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = (𝐹‘𝑗)) ↔ (𝜑 → ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘)))) | 
| 11 |  | oveq2 7440 | . . . . . 6
⊢ (𝑗 = (𝑘 + 1) → (1...𝑗) = (1...(𝑘 + 1))) | 
| 12 | 11 | iuneq1d 5018 | . . . . 5
⊢ (𝑗 = (𝑘 + 1) → ∪ 𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛)) | 
| 13 |  | fveq2 6905 | . . . . 5
⊢ (𝑗 = (𝑘 + 1) → (𝐹‘𝑗) = (𝐹‘(𝑘 + 1))) | 
| 14 | 12, 13 | eqeq12d 2752 | . . . 4
⊢ (𝑗 = (𝑘 + 1) → (∪ 𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = (𝐹‘𝑗) ↔ ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) = (𝐹‘(𝑘 + 1)))) | 
| 15 | 14 | imbi2d 340 | . . 3
⊢ (𝑗 = (𝑘 + 1) → ((𝜑 → ∪
𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = (𝐹‘𝑗)) ↔ (𝜑 → ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) = (𝐹‘(𝑘 + 1))))) | 
| 16 |  | oveq2 7440 | . . . . . 6
⊢ (𝑗 = 𝑖 → (1...𝑗) = (1...𝑖)) | 
| 17 | 16 | iuneq1d 5018 | . . . . 5
⊢ (𝑗 = 𝑖 → ∪
𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = ∪ 𝑛 ∈ (1...𝑖)(𝐹‘𝑛)) | 
| 18 |  | fveq2 6905 | . . . . 5
⊢ (𝑗 = 𝑖 → (𝐹‘𝑗) = (𝐹‘𝑖)) | 
| 19 | 17, 18 | eqeq12d 2752 | . . . 4
⊢ (𝑗 = 𝑖 → (∪
𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = (𝐹‘𝑗) ↔ ∪
𝑛 ∈ (1...𝑖)(𝐹‘𝑛) = (𝐹‘𝑖))) | 
| 20 | 19 | imbi2d 340 | . . 3
⊢ (𝑗 = 𝑖 → ((𝜑 → ∪
𝑛 ∈ (1...𝑗)(𝐹‘𝑛) = (𝐹‘𝑗)) ↔ (𝜑 → ∪
𝑛 ∈ (1...𝑖)(𝐹‘𝑛) = (𝐹‘𝑖)))) | 
| 21 |  | 1z 12649 | . . . . . 6
⊢ 1 ∈
ℤ | 
| 22 |  | fzsn 13607 | . . . . . 6
⊢ (1 ∈
ℤ → (1...1) = {1}) | 
| 23 |  | iuneq1 5007 | . . . . . 6
⊢ ((1...1)
= {1} → ∪ 𝑛 ∈ (1...1)(𝐹‘𝑛) = ∪ 𝑛 ∈ {1} (𝐹‘𝑛)) | 
| 24 | 21, 22, 23 | mp2b 10 | . . . . 5
⊢ ∪ 𝑛 ∈ (1...1)(𝐹‘𝑛) = ∪ 𝑛 ∈ {1} (𝐹‘𝑛) | 
| 25 |  | 1ex 11258 | . . . . . 6
⊢ 1 ∈
V | 
| 26 |  | fveq2 6905 | . . . . . 6
⊢ (𝑛 = 1 → (𝐹‘𝑛) = (𝐹‘1)) | 
| 27 | 25, 26 | iunxsn 5090 | . . . . 5
⊢ ∪ 𝑛 ∈ {1} (𝐹‘𝑛) = (𝐹‘1) | 
| 28 | 24, 27 | eqtri 2764 | . . . 4
⊢ ∪ 𝑛 ∈ (1...1)(𝐹‘𝑛) = (𝐹‘1) | 
| 29 | 28 | a1i 11 | . . 3
⊢ (𝜑 → ∪ 𝑛 ∈ (1...1)(𝐹‘𝑛) = (𝐹‘1)) | 
| 30 |  | simpll 766 | . . . . . . 7
⊢ (((𝑘 ∈ ℕ ∧ 𝜑) ∧ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘)) → 𝑘 ∈ ℕ) | 
| 31 |  | elnnuz 12923 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ ↔ 𝑘 ∈
(ℤ≥‘1)) | 
| 32 |  | fzsuc 13612 | . . . . . . . . . 10
⊢ (𝑘 ∈
(ℤ≥‘1) → (1...(𝑘 + 1)) = ((1...𝑘) ∪ {(𝑘 + 1)})) | 
| 33 | 31, 32 | sylbi 217 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ →
(1...(𝑘 + 1)) = ((1...𝑘) ∪ {(𝑘 + 1)})) | 
| 34 | 33 | iuneq1d 5018 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ → ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) = ∪ 𝑛 ∈ ((1...𝑘) ∪ {(𝑘 + 1)})(𝐹‘𝑛)) | 
| 35 |  | iunxun 5093 | . . . . . . . . 9
⊢ ∪ 𝑛 ∈ ((1...𝑘) ∪ {(𝑘 + 1)})(𝐹‘𝑛) = (∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∪ ∪
𝑛 ∈ {(𝑘 + 1)} (𝐹‘𝑛)) | 
| 36 |  | ovex 7465 | . . . . . . . . . . 11
⊢ (𝑘 + 1) ∈ V | 
| 37 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑛 = (𝑘 + 1) → (𝐹‘𝑛) = (𝐹‘(𝑘 + 1))) | 
| 38 | 36, 37 | iunxsn 5090 | . . . . . . . . . 10
⊢ ∪ 𝑛 ∈ {(𝑘 + 1)} (𝐹‘𝑛) = (𝐹‘(𝑘 + 1)) | 
| 39 | 38 | uneq2i 4164 | . . . . . . . . 9
⊢ (∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∪ ∪
𝑛 ∈ {(𝑘 + 1)} (𝐹‘𝑛)) = (∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∪ (𝐹‘(𝑘 + 1))) | 
| 40 | 35, 39 | eqtri 2764 | . . . . . . . 8
⊢ ∪ 𝑛 ∈ ((1...𝑘) ∪ {(𝑘 + 1)})(𝐹‘𝑛) = (∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∪ (𝐹‘(𝑘 + 1))) | 
| 41 | 34, 40 | eqtrdi 2792 | . . . . . . 7
⊢ (𝑘 ∈ ℕ → ∪ 𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) = (∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∪ (𝐹‘(𝑘 + 1)))) | 
| 42 | 30, 41 | syl 17 | . . . . . 6
⊢ (((𝑘 ∈ ℕ ∧ 𝜑) ∧ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘)) → ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) = (∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∪ (𝐹‘(𝑘 + 1)))) | 
| 43 |  | simpr 484 | . . . . . . 7
⊢ (((𝑘 ∈ ℕ ∧ 𝜑) ∧ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘)) → ∪
𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘)) | 
| 44 | 43 | uneq1d 4166 | . . . . . 6
⊢ (((𝑘 ∈ ℕ ∧ 𝜑) ∧ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘)) → (∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) ∪ (𝐹‘(𝑘 + 1))) = ((𝐹‘𝑘) ∪ (𝐹‘(𝑘 + 1)))) | 
| 45 |  | simplr 768 | . . . . . . 7
⊢ (((𝑘 ∈ ℕ ∧ 𝜑) ∧ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘)) → 𝜑) | 
| 46 |  | iuninc.2 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) | 
| 47 | 46 | sbt 2065 | . . . . . . . . 9
⊢ [𝑘 / 𝑛]((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) | 
| 48 |  | sbim 2302 | . . . . . . . . . 10
⊢ ([𝑘 / 𝑛]((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ↔ ([𝑘 / 𝑛](𝜑 ∧ 𝑛 ∈ ℕ) → [𝑘 / 𝑛](𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)))) | 
| 49 |  | sban 2079 | . . . . . . . . . . . 12
⊢ ([𝑘 / 𝑛](𝜑 ∧ 𝑛 ∈ ℕ) ↔ ([𝑘 / 𝑛]𝜑 ∧ [𝑘 / 𝑛]𝑛 ∈ ℕ)) | 
| 50 |  | sbv 2087 | . . . . . . . . . . . . 13
⊢ ([𝑘 / 𝑛]𝜑 ↔ 𝜑) | 
| 51 |  | clelsb1 2867 | . . . . . . . . . . . . 13
⊢ ([𝑘 / 𝑛]𝑛 ∈ ℕ ↔ 𝑘 ∈ ℕ) | 
| 52 | 50, 51 | anbi12i 628 | . . . . . . . . . . . 12
⊢ (([𝑘 / 𝑛]𝜑 ∧ [𝑘 / 𝑛]𝑛 ∈ ℕ) ↔ (𝜑 ∧ 𝑘 ∈ ℕ)) | 
| 53 | 49, 52 | bitr2i 276 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) ↔ [𝑘 / 𝑛](𝜑 ∧ 𝑛 ∈ ℕ)) | 
| 54 |  | sbsbc 3791 | . . . . . . . . . . . 12
⊢ ([𝑘 / 𝑛](𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)) ↔ [𝑘 / 𝑛](𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) | 
| 55 |  | sbcssg 4519 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ V → ([𝑘 / 𝑛](𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)) ↔ ⦋𝑘 / 𝑛⦌(𝐹‘𝑛) ⊆ ⦋𝑘 / 𝑛⦌(𝐹‘(𝑛 + 1)))) | 
| 56 | 55 | elv 3484 | . . . . . . . . . . . 12
⊢
([𝑘 / 𝑛](𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)) ↔ ⦋𝑘 / 𝑛⦌(𝐹‘𝑛) ⊆ ⦋𝑘 / 𝑛⦌(𝐹‘(𝑛 + 1))) | 
| 57 |  | csbfv 6955 | . . . . . . . . . . . . 13
⊢
⦋𝑘 /
𝑛⦌(𝐹‘𝑛) = (𝐹‘𝑘) | 
| 58 |  | csbfv2g 6954 | . . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ V →
⦋𝑘 / 𝑛⦌(𝐹‘(𝑛 + 1)) = (𝐹‘⦋𝑘 / 𝑛⦌(𝑛 + 1))) | 
| 59 | 58 | elv 3484 | . . . . . . . . . . . . . 14
⊢
⦋𝑘 /
𝑛⦌(𝐹‘(𝑛 + 1)) = (𝐹‘⦋𝑘 / 𝑛⦌(𝑛 + 1)) | 
| 60 |  | csbov1g 7479 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ V →
⦋𝑘 / 𝑛⦌(𝑛 + 1) = (⦋𝑘 / 𝑛⦌𝑛 + 1)) | 
| 61 | 60 | elv 3484 | . . . . . . . . . . . . . . 15
⊢
⦋𝑘 /
𝑛⦌(𝑛 + 1) = (⦋𝑘 / 𝑛⦌𝑛 + 1) | 
| 62 | 61 | fveq2i 6908 | . . . . . . . . . . . . . 14
⊢ (𝐹‘⦋𝑘 / 𝑛⦌(𝑛 + 1)) = (𝐹‘(⦋𝑘 / 𝑛⦌𝑛 + 1)) | 
| 63 |  | vex 3483 | . . . . . . . . . . . . . . . . 17
⊢ 𝑘 ∈ V | 
| 64 | 63 | csbvargi 4434 | . . . . . . . . . . . . . . . 16
⊢
⦋𝑘 /
𝑛⦌𝑛 = 𝑘 | 
| 65 | 64 | oveq1i 7442 | . . . . . . . . . . . . . . 15
⊢
(⦋𝑘 /
𝑛⦌𝑛 + 1) = (𝑘 + 1) | 
| 66 | 65 | fveq2i 6908 | . . . . . . . . . . . . . 14
⊢ (𝐹‘(⦋𝑘 / 𝑛⦌𝑛 + 1)) = (𝐹‘(𝑘 + 1)) | 
| 67 | 59, 62, 66 | 3eqtri 2768 | . . . . . . . . . . . . 13
⊢
⦋𝑘 /
𝑛⦌(𝐹‘(𝑛 + 1)) = (𝐹‘(𝑘 + 1)) | 
| 68 | 57, 67 | sseq12i 4013 | . . . . . . . . . . . 12
⊢
(⦋𝑘 /
𝑛⦌(𝐹‘𝑛) ⊆ ⦋𝑘 / 𝑛⦌(𝐹‘(𝑛 + 1)) ↔ (𝐹‘𝑘) ⊆ (𝐹‘(𝑘 + 1))) | 
| 69 | 54, 56, 68 | 3bitrri 298 | . . . . . . . . . . 11
⊢ ((𝐹‘𝑘) ⊆ (𝐹‘(𝑘 + 1)) ↔ [𝑘 / 𝑛](𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) | 
| 70 | 53, 69 | imbi12i 350 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ⊆ (𝐹‘(𝑘 + 1))) ↔ ([𝑘 / 𝑛](𝜑 ∧ 𝑛 ∈ ℕ) → [𝑘 / 𝑛](𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1)))) | 
| 71 | 48, 70 | bitr4i 278 | . . . . . . . . 9
⊢ ([𝑘 / 𝑛]((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑛 + 1))) ↔ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ⊆ (𝐹‘(𝑘 + 1)))) | 
| 72 | 47, 71 | mpbi 230 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ⊆ (𝐹‘(𝑘 + 1))) | 
| 73 |  | ssequn1 4185 | . . . . . . . 8
⊢ ((𝐹‘𝑘) ⊆ (𝐹‘(𝑘 + 1)) ↔ ((𝐹‘𝑘) ∪ (𝐹‘(𝑘 + 1))) = (𝐹‘(𝑘 + 1))) | 
| 74 | 72, 73 | sylib 218 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘) ∪ (𝐹‘(𝑘 + 1))) = (𝐹‘(𝑘 + 1))) | 
| 75 | 45, 30, 74 | syl2anc 584 | . . . . . 6
⊢ (((𝑘 ∈ ℕ ∧ 𝜑) ∧ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘)) → ((𝐹‘𝑘) ∪ (𝐹‘(𝑘 + 1))) = (𝐹‘(𝑘 + 1))) | 
| 76 | 42, 44, 75 | 3eqtrd 2780 | . . . . 5
⊢ (((𝑘 ∈ ℕ ∧ 𝜑) ∧ ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘)) → ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) = (𝐹‘(𝑘 + 1))) | 
| 77 | 76 | exp31 419 | . . . 4
⊢ (𝑘 ∈ ℕ → (𝜑 → (∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘) → ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) = (𝐹‘(𝑘 + 1))))) | 
| 78 | 77 | a2d 29 | . . 3
⊢ (𝑘 ∈ ℕ → ((𝜑 → ∪ 𝑛 ∈ (1...𝑘)(𝐹‘𝑛) = (𝐹‘𝑘)) → (𝜑 → ∪
𝑛 ∈ (1...(𝑘 + 1))(𝐹‘𝑛) = (𝐹‘(𝑘 + 1))))) | 
| 79 | 5, 10, 15, 20, 29, 78 | nnind 12285 | . 2
⊢ (𝑖 ∈ ℕ → (𝜑 → ∪ 𝑛 ∈ (1...𝑖)(𝐹‘𝑛) = (𝐹‘𝑖))) | 
| 80 | 79 | impcom 407 | 1
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ∪ 𝑛 ∈ (1...𝑖)(𝐹‘𝑛) = (𝐹‘𝑖)) |