Step | Hyp | Ref
| Expression |
1 | | incom 4139 |
. 2
⊢ ((𝐹‘𝐽) ∩ (𝐹‘𝐾)) = ((𝐹‘𝐾) ∩ (𝐹‘𝐽)) |
2 | | simpl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → 𝜑) |
3 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → 𝑥 ∈ (𝐹‘𝐾)) |
4 | | iundjiunlem.k |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈ 𝑍) |
5 | | fveq2 6768 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝐾 → (𝐸‘𝑛) = (𝐸‘𝐾)) |
6 | | oveq2 7276 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝐾 → (𝑁..^𝑛) = (𝑁..^𝐾)) |
7 | 6 | iuneq1d 4956 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝐾 → ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖)) |
8 | 5, 7 | difeq12d 4062 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝐾 → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) = ((𝐸‘𝐾) ∖ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖))) |
9 | | iundjiunlem.f |
. . . . . . . . . . . 12
⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
10 | | fvex 6781 |
. . . . . . . . . . . . 13
⊢ (𝐸‘𝐾) ∈ V |
11 | 10 | difexi 5255 |
. . . . . . . . . . . 12
⊢ ((𝐸‘𝐾) ∖ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖)) ∈ V |
12 | 8, 9, 11 | fvmpt 6869 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ 𝑍 → (𝐹‘𝐾) = ((𝐸‘𝐾) ∖ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖))) |
13 | 4, 12 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝐾) = ((𝐸‘𝐾) ∖ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖))) |
14 | 13 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → (𝐹‘𝐾) = ((𝐸‘𝐾) ∖ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖))) |
15 | 3, 14 | eleqtrd 2842 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → 𝑥 ∈ ((𝐸‘𝐾) ∖ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖))) |
16 | 15 | eldifbd 3904 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → ¬ 𝑥 ∈ ∪
𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖)) |
17 | | iundjiunlem.j |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ∈ 𝑍) |
18 | | iundjiunlem.z |
. . . . . . . . . . 11
⊢ 𝑍 =
(ℤ≥‘𝑁) |
19 | 17, 18 | eleqtrdi 2850 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽 ∈ (ℤ≥‘𝑁)) |
20 | 18, 4 | eluzelz2d 42907 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ ℤ) |
21 | | iundjiunlem.lt |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽 < 𝐾) |
22 | 19, 20, 21 | elfzod 42894 |
. . . . . . . . 9
⊢ (𝜑 → 𝐽 ∈ (𝑁..^𝐾)) |
23 | | fveq2 6768 |
. . . . . . . . . 10
⊢ (𝑖 = 𝐽 → (𝐸‘𝑖) = (𝐸‘𝐽)) |
24 | 23 | ssiun2s 4982 |
. . . . . . . . 9
⊢ (𝐽 ∈ (𝑁..^𝐾) → (𝐸‘𝐽) ⊆ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖)) |
25 | 22, 24 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐸‘𝐽) ⊆ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖)) |
26 | 25 | ssneld 3927 |
. . . . . . 7
⊢ (𝜑 → (¬ 𝑥 ∈ ∪
𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖) → ¬ 𝑥 ∈ (𝐸‘𝐽))) |
27 | 2, 16, 26 | sylc 65 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → ¬ 𝑥 ∈ (𝐸‘𝐽)) |
28 | | eldifi 4065 |
. . . . . 6
⊢ (𝑥 ∈ ((𝐸‘𝐽) ∖ ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖)) → 𝑥 ∈ (𝐸‘𝐽)) |
29 | 27, 28 | nsyl 140 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → ¬ 𝑥 ∈ ((𝐸‘𝐽) ∖ ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖))) |
30 | | fveq2 6768 |
. . . . . . . . 9
⊢ (𝑛 = 𝐽 → (𝐸‘𝑛) = (𝐸‘𝐽)) |
31 | | oveq2 7276 |
. . . . . . . . . 10
⊢ (𝑛 = 𝐽 → (𝑁..^𝑛) = (𝑁..^𝐽)) |
32 | 31 | iuneq1d 4956 |
. . . . . . . . 9
⊢ (𝑛 = 𝐽 → ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖)) |
33 | 30, 32 | difeq12d 4062 |
. . . . . . . 8
⊢ (𝑛 = 𝐽 → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) = ((𝐸‘𝐽) ∖ ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖))) |
34 | | fvex 6781 |
. . . . . . . . 9
⊢ (𝐸‘𝐽) ∈ V |
35 | 34 | difexi 5255 |
. . . . . . . 8
⊢ ((𝐸‘𝐽) ∖ ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖)) ∈ V |
36 | 33, 9, 35 | fvmpt 6869 |
. . . . . . 7
⊢ (𝐽 ∈ 𝑍 → (𝐹‘𝐽) = ((𝐸‘𝐽) ∖ ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖))) |
37 | 17, 36 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝐽) = ((𝐸‘𝐽) ∖ ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖))) |
38 | 37 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → (𝐹‘𝐽) = ((𝐸‘𝐽) ∖ ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖))) |
39 | 29, 38 | neleqtrrd 2862 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → ¬ 𝑥 ∈ (𝐹‘𝐽)) |
40 | 39 | ralrimiva 3109 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ (𝐹‘𝐾) ¬ 𝑥 ∈ (𝐹‘𝐽)) |
41 | | disj 4386 |
. . 3
⊢ (((𝐹‘𝐾) ∩ (𝐹‘𝐽)) = ∅ ↔ ∀𝑥 ∈ (𝐹‘𝐾) ¬ 𝑥 ∈ (𝐹‘𝐽)) |
42 | 40, 41 | sylibr 233 |
. 2
⊢ (𝜑 → ((𝐹‘𝐾) ∩ (𝐹‘𝐽)) = ∅) |
43 | 1, 42 | eqtrid 2791 |
1
⊢ (𝜑 → ((𝐹‘𝐽) ∩ (𝐹‘𝐾)) = ∅) |