Step | Hyp | Ref
| Expression |
1 | | incom 4178 |
. . 3
⊢ ((𝐹‘𝐽) ∩ (𝐹‘𝐾)) = ((𝐹‘𝐾) ∩ (𝐹‘𝐽)) |
2 | 1 | a1i 11 |
. 2
⊢ (𝜑 → ((𝐹‘𝐽) ∩ (𝐹‘𝐾)) = ((𝐹‘𝐾) ∩ (𝐹‘𝐽))) |
3 | | simpl 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → 𝜑) |
4 | | simpr 487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → 𝑥 ∈ (𝐹‘𝐾)) |
5 | | iundjiunlem.k |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈ 𝑍) |
6 | | fveq2 6670 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝐾 → (𝐸‘𝑛) = (𝐸‘𝐾)) |
7 | | oveq2 7164 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝐾 → (𝑁..^𝑛) = (𝑁..^𝐾)) |
8 | 7 | iuneq1d 4946 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝐾 → ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖)) |
9 | 6, 8 | difeq12d 4100 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝐾 → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) = ((𝐸‘𝐾) ∖ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖))) |
10 | | iundjiunlem.f |
. . . . . . . . . . . 12
⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖))) |
11 | | fvex 6683 |
. . . . . . . . . . . . 13
⊢ (𝐸‘𝐾) ∈ V |
12 | | difexg 5231 |
. . . . . . . . . . . . 13
⊢ ((𝐸‘𝐾) ∈ V → ((𝐸‘𝐾) ∖ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖)) ∈ V) |
13 | 11, 12 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ((𝐸‘𝐾) ∖ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖)) ∈ V |
14 | 9, 10, 13 | fvmpt 6768 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ 𝑍 → (𝐹‘𝐾) = ((𝐸‘𝐾) ∖ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖))) |
15 | 5, 14 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝐾) = ((𝐸‘𝐾) ∖ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖))) |
16 | 3, 15 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → (𝐹‘𝐾) = ((𝐸‘𝐾) ∖ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖))) |
17 | 4, 16 | eleqtrd 2915 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → 𝑥 ∈ ((𝐸‘𝐾) ∖ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖))) |
18 | | eldifn 4104 |
. . . . . . . 8
⊢ (𝑥 ∈ ((𝐸‘𝐾) ∖ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖)) → ¬ 𝑥 ∈ ∪
𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖)) |
19 | 17, 18 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → ¬ 𝑥 ∈ ∪
𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖)) |
20 | | iundjiunlem.j |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐽 ∈ 𝑍) |
21 | | iundjiunlem.z |
. . . . . . . . . . . 12
⊢ 𝑍 =
(ℤ≥‘𝑁) |
22 | 20, 21 | eleqtrdi 2923 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ∈ (ℤ≥‘𝑁)) |
23 | 21 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑍 = (ℤ≥‘𝑁)) |
24 | 5, 23 | eleqtrd 2915 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑁)) |
25 | | eluzelz 12254 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈
(ℤ≥‘𝑁) → 𝐾 ∈ ℤ) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈ ℤ) |
27 | | iundjiunlem.lt |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 < 𝐾) |
28 | 22, 26, 27 | 3jca 1124 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐽 ∈ (ℤ≥‘𝑁) ∧ 𝐾 ∈ ℤ ∧ 𝐽 < 𝐾)) |
29 | | elfzo2 13042 |
. . . . . . . . . 10
⊢ (𝐽 ∈ (𝑁..^𝐾) ↔ (𝐽 ∈ (ℤ≥‘𝑁) ∧ 𝐾 ∈ ℤ ∧ 𝐽 < 𝐾)) |
30 | 28, 29 | sylibr 236 |
. . . . . . . . 9
⊢ (𝜑 → 𝐽 ∈ (𝑁..^𝐾)) |
31 | | fveq2 6670 |
. . . . . . . . . 10
⊢ (𝑖 = 𝐽 → (𝐸‘𝑖) = (𝐸‘𝐽)) |
32 | 31 | ssiun2s 4972 |
. . . . . . . . 9
⊢ (𝐽 ∈ (𝑁..^𝐾) → (𝐸‘𝐽) ⊆ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖)) |
33 | 30, 32 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐸‘𝐽) ⊆ ∪ 𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖)) |
34 | 33 | ssneld 3969 |
. . . . . . 7
⊢ (𝜑 → (¬ 𝑥 ∈ ∪
𝑖 ∈ (𝑁..^𝐾)(𝐸‘𝑖) → ¬ 𝑥 ∈ (𝐸‘𝐽))) |
35 | 3, 19, 34 | sylc 65 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → ¬ 𝑥 ∈ (𝐸‘𝐽)) |
36 | | eldifi 4103 |
. . . . . . 7
⊢ (𝑥 ∈ ((𝐸‘𝐽) ∖ ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖)) → 𝑥 ∈ (𝐸‘𝐽)) |
37 | 36 | con3i 157 |
. . . . . 6
⊢ (¬
𝑥 ∈ (𝐸‘𝐽) → ¬ 𝑥 ∈ ((𝐸‘𝐽) ∖ ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖))) |
38 | 35, 37 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → ¬ 𝑥 ∈ ((𝐸‘𝐽) ∖ ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖))) |
39 | | fveq2 6670 |
. . . . . . . . . 10
⊢ (𝑛 = 𝐽 → (𝐸‘𝑛) = (𝐸‘𝐽)) |
40 | | oveq2 7164 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝐽 → (𝑁..^𝑛) = (𝑁..^𝐽)) |
41 | 40 | iuneq1d 4946 |
. . . . . . . . . 10
⊢ (𝑛 = 𝐽 → ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖)) |
42 | 39, 41 | difeq12d 4100 |
. . . . . . . . 9
⊢ (𝑛 = 𝐽 → ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) = ((𝐸‘𝐽) ∖ ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖))) |
43 | | fvex 6683 |
. . . . . . . . . 10
⊢ (𝐸‘𝐽) ∈ V |
44 | | difexg 5231 |
. . . . . . . . . 10
⊢ ((𝐸‘𝐽) ∈ V → ((𝐸‘𝐽) ∖ ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖)) ∈ V) |
45 | 43, 44 | ax-mp 5 |
. . . . . . . . 9
⊢ ((𝐸‘𝐽) ∖ ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖)) ∈ V |
46 | 42, 10, 45 | fvmpt 6768 |
. . . . . . . 8
⊢ (𝐽 ∈ 𝑍 → (𝐹‘𝐽) = ((𝐸‘𝐽) ∖ ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖))) |
47 | 20, 46 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘𝐽) = ((𝐸‘𝐽) ∖ ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖))) |
48 | 47 | adantr 483 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → (𝐹‘𝐽) = ((𝐸‘𝐽) ∖ ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖))) |
49 | 48 | eqcomd 2827 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → ((𝐸‘𝐽) ∖ ∪ 𝑖 ∈ (𝑁..^𝐽)(𝐸‘𝑖)) = (𝐹‘𝐽)) |
50 | 38, 49 | neleqtrd 2934 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐹‘𝐾)) → ¬ 𝑥 ∈ (𝐹‘𝐽)) |
51 | 50 | ralrimiva 3182 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ (𝐹‘𝐾) ¬ 𝑥 ∈ (𝐹‘𝐽)) |
52 | | disj 4399 |
. . 3
⊢ (((𝐹‘𝐾) ∩ (𝐹‘𝐽)) = ∅ ↔ ∀𝑥 ∈ (𝐹‘𝐾) ¬ 𝑥 ∈ (𝐹‘𝐽)) |
53 | 51, 52 | sylibr 236 |
. 2
⊢ (𝜑 → ((𝐹‘𝐾) ∩ (𝐹‘𝐽)) = ∅) |
54 | 2, 53 | eqtrd 2856 |
1
⊢ (𝜑 → ((𝐹‘𝐽) ∩ (𝐹‘𝐾)) = ∅) |