| Step | Hyp | Ref
| Expression |
| 1 | | incom 4209 |
. 2
⊢ ((𝐹‘𝐽) ∩ (𝐹‘𝐾)) = ((𝐹‘𝐾) ∩ (𝐹‘𝐽)) |
| 2 | | simpl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → 𝜑) |
| 3 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → 𝑥 ∈ (𝐹‘𝐾)) |
| 4 | | iundjiunlem.k |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈ 𝑍) |
| 5 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝐾 → (𝐸‘𝑛) = (𝐸‘𝐾)) |
| 6 | | oveq2 7439 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝐾 → (𝑁..^𝑛) = (𝑁..^𝐾)) |
| 7 | 6 | iuneq1d 5019 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝐾 → ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖)) |
| 8 | 5, 7 | difeq12d 4127 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝐾 → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) = ((𝐸‘𝐾) ∖ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖))) |
| 9 | | iundjiunlem.f |
. . . . . . . . . . . 12
⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
| 10 | | fvex 6919 |
. . . . . . . . . . . . 13
⊢ (𝐸‘𝐾) ∈ V |
| 11 | 10 | difexi 5330 |
. . . . . . . . . . . 12
⊢ ((𝐸‘𝐾) ∖ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖)) ∈ V |
| 12 | 8, 9, 11 | fvmpt 7016 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ 𝑍 → (𝐹‘𝐾) = ((𝐸‘𝐾) ∖ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖))) |
| 13 | 4, 12 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝐾) = ((𝐸‘𝐾) ∖ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖))) |
| 14 | 13 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → (𝐹‘𝐾) = ((𝐸‘𝐾) ∖ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖))) |
| 15 | 3, 14 | eleqtrd 2843 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → 𝑥 ∈ ((𝐸‘𝐾) ∖ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖))) |
| 16 | 15 | eldifbd 3964 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → ¬ 𝑥 ∈ ∪
𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖)) |
| 17 | | iundjiunlem.j |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ∈ 𝑍) |
| 18 | | iundjiunlem.z |
. . . . . . . . . . 11
⊢ 𝑍 =
(ℤ≥‘𝑁) |
| 19 | 17, 18 | eleqtrdi 2851 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽 ∈ (ℤ≥‘𝑁)) |
| 20 | 18, 4 | eluzelz2d 45424 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ ℤ) |
| 21 | | iundjiunlem.lt |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽 < 𝐾) |
| 22 | 19, 20, 21 | elfzod 45411 |
. . . . . . . . 9
⊢ (𝜑 → 𝐽 ∈ (𝑁..^𝐾)) |
| 23 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑖 = 𝐽 → (𝐸‘𝑖) = (𝐸‘𝐽)) |
| 24 | 23 | ssiun2s 5048 |
. . . . . . . . 9
⊢ (𝐽 ∈ (𝑁..^𝐾) → (𝐸‘𝐽) ⊆ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖)) |
| 25 | 22, 24 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐸‘𝐽) ⊆ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖)) |
| 26 | 25 | ssneld 3985 |
. . . . . . 7
⊢ (𝜑 → (¬ 𝑥 ∈ ∪
𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖) → ¬ 𝑥 ∈ (𝐸‘𝐽))) |
| 27 | 2, 16, 26 | sylc 65 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → ¬ 𝑥 ∈ (𝐸‘𝐽)) |
| 28 | | eldifi 4131 |
. . . . . 6
⊢ (𝑥 ∈ ((𝐸‘𝐽) ∖ ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖)) → 𝑥 ∈ (𝐸‘𝐽)) |
| 29 | 27, 28 | nsyl 140 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → ¬ 𝑥 ∈ ((𝐸‘𝐽) ∖ ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖))) |
| 30 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑛 = 𝐽 → (𝐸‘𝑛) = (𝐸‘𝐽)) |
| 31 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑛 = 𝐽 → (𝑁..^𝑛) = (𝑁..^𝐽)) |
| 32 | 31 | iuneq1d 5019 |
. . . . . . . . 9
⊢ (𝑛 = 𝐽 → ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖)) |
| 33 | 30, 32 | difeq12d 4127 |
. . . . . . . 8
⊢ (𝑛 = 𝐽 → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) = ((𝐸‘𝐽) ∖ ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖))) |
| 34 | | fvex 6919 |
. . . . . . . . 9
⊢ (𝐸‘𝐽) ∈ V |
| 35 | 34 | difexi 5330 |
. . . . . . . 8
⊢ ((𝐸‘𝐽) ∖ ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖)) ∈ V |
| 36 | 33, 9, 35 | fvmpt 7016 |
. . . . . . 7
⊢ (𝐽 ∈ 𝑍 → (𝐹‘𝐽) = ((𝐸‘𝐽) ∖ ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖))) |
| 37 | 17, 36 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝐽) = ((𝐸‘𝐽) ∖ ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖))) |
| 38 | 37 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → (𝐹‘𝐽) = ((𝐸‘𝐽) ∖ ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖))) |
| 39 | 29, 38 | neleqtrrd 2864 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → ¬ 𝑥 ∈ (𝐹‘𝐽)) |
| 40 | 39 | ralrimiva 3146 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ (𝐹‘𝐾) ¬ 𝑥 ∈ (𝐹‘𝐽)) |
| 41 | | disj 4450 |
. . 3
⊢ (((𝐹‘𝐾) ∩ (𝐹‘𝐽)) = ∅ ↔ ∀𝑥 ∈ (𝐹‘𝐾) ¬ 𝑥 ∈ (𝐹‘𝐽)) |
| 42 | 40, 41 | sylibr 234 |
. 2
⊢ (𝜑 → ((𝐹‘𝐾) ∩ (𝐹‘𝐽)) = ∅) |
| 43 | 1, 42 | eqtrid 2789 |
1
⊢ (𝜑 → ((𝐹‘𝐽) ∩ (𝐹‘𝐾)) = ∅) |