Step | Hyp | Ref
| Expression |
1 | | incom 4135 |
. 2
⊢ ((𝐹‘𝐽) ∩ (𝐹‘𝐾)) = ((𝐹‘𝐾) ∩ (𝐹‘𝐽)) |
2 | | simpl 483 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → 𝜑) |
3 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → 𝑥 ∈ (𝐹‘𝐾)) |
4 | | iundjiunlem.k |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈ 𝑍) |
5 | | fveq2 6774 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝐾 → (𝐸‘𝑛) = (𝐸‘𝐾)) |
6 | | oveq2 7283 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝐾 → (𝑁..^𝑛) = (𝑁..^𝐾)) |
7 | 6 | iuneq1d 4951 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝐾 → ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖)) |
8 | 5, 7 | difeq12d 4058 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝐾 → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) = ((𝐸‘𝐾) ∖ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖))) |
9 | | iundjiunlem.f |
. . . . . . . . . . . 12
⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
10 | | fvex 6787 |
. . . . . . . . . . . . 13
⊢ (𝐸‘𝐾) ∈ V |
11 | 10 | difexi 5252 |
. . . . . . . . . . . 12
⊢ ((𝐸‘𝐾) ∖ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖)) ∈ V |
12 | 8, 9, 11 | fvmpt 6875 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ 𝑍 → (𝐹‘𝐾) = ((𝐸‘𝐾) ∖ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖))) |
13 | 4, 12 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝐾) = ((𝐸‘𝐾) ∖ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖))) |
14 | 13 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → (𝐹‘𝐾) = ((𝐸‘𝐾) ∖ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖))) |
15 | 3, 14 | eleqtrd 2841 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → 𝑥 ∈ ((𝐸‘𝐾) ∖ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖))) |
16 | 15 | eldifbd 3900 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → ¬ 𝑥 ∈ ∪
𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖)) |
17 | | iundjiunlem.j |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ∈ 𝑍) |
18 | | iundjiunlem.z |
. . . . . . . . . . 11
⊢ 𝑍 =
(ℤ≥‘𝑁) |
19 | 17, 18 | eleqtrdi 2849 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽 ∈ (ℤ≥‘𝑁)) |
20 | 18, 4 | eluzelz2d 42953 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ ℤ) |
21 | | iundjiunlem.lt |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽 < 𝐾) |
22 | 19, 20, 21 | elfzod 42940 |
. . . . . . . . 9
⊢ (𝜑 → 𝐽 ∈ (𝑁..^𝐾)) |
23 | | fveq2 6774 |
. . . . . . . . . 10
⊢ (𝑖 = 𝐽 → (𝐸‘𝑖) = (𝐸‘𝐽)) |
24 | 23 | ssiun2s 4978 |
. . . . . . . . 9
⊢ (𝐽 ∈ (𝑁..^𝐾) → (𝐸‘𝐽) ⊆ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖)) |
25 | 22, 24 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐸‘𝐽) ⊆ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖)) |
26 | 25 | ssneld 3923 |
. . . . . . 7
⊢ (𝜑 → (¬ 𝑥 ∈ ∪
𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖) → ¬ 𝑥 ∈ (𝐸‘𝐽))) |
27 | 2, 16, 26 | sylc 65 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → ¬ 𝑥 ∈ (𝐸‘𝐽)) |
28 | | eldifi 4061 |
. . . . . 6
⊢ (𝑥 ∈ ((𝐸‘𝐽) ∖ ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖)) → 𝑥 ∈ (𝐸‘𝐽)) |
29 | 27, 28 | nsyl 140 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → ¬ 𝑥 ∈ ((𝐸‘𝐽) ∖ ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖))) |
30 | | fveq2 6774 |
. . . . . . . . 9
⊢ (𝑛 = 𝐽 → (𝐸‘𝑛) = (𝐸‘𝐽)) |
31 | | oveq2 7283 |
. . . . . . . . . 10
⊢ (𝑛 = 𝐽 → (𝑁..^𝑛) = (𝑁..^𝐽)) |
32 | 31 | iuneq1d 4951 |
. . . . . . . . 9
⊢ (𝑛 = 𝐽 → ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖)) |
33 | 30, 32 | difeq12d 4058 |
. . . . . . . 8
⊢ (𝑛 = 𝐽 → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) = ((𝐸‘𝐽) ∖ ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖))) |
34 | | fvex 6787 |
. . . . . . . . 9
⊢ (𝐸‘𝐽) ∈ V |
35 | 34 | difexi 5252 |
. . . . . . . 8
⊢ ((𝐸‘𝐽) ∖ ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖)) ∈ V |
36 | 33, 9, 35 | fvmpt 6875 |
. . . . . . 7
⊢ (𝐽 ∈ 𝑍 → (𝐹‘𝐽) = ((𝐸‘𝐽) ∖ ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖))) |
37 | 17, 36 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝐽) = ((𝐸‘𝐽) ∖ ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖))) |
38 | 37 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → (𝐹‘𝐽) = ((𝐸‘𝐽) ∖ ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖))) |
39 | 29, 38 | neleqtrrd 2861 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → ¬ 𝑥 ∈ (𝐹‘𝐽)) |
40 | 39 | ralrimiva 3103 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ (𝐹‘𝐾) ¬ 𝑥 ∈ (𝐹‘𝐽)) |
41 | | disj 4381 |
. . 3
⊢ (((𝐹‘𝐾) ∩ (𝐹‘𝐽)) = ∅ ↔ ∀𝑥 ∈ (𝐹‘𝐾) ¬ 𝑥 ∈ (𝐹‘𝐽)) |
42 | 40, 41 | sylibr 233 |
. 2
⊢ (𝜑 → ((𝐹‘𝐾) ∩ (𝐹‘𝐽)) = ∅) |
43 | 1, 42 | eqtrid 2790 |
1
⊢ (𝜑 → ((𝐹‘𝐽) ∩ (𝐹‘𝐾)) = ∅) |