Step | Hyp | Ref
| Expression |
1 | | heibor1.4 |
. . 3
⊢ (𝜑 → 𝐽 ∈ Comp) |
2 | | heibor1.3 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) |
3 | | metxmet 23485 |
. . . . . . . . . 10
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
4 | 2, 3 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) |
5 | | heibor.1 |
. . . . . . . . . 10
⊢ 𝐽 = (MetOpen‘𝐷) |
6 | 5 | mopntop 23591 |
. . . . . . . . 9
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top) |
7 | 4, 6 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ Top) |
8 | | imassrn 5979 |
. . . . . . . . 9
⊢ (𝐹 “ 𝑢) ⊆ ran 𝐹 |
9 | | heibor1.6 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:ℕ⟶𝑋) |
10 | 9 | frnd 6606 |
. . . . . . . . . 10
⊢ (𝜑 → ran 𝐹 ⊆ 𝑋) |
11 | 5 | mopnuni 23592 |
. . . . . . . . . . 11
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽) |
12 | 4, 11 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 = ∪ 𝐽) |
13 | 10, 12 | sseqtrd 3966 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝐹 ⊆ ∪ 𝐽) |
14 | 8, 13 | sstrid 3937 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 “ 𝑢) ⊆ ∪ 𝐽) |
15 | | eqid 2740 |
. . . . . . . . 9
⊢ ∪ 𝐽 =
∪ 𝐽 |
16 | 15 | clscld 22196 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ (𝐹 “ 𝑢) ⊆ ∪ 𝐽) → ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∈ (Clsd‘𝐽)) |
17 | 7, 14, 16 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∈ (Clsd‘𝐽)) |
18 | | eleq1a 2836 |
. . . . . . 7
⊢
(((cls‘𝐽)‘(𝐹 “ 𝑢)) ∈ (Clsd‘𝐽) → (𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑘 ∈ (Clsd‘𝐽))) |
19 | 17, 18 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑘 ∈ (Clsd‘𝐽))) |
20 | 19 | rexlimdvw 3221 |
. . . . 5
⊢ (𝜑 → (∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑘 ∈ (Clsd‘𝐽))) |
21 | 20 | abssdv 4007 |
. . . 4
⊢ (𝜑 → {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ⊆ (Clsd‘𝐽)) |
22 | | fvex 6784 |
. . . . 5
⊢
(Clsd‘𝐽)
∈ V |
23 | 22 | elpw2 5273 |
. . . 4
⊢ ({𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ∈ 𝒫 (Clsd‘𝐽) ↔ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ⊆ (Clsd‘𝐽)) |
24 | 21, 23 | sylibr 233 |
. . 3
⊢ (𝜑 → {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∈ 𝒫 (Clsd‘𝐽)) |
25 | | elin 3908 |
. . . . . . 7
⊢ (𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ∩ Fin) ↔ (𝑟 ∈ 𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∧ 𝑟 ∈ Fin)) |
26 | | velpw 4544 |
. . . . . . . . 9
⊢ (𝑟 ∈ 𝒫 {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ↔ 𝑟 ⊆ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))}) |
27 | | ssabral 4001 |
. . . . . . . . 9
⊢ (𝑟 ⊆ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ↔ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) |
28 | 26, 27 | bitri 274 |
. . . . . . . 8
⊢ (𝑟 ∈ 𝒫 {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ↔ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) |
29 | 28 | anbi1i 624 |
. . . . . . 7
⊢ ((𝑟 ∈ 𝒫 {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ∧ 𝑟 ∈ Fin) ↔ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin)) |
30 | 25, 29 | bitri 274 |
. . . . . 6
⊢ (𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ∩ Fin) ↔ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin)) |
31 | | raleq 3341 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = ∅ → (∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∀𝑘 ∈ ∅ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))) |
32 | 31 | anbi2d 629 |
. . . . . . . . . . . . 13
⊢ (𝑚 = ∅ → ((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) ↔ (𝜑 ∧ ∀𝑘 ∈ ∅ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))))) |
33 | | inteq 4888 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = ∅ → ∩ 𝑚 =
∩ ∅) |
34 | 33 | sseq2d 3958 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = ∅ → ((𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ (𝐹 “ 𝑘) ⊆ ∩
∅)) |
35 | 34 | rexbidv 3228 |
. . . . . . . . . . . . 13
⊢ (𝑚 = ∅ → (∃𝑘 ∈ ran
ℤ≥(𝐹
“ 𝑘) ⊆ ∩ 𝑚
↔ ∃𝑘 ∈ ran
ℤ≥(𝐹
“ 𝑘) ⊆ ∩ ∅)) |
36 | 32, 35 | imbi12d 345 |
. . . . . . . . . . . 12
⊢ (𝑚 = ∅ → (((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚) ↔ ((𝜑 ∧ ∀𝑘 ∈ ∅ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩
∅))) |
37 | | raleq 3341 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑦 → (∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∀𝑘 ∈ 𝑦 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))) |
38 | 37 | anbi2d 629 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑦 → ((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) ↔ (𝜑 ∧ ∀𝑘 ∈ 𝑦 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))))) |
39 | | inteq 4888 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑦 → ∩ 𝑚 = ∩
𝑦) |
40 | 39 | sseq2d 3958 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑦 → ((𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ (𝐹 “ 𝑘) ⊆ ∩ 𝑦)) |
41 | 40 | rexbidv 3228 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑦 → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ ∃𝑘 ∈ ran
ℤ≥(𝐹
“ 𝑘) ⊆ ∩ 𝑦)) |
42 | 38, 41 | imbi12d 345 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑦 → (((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚) ↔ ((𝜑 ∧ ∀𝑘 ∈ 𝑦 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦))) |
43 | | raleq 3341 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑦 ∪ {𝑛}) → (∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))) |
44 | 43 | anbi2d 629 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (𝑦 ∪ {𝑛}) → ((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) ↔ (𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))))) |
45 | | inteq 4888 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = (𝑦 ∪ {𝑛}) → ∩ 𝑚 = ∩
(𝑦 ∪ {𝑛})) |
46 | 45 | sseq2d 3958 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑦 ∪ {𝑛}) → ((𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ (𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛}))) |
47 | 46 | rexbidv 3228 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (𝑦 ∪ {𝑛}) → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ ∃𝑘 ∈ ran
ℤ≥(𝐹
“ 𝑘) ⊆ ∩ (𝑦
∪ {𝑛}))) |
48 | 44, 47 | imbi12d 345 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑦 ∪ {𝑛}) → (((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚) ↔ ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛})))) |
49 | | raleq 3341 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑟 → (∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))) |
50 | 49 | anbi2d 629 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑟 → ((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) ↔ (𝜑 ∧ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))))) |
51 | | inteq 4888 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑟 → ∩ 𝑚 = ∩
𝑟) |
52 | 51 | sseq2d 3958 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑟 → ((𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ (𝐹 “ 𝑘) ⊆ ∩ 𝑟)) |
53 | 52 | rexbidv 3228 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑟 → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ ∃𝑘 ∈ ran
ℤ≥(𝐹
“ 𝑘) ⊆ ∩ 𝑟)) |
54 | 50, 53 | imbi12d 345 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑟 → (((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚) ↔ ((𝜑 ∧ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑟))) |
55 | | uzf 12584 |
. . . . . . . . . . . . . . . 16
⊢
ℤ≥:ℤ⟶𝒫 ℤ |
56 | | ffn 6598 |
. . . . . . . . . . . . . . . 16
⊢
(ℤ≥:ℤ⟶𝒫 ℤ →
ℤ≥ Fn ℤ) |
57 | 55, 56 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
ℤ≥ Fn ℤ |
58 | | 0z 12330 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℤ |
59 | | fnfvelrn 6955 |
. . . . . . . . . . . . . . 15
⊢
((ℤ≥ Fn ℤ ∧ 0 ∈ ℤ) →
(ℤ≥‘0) ∈ ran
ℤ≥) |
60 | 57, 58, 59 | mp2an 689 |
. . . . . . . . . . . . . 14
⊢
(ℤ≥‘0) ∈ ran
ℤ≥ |
61 | | ssv 3950 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 “
(ℤ≥‘0)) ⊆ V |
62 | | int0 4899 |
. . . . . . . . . . . . . . 15
⊢ ∩ ∅ = V |
63 | 61, 62 | sseqtrri 3963 |
. . . . . . . . . . . . . 14
⊢ (𝐹 “
(ℤ≥‘0)) ⊆ ∩
∅ |
64 | | imaeq2 5964 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 =
(ℤ≥‘0) → (𝐹 “ 𝑘) = (𝐹 “
(ℤ≥‘0))) |
65 | 64 | sseq1d 3957 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 =
(ℤ≥‘0) → ((𝐹 “ 𝑘) ⊆ ∩
∅ ↔ (𝐹 “
(ℤ≥‘0)) ⊆ ∩
∅)) |
66 | 65 | rspcev 3561 |
. . . . . . . . . . . . . 14
⊢
(((ℤ≥‘0) ∈ ran ℤ≥
∧ (𝐹 “
(ℤ≥‘0)) ⊆ ∩ ∅)
→ ∃𝑘 ∈ ran
ℤ≥(𝐹
“ 𝑘) ⊆ ∩ ∅) |
67 | 60, 63, 66 | mp2an 689 |
. . . . . . . . . . . . 13
⊢
∃𝑘 ∈ ran
ℤ≥(𝐹
“ 𝑘) ⊆ ∩ ∅ |
68 | 67 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ∀𝑘 ∈ ∅ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩
∅) |
69 | | ssun1 4111 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑦 ⊆ (𝑦 ∪ {𝑛}) |
70 | | ssralv 3992 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ⊆ (𝑦 ∪ {𝑛}) → (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → ∀𝑘 ∈ 𝑦 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))) |
71 | 69, 70 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑘 ∈
(𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → ∀𝑘 ∈ 𝑦 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) |
72 | 71 | anim2i 617 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → (𝜑 ∧ ∀𝑘 ∈ 𝑦 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))) |
73 | 72 | imim1i 63 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝑦 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦) → ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦)) |
74 | | ssun2 4112 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑛} ⊆ (𝑦 ∪ {𝑛}) |
75 | | ssralv 3992 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝑛} ⊆ (𝑦 ∪ {𝑛}) → (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → ∀𝑘 ∈ {𝑛}∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))) |
76 | 74, 75 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑘 ∈
(𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → ∀𝑘 ∈ {𝑛}∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) |
77 | | vex 3435 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑛 ∈ V |
78 | | eqeq1 2744 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑛 → (𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ 𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))) |
79 | 78 | rexbidv 3228 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑛 → (∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∃𝑢 ∈ ran ℤ≥𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))) |
80 | 77, 79 | ralsn 4623 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑘 ∈
{𝑛}∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∃𝑢 ∈ ran ℤ≥𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) |
81 | 76, 80 | sylib 217 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑘 ∈
(𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → ∃𝑢 ∈ ran ℤ≥𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) |
82 | | uzin2 15054 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑢 ∈ ran
ℤ≥ ∧ 𝑘 ∈ ran ℤ≥) →
(𝑢 ∩ 𝑘) ∈ ran
ℤ≥) |
83 | 8, 10 | sstrid 3937 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝐹 “ 𝑢) ⊆ 𝑋) |
84 | 83, 12 | sseqtrd 3966 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝐹 “ 𝑢) ⊆ ∪ 𝐽) |
85 | 15 | sscls 22205 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐽 ∈ Top ∧ (𝐹 “ 𝑢) ⊆ ∪ 𝐽) → (𝐹 “ 𝑢) ⊆ ((cls‘𝐽)‘(𝐹 “ 𝑢))) |
86 | 7, 84, 85 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝐹 “ 𝑢) ⊆ ((cls‘𝐽)‘(𝐹 “ 𝑢))) |
87 | | sseq2 3952 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → ((𝐹 “ 𝑢) ⊆ 𝑛 ↔ (𝐹 “ 𝑢) ⊆ ((cls‘𝐽)‘(𝐹 “ 𝑢)))) |
88 | 86, 87 | syl5ibrcom 246 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → (𝐹 “ 𝑢) ⊆ 𝑛)) |
89 | | inss2 4169 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑢 ∩ 𝑘) ⊆ 𝑘 |
90 | | inss1 4168 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑢 ∩ 𝑘) ⊆ 𝑢 |
91 | | imass2 6009 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑢 ∩ 𝑘) ⊆ 𝑘 → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (𝐹 “ 𝑘)) |
92 | | imass2 6009 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑢 ∩ 𝑘) ⊆ 𝑢 → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (𝐹 “ 𝑢)) |
93 | 91, 92 | anim12i 613 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑢 ∩ 𝑘) ⊆ 𝑘 ∧ (𝑢 ∩ 𝑘) ⊆ 𝑢) → ((𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (𝐹 “ 𝑘) ∧ (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (𝐹 “ 𝑢))) |
94 | | ssin 4170 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (𝐹 “ 𝑘) ∧ (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (𝐹 “ 𝑢)) ↔ (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ((𝐹 “ 𝑘) ∩ (𝐹 “ 𝑢))) |
95 | 93, 94 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑢 ∩ 𝑘) ⊆ 𝑘 ∧ (𝑢 ∩ 𝑘) ⊆ 𝑢) → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ((𝐹 “ 𝑘) ∩ (𝐹 “ 𝑢))) |
96 | 89, 90, 95 | mp2an 689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ((𝐹 “ 𝑘) ∩ (𝐹 “ 𝑢)) |
97 | | ss2in 4176 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐹 “ 𝑘) ⊆ ∩ 𝑦 ∧ (𝐹 “ 𝑢) ⊆ 𝑛) → ((𝐹 “ 𝑘) ∩ (𝐹 “ 𝑢)) ⊆ (∩
𝑦 ∩ 𝑛)) |
98 | 96, 97 | sstrid 3937 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐹 “ 𝑘) ⊆ ∩ 𝑦 ∧ (𝐹 “ 𝑢) ⊆ 𝑛) → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (∩
𝑦 ∩ 𝑛)) |
99 | 77 | intunsn 4926 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ∩ (𝑦
∪ {𝑛}) = (∩ 𝑦
∩ 𝑛) |
100 | 98, 99 | sseqtrrdi 3977 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐹 “ 𝑘) ⊆ ∩ 𝑦 ∧ (𝐹 “ 𝑢) ⊆ 𝑛) → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ∩
(𝑦 ∪ {𝑛})) |
101 | 100 | expcom 414 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹 “ 𝑢) ⊆ 𝑛 → ((𝐹 “ 𝑘) ⊆ ∩ 𝑦 → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ∩
(𝑦 ∪ {𝑛}))) |
102 | 88, 101 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → ((𝐹 “ 𝑘) ⊆ ∩ 𝑦 → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ∩
(𝑦 ∪ {𝑛})))) |
103 | 102 | impd 411 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ (𝐹 “ 𝑘) ⊆ ∩ 𝑦) → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ∩
(𝑦 ∪ {𝑛}))) |
104 | | imaeq2 5964 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑚 = (𝑢 ∩ 𝑘) → (𝐹 “ 𝑚) = (𝐹 “ (𝑢 ∩ 𝑘))) |
105 | 104 | sseq1d 3957 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑚 = (𝑢 ∩ 𝑘) → ((𝐹 “ 𝑚) ⊆ ∩ (𝑦 ∪ {𝑛}) ↔ (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ∩
(𝑦 ∪ {𝑛}))) |
106 | 105 | rspcev 3561 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑢 ∩ 𝑘) ∈ ran ℤ≥ ∧
(𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ∩
(𝑦 ∪ {𝑛})) → ∃𝑚 ∈ ran
ℤ≥(𝐹
“ 𝑚) ⊆ ∩ (𝑦
∪ {𝑛})) |
107 | 106 | expcom 414 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ∩
(𝑦 ∪ {𝑛}) → ((𝑢 ∩ 𝑘) ∈ ran ℤ≥ →
∃𝑚 ∈ ran
ℤ≥(𝐹
“ 𝑚) ⊆ ∩ (𝑦
∪ {𝑛}))) |
108 | 103, 107 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ (𝐹 “ 𝑘) ⊆ ∩ 𝑦) → ((𝑢 ∩ 𝑘) ∈ ran ℤ≥ →
∃𝑚 ∈ ran
ℤ≥(𝐹
“ 𝑚) ⊆ ∩ (𝑦
∪ {𝑛})))) |
109 | 108 | com23 86 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑢 ∩ 𝑘) ∈ ran ℤ≥ →
((𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ (𝐹 “ 𝑘) ⊆ ∩ 𝑦) → ∃𝑚 ∈ ran
ℤ≥(𝐹
“ 𝑚) ⊆ ∩ (𝑦
∪ {𝑛})))) |
110 | 82, 109 | syl5 34 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑢 ∈ ran ℤ≥ ∧
𝑘 ∈ ran
ℤ≥) → ((𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ (𝐹 “ 𝑘) ⊆ ∩ 𝑦) → ∃𝑚 ∈ ran
ℤ≥(𝐹
“ 𝑚) ⊆ ∩ (𝑦
∪ {𝑛})))) |
111 | 110 | rexlimdvv 3224 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (∃𝑢 ∈ ran
ℤ≥∃𝑘 ∈ ran ℤ≥(𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ (𝐹 “ 𝑘) ⊆ ∩ 𝑦) → ∃𝑚 ∈ ran
ℤ≥(𝐹
“ 𝑚) ⊆ ∩ (𝑦
∪ {𝑛}))) |
112 | | reeanv 3295 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑢 ∈ ran
ℤ≥∃𝑘 ∈ ran ℤ≥(𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ (𝐹 “ 𝑘) ⊆ ∩ 𝑦) ↔ (∃𝑢 ∈ ran
ℤ≥𝑛 =
((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦)) |
113 | | imaeq2 5964 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 = 𝑘 → (𝐹 “ 𝑚) = (𝐹 “ 𝑘)) |
114 | 113 | sseq1d 3957 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 = 𝑘 → ((𝐹 “ 𝑚) ⊆ ∩ (𝑦 ∪ {𝑛}) ↔ (𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛}))) |
115 | 114 | cbvrexvw 3382 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑚 ∈ ran
ℤ≥(𝐹
“ 𝑚) ⊆ ∩ (𝑦
∪ {𝑛}) ↔
∃𝑘 ∈ ran
ℤ≥(𝐹
“ 𝑘) ⊆ ∩ (𝑦
∪ {𝑛})) |
116 | 111, 112,
115 | 3imtr3g 295 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((∃𝑢 ∈ ran
ℤ≥𝑛 =
((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦) → ∃𝑘 ∈ ran
ℤ≥(𝐹
“ 𝑘) ⊆ ∩ (𝑦
∪ {𝑛}))) |
117 | 116 | expd 416 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (∃𝑢 ∈ ran ℤ≥𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦 → ∃𝑘 ∈ ran
ℤ≥(𝐹
“ 𝑘) ⊆ ∩ (𝑦
∪ {𝑛})))) |
118 | 81, 117 | syl5 34 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦 → ∃𝑘 ∈ ran
ℤ≥(𝐹
“ 𝑘) ⊆ ∩ (𝑦
∪ {𝑛})))) |
119 | 118 | imp 407 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦 → ∃𝑘 ∈ ran
ℤ≥(𝐹
“ 𝑘) ⊆ ∩ (𝑦
∪ {𝑛}))) |
120 | 73, 119 | sylcom 30 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝑦 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦) → ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛}))) |
121 | 120 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ Fin → (((𝜑 ∧ ∀𝑘 ∈ 𝑦 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦) → ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛})))) |
122 | 36, 42, 48, 54, 68, 121 | findcard2 8929 |
. . . . . . . . . . 11
⊢ (𝑟 ∈ Fin → ((𝜑 ∧ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑟)) |
123 | 122 | com12 32 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → (𝑟 ∈ Fin → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑟)) |
124 | 123 | impr 455 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin)) → ∃𝑘 ∈ ran
ℤ≥(𝐹
“ 𝑘) ⊆ ∩ 𝑟) |
125 | 9 | ffnd 6599 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 Fn ℕ) |
126 | | inss1 4168 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∩ ℕ) ⊆ 𝑘 |
127 | | imass2 6009 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∩ ℕ) ⊆ 𝑘 → (𝐹 “ (𝑘 ∩ ℕ)) ⊆ (𝐹 “ 𝑘)) |
128 | 126, 127 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (𝐹 “ (𝑘 ∩ ℕ)) ⊆ (𝐹 “ 𝑘) |
129 | | nnuz 12620 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ℕ =
(ℤ≥‘1) |
130 | | 1z 12350 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
ℤ |
131 | | fnfvelrn 6955 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((ℤ≥ Fn ℤ ∧ 1 ∈ ℤ) →
(ℤ≥‘1) ∈ ran
ℤ≥) |
132 | 57, 130, 131 | mp2an 689 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(ℤ≥‘1) ∈ ran
ℤ≥ |
133 | 129, 132 | eqeltri 2837 |
. . . . . . . . . . . . . . . . . . 19
⊢ ℕ
∈ ran ℤ≥ |
134 | | uzin2 15054 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ran
ℤ≥ ∧ ℕ ∈ ran ℤ≥) →
(𝑘 ∩ ℕ) ∈
ran ℤ≥) |
135 | 133, 134 | mpan2 688 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ran
ℤ≥ → (𝑘 ∩ ℕ) ∈ ran
ℤ≥) |
136 | | uzn0 12598 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∩ ℕ) ∈ ran
ℤ≥ → (𝑘 ∩ ℕ) ≠
∅) |
137 | 135, 136 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ran
ℤ≥ → (𝑘 ∩ ℕ) ≠
∅) |
138 | | n0 4286 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∩ ℕ) ≠ ∅
↔ ∃𝑦 𝑦 ∈ (𝑘 ∩ ℕ)) |
139 | 137, 138 | sylib 217 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ran
ℤ≥ → ∃𝑦 𝑦 ∈ (𝑘 ∩ ℕ)) |
140 | | fnfun 6531 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 Fn ℕ → Fun 𝐹) |
141 | | inss2 4169 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∩ ℕ) ⊆
ℕ |
142 | | fndm 6534 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐹 Fn ℕ → dom 𝐹 = ℕ) |
143 | 141, 142 | sseqtrrid 3979 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 Fn ℕ → (𝑘 ∩ ℕ) ⊆ dom
𝐹) |
144 | | funfvima2 7104 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((Fun
𝐹 ∧ (𝑘 ∩ ℕ) ⊆ dom 𝐹) → (𝑦 ∈ (𝑘 ∩ ℕ) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑘 ∩ ℕ)))) |
145 | 140, 143,
144 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 Fn ℕ → (𝑦 ∈ (𝑘 ∩ ℕ) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑘 ∩ ℕ)))) |
146 | | ne0i 4274 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑦) ∈ (𝐹 “ (𝑘 ∩ ℕ)) → (𝐹 “ (𝑘 ∩ ℕ)) ≠
∅) |
147 | 145, 146 | syl6 35 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 Fn ℕ → (𝑦 ∈ (𝑘 ∩ ℕ) → (𝐹 “ (𝑘 ∩ ℕ)) ≠
∅)) |
148 | 147 | exlimdv 1940 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 Fn ℕ → (∃𝑦 𝑦 ∈ (𝑘 ∩ ℕ) → (𝐹 “ (𝑘 ∩ ℕ)) ≠
∅)) |
149 | 139, 148 | syl5 34 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 Fn ℕ → (𝑘 ∈ ran
ℤ≥ → (𝐹 “ (𝑘 ∩ ℕ)) ≠
∅)) |
150 | 149 | imp 407 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 Fn ℕ ∧ 𝑘 ∈ ran
ℤ≥) → (𝐹 “ (𝑘 ∩ ℕ)) ≠
∅) |
151 | | ssn0 4340 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 “ (𝑘 ∩ ℕ)) ⊆ (𝐹 “ 𝑘) ∧ (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅) → (𝐹 “ 𝑘) ≠ ∅) |
152 | 128, 150,
151 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ ((𝐹 Fn ℕ ∧ 𝑘 ∈ ran
ℤ≥) → (𝐹 “ 𝑘) ≠ ∅) |
153 | | ssn0 4340 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 “ 𝑘) ⊆ ∩ 𝑟 ∧ (𝐹 “ 𝑘) ≠ ∅) → ∩ 𝑟
≠ ∅) |
154 | 153 | expcom 414 |
. . . . . . . . . . . . 13
⊢ ((𝐹 “ 𝑘) ≠ ∅ → ((𝐹 “ 𝑘) ⊆ ∩ 𝑟 → ∩ 𝑟
≠ ∅)) |
155 | 152, 154 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐹 Fn ℕ ∧ 𝑘 ∈ ran
ℤ≥) → ((𝐹 “ 𝑘) ⊆ ∩ 𝑟 → ∩ 𝑟
≠ ∅)) |
156 | 155 | rexlimdva 3215 |
. . . . . . . . . . 11
⊢ (𝐹 Fn ℕ → (∃𝑘 ∈ ran
ℤ≥(𝐹
“ 𝑘) ⊆ ∩ 𝑟
→ ∩ 𝑟 ≠ ∅)) |
157 | 125, 156 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑟 → ∩ 𝑟
≠ ∅)) |
158 | 157 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin)) → (∃𝑘 ∈ ran
ℤ≥(𝐹
“ 𝑘) ⊆ ∩ 𝑟
→ ∩ 𝑟 ≠ ∅)) |
159 | 124, 158 | mpd 15 |
. . . . . . . 8
⊢ ((𝜑 ∧ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin)) → ∩ 𝑟
≠ ∅) |
160 | 159 | necomd 3001 |
. . . . . . 7
⊢ ((𝜑 ∧ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin)) → ∅ ≠ ∩ 𝑟) |
161 | 160 | neneqd 2950 |
. . . . . 6
⊢ ((𝜑 ∧ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin)) → ¬ ∅ = ∩ 𝑟) |
162 | 30, 161 | sylan2b 594 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∩ Fin)) → ¬ ∅ = ∩ 𝑟) |
163 | 162 | nrexdv 3200 |
. . . 4
⊢ (𝜑 → ¬ ∃𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ∩ Fin)∅ = ∩ 𝑟) |
164 | | 0ex 5235 |
. . . . 5
⊢ ∅
∈ V |
165 | | zex 12328 |
. . . . . . . 8
⊢ ℤ
∈ V |
166 | 165 | pwex 5307 |
. . . . . . 7
⊢ 𝒫
ℤ ∈ V |
167 | | frn 6605 |
. . . . . . . 8
⊢
(ℤ≥:ℤ⟶𝒫 ℤ → ran
ℤ≥ ⊆ 𝒫 ℤ) |
168 | 55, 167 | ax-mp 5 |
. . . . . . 7
⊢ ran
ℤ≥ ⊆ 𝒫 ℤ |
169 | 166, 168 | ssexi 5250 |
. . . . . 6
⊢ ran
ℤ≥ ∈ V |
170 | 169 | abrexex 7798 |
. . . . 5
⊢ {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ∈ V |
171 | | elfi 9150 |
. . . . 5
⊢ ((∅
∈ V ∧ {𝑘 ∣
∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ∈ V) → (∅ ∈
(fi‘{𝑘 ∣
∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))}) ↔ ∃𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∩ Fin)∅ = ∩ 𝑟)) |
172 | 164, 170,
171 | mp2an 689 |
. . . 4
⊢ (∅
∈ (fi‘{𝑘 ∣
∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))}) ↔ ∃𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∩ Fin)∅ = ∩ 𝑟) |
173 | 163, 172 | sylnibr 329 |
. . 3
⊢ (𝜑 → ¬ ∅ ∈
(fi‘{𝑘 ∣
∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))})) |
174 | | cmptop 22544 |
. . . . . 6
⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top) |
175 | | cmpfi 22557 |
. . . . . 6
⊢ (𝐽 ∈ Top → (𝐽 ∈ Comp ↔
∀𝑚 ∈ 𝒫
(Clsd‘𝐽)(¬
∅ ∈ (fi‘𝑚)
→ ∩ 𝑚 ≠ ∅))) |
176 | 174, 175 | syl 17 |
. . . . 5
⊢ (𝐽 ∈ Comp → (𝐽 ∈ Comp ↔
∀𝑚 ∈ 𝒫
(Clsd‘𝐽)(¬
∅ ∈ (fi‘𝑚)
→ ∩ 𝑚 ≠ ∅))) |
177 | 176 | ibi 266 |
. . . 4
⊢ (𝐽 ∈ Comp →
∀𝑚 ∈ 𝒫
(Clsd‘𝐽)(¬
∅ ∈ (fi‘𝑚)
→ ∩ 𝑚 ≠ ∅)) |
178 | | fveq2 6771 |
. . . . . . . 8
⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → (fi‘𝑚) = (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))})) |
179 | 178 | eleq2d 2826 |
. . . . . . 7
⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → (∅ ∈ (fi‘𝑚) ↔ ∅ ∈
(fi‘{𝑘 ∣
∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))}))) |
180 | 179 | notbid 318 |
. . . . . 6
⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → (¬ ∅ ∈
(fi‘𝑚) ↔ ¬
∅ ∈ (fi‘{𝑘
∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))}))) |
181 | | inteq 4888 |
. . . . . . . 8
⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → ∩ 𝑚 = ∩
{𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))}) |
182 | 181 | neeq1d 3005 |
. . . . . . 7
⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → (∩
𝑚 ≠ ∅ ↔ ∩ {𝑘
∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ≠ ∅)) |
183 | | n0 4286 |
. . . . . . 7
⊢ (∩ {𝑘
∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ≠ ∅ ↔ ∃𝑦 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))}) |
184 | 182, 183 | bitrdi 287 |
. . . . . 6
⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → (∩
𝑚 ≠ ∅ ↔
∃𝑦 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))})) |
185 | 180, 184 | imbi12d 345 |
. . . . 5
⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → ((¬ ∅ ∈
(fi‘𝑚) → ∩ 𝑚
≠ ∅) ↔ (¬ ∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))}) → ∃𝑦 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))}))) |
186 | 185 | rspccv 3558 |
. . . 4
⊢
(∀𝑚 ∈
𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑚) → ∩ 𝑚
≠ ∅) → ({𝑘
∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ∈ 𝒫 (Clsd‘𝐽) → (¬ ∅ ∈
(fi‘{𝑘 ∣
∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))}) → ∃𝑦 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))}))) |
187 | 177, 186 | syl 17 |
. . 3
⊢ (𝐽 ∈ Comp → ({𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ∈ 𝒫 (Clsd‘𝐽) → (¬ ∅ ∈
(fi‘{𝑘 ∣
∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))}) → ∃𝑦 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))}))) |
188 | 1, 24, 173, 187 | syl3c 66 |
. 2
⊢ (𝜑 → ∃𝑦 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))}) |
189 | | lmrel 22379 |
. . 3
⊢ Rel
(⇝𝑡‘𝐽) |
190 | | r19.23v 3210 |
. . . . . 6
⊢
(∀𝑢 ∈
ran ℤ≥(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘) ↔ (∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘)) |
191 | 190 | albii 1826 |
. . . . 5
⊢
(∀𝑘∀𝑢 ∈ ran ℤ≥(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘) ↔ ∀𝑘(∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘)) |
192 | | fvex 6784 |
. . . . . . . 8
⊢
((cls‘𝐽)‘(𝐹 “ 𝑢)) ∈ V |
193 | | eleq2 2829 |
. . . . . . . 8
⊢ (𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → (𝑦 ∈ 𝑘 ↔ 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢)))) |
194 | 192, 193 | ceqsalv 3466 |
. . . . . . 7
⊢
(∀𝑘(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘) ↔ 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) |
195 | 194 | ralbii 3093 |
. . . . . 6
⊢
(∀𝑢 ∈
ran ℤ≥∀𝑘(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘) ↔ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) |
196 | | ralcom4 3164 |
. . . . . 6
⊢
(∀𝑢 ∈
ran ℤ≥∀𝑘(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘) ↔ ∀𝑘∀𝑢 ∈ ran ℤ≥(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘)) |
197 | 195, 196 | bitr3i 276 |
. . . . 5
⊢
(∀𝑢 ∈
ran ℤ≥𝑦
∈ ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∀𝑘∀𝑢 ∈ ran ℤ≥(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘)) |
198 | | vex 3435 |
. . . . . 6
⊢ 𝑦 ∈ V |
199 | 198 | elintab 4896 |
. . . . 5
⊢ (𝑦 ∈ ∩ {𝑘
∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ↔ ∀𝑘(∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘)) |
200 | 191, 197,
199 | 3bitr4i 303 |
. . . 4
⊢
(∀𝑢 ∈
ran ℤ≥𝑦
∈ ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))}) |
201 | | eqid 2740 |
. . . . . . . . . . 11
⊢
((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ ℕ)) |
202 | | imaeq2 5964 |
. . . . . . . . . . . . 13
⊢ (𝑢 = ℕ → (𝐹 “ 𝑢) = (𝐹 “ ℕ)) |
203 | 202 | fveq2d 6775 |
. . . . . . . . . . . 12
⊢ (𝑢 = ℕ →
((cls‘𝐽)‘(𝐹 “ 𝑢)) = ((cls‘𝐽)‘(𝐹 “ ℕ))) |
204 | 203 | rspceeqv 3576 |
. . . . . . . . . . 11
⊢ ((ℕ
∈ ran ℤ≥ ∧ ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ ℕ))) → ∃𝑢 ∈ ran
ℤ≥((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ 𝑢))) |
205 | 133, 201,
204 | mp2an 689 |
. . . . . . . . . 10
⊢
∃𝑢 ∈ ran
ℤ≥((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ 𝑢)) |
206 | | fvex 6784 |
. . . . . . . . . . 11
⊢
((cls‘𝐽)‘(𝐹 “ ℕ)) ∈ V |
207 | | eqeq1 2744 |
. . . . . . . . . . . 12
⊢ (𝑘 = ((cls‘𝐽)‘(𝐹 “ ℕ)) → (𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ 𝑢)))) |
208 | 207 | rexbidv 3228 |
. . . . . . . . . . 11
⊢ (𝑘 = ((cls‘𝐽)‘(𝐹 “ ℕ)) → (∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∃𝑢 ∈ ran
ℤ≥((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ 𝑢)))) |
209 | 206, 208 | elab 3611 |
. . . . . . . . . 10
⊢
(((cls‘𝐽)‘(𝐹 “ ℕ)) ∈ {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ↔ ∃𝑢 ∈ ran
ℤ≥((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ 𝑢))) |
210 | 205, 209 | mpbir 230 |
. . . . . . . . 9
⊢
((cls‘𝐽)‘(𝐹 “ ℕ)) ∈ {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} |
211 | | intss1 4900 |
. . . . . . . . 9
⊢
(((cls‘𝐽)‘(𝐹 “ ℕ)) ∈ {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} → ∩
{𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ⊆ ((cls‘𝐽)‘(𝐹 “ ℕ))) |
212 | 210, 211 | ax-mp 5 |
. . . . . . . 8
⊢ ∩ {𝑘
∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ⊆ ((cls‘𝐽)‘(𝐹 “ ℕ)) |
213 | | imassrn 5979 |
. . . . . . . . . . 11
⊢ (𝐹 “ ℕ) ⊆ ran
𝐹 |
214 | 213, 13 | sstrid 3937 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 “ ℕ) ⊆ ∪ 𝐽) |
215 | 15 | clsss3 22208 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ (𝐹 “ ℕ) ⊆ ∪ 𝐽)
→ ((cls‘𝐽)‘(𝐹 “ ℕ)) ⊆ ∪ 𝐽) |
216 | 7, 214, 215 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → ((cls‘𝐽)‘(𝐹 “ ℕ)) ⊆ ∪ 𝐽) |
217 | 216, 12 | sseqtrrd 3967 |
. . . . . . . 8
⊢ (𝜑 → ((cls‘𝐽)‘(𝐹 “ ℕ)) ⊆ 𝑋) |
218 | 212, 217 | sstrid 3937 |
. . . . . . 7
⊢ (𝜑 → ∩ {𝑘
∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ⊆ 𝑋) |
219 | 218 | sselda 3926 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))}) → 𝑦 ∈ 𝑋) |
220 | 200, 219 | sylan2b 594 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) → 𝑦 ∈ 𝑋) |
221 | | heibor1.5 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 ∈ (Cau‘𝐷)) |
222 | | 1zzd 12351 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 ∈
ℤ) |
223 | 129, 4, 222 | iscau3 24440 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧
∀𝑦 ∈
ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦)))) |
224 | 221, 223 | mpbid 231 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹 ∈ (𝑋 ↑pm ℂ) ∧
∀𝑦 ∈
ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦))) |
225 | 224 | simprd 496 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑦 ∈ ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦)) |
226 | | simp3 1137 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦) → ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦) |
227 | 226 | ralimi 3089 |
. . . . . . . . . . . 12
⊢
(∀𝑘 ∈
(ℤ≥‘𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦) → ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦) |
228 | 227 | reximi 3177 |
. . . . . . . . . . 11
⊢
(∃𝑚 ∈
ℕ ∀𝑘 ∈
(ℤ≥‘𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦) → ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦) |
229 | 228 | ralimi 3089 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦) → ∀𝑦 ∈ ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦) |
230 | 225, 229 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑦 ∈ ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦) |
231 | 230 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∀𝑦 ∈ ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦) |
232 | | rphalfcl 12756 |
. . . . . . . 8
⊢ (𝑟 ∈ ℝ+
→ (𝑟 / 2) ∈
ℝ+) |
233 | | breq2 5083 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑟 / 2) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦 ↔ ((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2))) |
234 | 233 | 2ralbidv 3125 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑟 / 2) → (∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦 ↔ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2))) |
235 | 234 | rexbidv 3228 |
. . . . . . . . 9
⊢ (𝑦 = (𝑟 / 2) → (∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦 ↔ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2))) |
236 | 235 | rspccva 3560 |
. . . . . . . 8
⊢
((∀𝑦 ∈
ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦 ∧ (𝑟 / 2) ∈ ℝ+) →
∃𝑚 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2)) |
237 | 231, 232,
236 | syl2an 596 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ 𝑟 ∈ ℝ+) →
∃𝑚 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2)) |
238 | 9 | ffund 6602 |
. . . . . . . . . . . 12
⊢ (𝜑 → Fun 𝐹) |
239 | 238 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → Fun
𝐹) |
240 | 7 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → 𝐽 ∈ Top) |
241 | | imassrn 5979 |
. . . . . . . . . . . . . 14
⊢ (𝐹 “
(ℤ≥‘𝑚)) ⊆ ran 𝐹 |
242 | 241, 13 | sstrid 3937 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹 “ (ℤ≥‘𝑚)) ⊆ ∪ 𝐽) |
243 | 242 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (𝐹 “
(ℤ≥‘𝑚)) ⊆ ∪ 𝐽) |
244 | | nnz 12342 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℤ) |
245 | | fnfvelrn 6955 |
. . . . . . . . . . . . . . 15
⊢
((ℤ≥ Fn ℤ ∧ 𝑚 ∈ ℤ) →
(ℤ≥‘𝑚) ∈ ran
ℤ≥) |
246 | 57, 244, 245 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ →
(ℤ≥‘𝑚) ∈ ran
ℤ≥) |
247 | 246 | ad2antll 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) →
(ℤ≥‘𝑚) ∈ ran
ℤ≥) |
248 | | simplr 766 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) →
∀𝑢 ∈ ran
ℤ≥𝑦
∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) |
249 | | imaeq2 5964 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 =
(ℤ≥‘𝑚) → (𝐹 “ 𝑢) = (𝐹 “ (ℤ≥‘𝑚))) |
250 | 249 | fveq2d 6775 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 =
(ℤ≥‘𝑚) → ((cls‘𝐽)‘(𝐹 “ 𝑢)) = ((cls‘𝐽)‘(𝐹 “ (ℤ≥‘𝑚)))) |
251 | 250 | eleq2d 2826 |
. . . . . . . . . . . . . 14
⊢ (𝑢 =
(ℤ≥‘𝑚) → (𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ (ℤ≥‘𝑚))))) |
252 | 251 | rspcv 3556 |
. . . . . . . . . . . . 13
⊢
((ℤ≥‘𝑚) ∈ ran ℤ≥ →
(∀𝑢 ∈ ran
ℤ≥𝑦
∈ ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ (ℤ≥‘𝑚))))) |
253 | 247, 248,
252 | sylc 65 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ (ℤ≥‘𝑚)))) |
254 | 4 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → 𝐷 ∈ (∞Met‘𝑋)) |
255 | 220 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → 𝑦 ∈ 𝑋) |
256 | 232 | ad2antrl 725 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (𝑟 / 2) ∈
ℝ+) |
257 | 256 | rpxrd 12772 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (𝑟 / 2) ∈
ℝ*) |
258 | 5 | blopn 23654 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ (𝑟 / 2) ∈ ℝ*) →
(𝑦(ball‘𝐷)(𝑟 / 2)) ∈ 𝐽) |
259 | 254, 255,
257, 258 | syl3anc 1370 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (𝑦(ball‘𝐷)(𝑟 / 2)) ∈ 𝐽) |
260 | | blcntr 23564 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ (𝑟 / 2) ∈ ℝ+) →
𝑦 ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) |
261 | 254, 255,
256, 260 | syl3anc 1370 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → 𝑦 ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) |
262 | 15 | clsndisj 22224 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ (𝐹 “
(ℤ≥‘𝑚)) ⊆ ∪ 𝐽 ∧ 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ (ℤ≥‘𝑚)))) ∧ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∈ 𝐽 ∧ 𝑦 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) → ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) ≠
∅) |
263 | 240, 243,
253, 259, 261, 262 | syl32anc 1377 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) ≠
∅) |
264 | | n0 4286 |
. . . . . . . . . . . 12
⊢ (((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) ≠ ∅ ↔
∃𝑛 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚)))) |
265 | | inss2 4169 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) ⊆ (𝐹 “ (ℤ≥‘𝑚)) |
266 | 265 | sseli 3922 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) → 𝑛 ∈ (𝐹 “ (ℤ≥‘𝑚))) |
267 | | fvelima 6832 |
. . . . . . . . . . . . . . . 16
⊢ ((Fun
𝐹 ∧ 𝑛 ∈ (𝐹 “ (ℤ≥‘𝑚))) → ∃𝑘 ∈
(ℤ≥‘𝑚)(𝐹‘𝑘) = 𝑛) |
268 | 266, 267 | sylan2 593 |
. . . . . . . . . . . . . . 15
⊢ ((Fun
𝐹 ∧ 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚)))) → ∃𝑘 ∈
(ℤ≥‘𝑚)(𝐹‘𝑘) = 𝑛) |
269 | | inss1 4168 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) ⊆ (𝑦(ball‘𝐷)(𝑟 / 2)) |
270 | 269 | sseli 3922 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) → 𝑛 ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) |
271 | 270 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((Fun
𝐹 ∧ 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚)))) → 𝑛 ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) |
272 | | eleq1a 2836 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) → ((𝐹‘𝑘) = 𝑛 → (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) |
273 | 271, 272 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((Fun
𝐹 ∧ 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚)))) → ((𝐹‘𝑘) = 𝑛 → (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) |
274 | 273 | reximdv 3204 |
. . . . . . . . . . . . . . 15
⊢ ((Fun
𝐹 ∧ 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚)))) → (∃𝑘 ∈
(ℤ≥‘𝑚)(𝐹‘𝑘) = 𝑛 → ∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) |
275 | 268, 274 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ ((Fun
𝐹 ∧ 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚)))) → ∃𝑘 ∈
(ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) |
276 | 275 | ex 413 |
. . . . . . . . . . . . 13
⊢ (Fun
𝐹 → (𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) → ∃𝑘 ∈
(ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) |
277 | 276 | exlimdv 1940 |
. . . . . . . . . . . 12
⊢ (Fun
𝐹 → (∃𝑛 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) → ∃𝑘 ∈
(ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) |
278 | 264, 277 | syl5bi 241 |
. . . . . . . . . . 11
⊢ (Fun
𝐹 → (((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) ≠ ∅ →
∃𝑘 ∈
(ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) |
279 | 239, 263,
278 | sylc 65 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) →
∃𝑘 ∈
(ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) |
280 | | r19.29 3186 |
. . . . . . . . . . 11
⊢
((∀𝑘 ∈
(ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ ∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ (ℤ≥‘𝑚)(∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) |
281 | | uznnssnn 12634 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ →
(ℤ≥‘𝑚) ⊆ ℕ) |
282 | 281 | ad2antll 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) →
(ℤ≥‘𝑚) ⊆ ℕ) |
283 | | simprlr 777 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) |
284 | 4 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝐷 ∈ (∞Met‘𝑋)) |
285 | | simplrl 774 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝑟 ∈ ℝ+) |
286 | 285, 232 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (𝑟 / 2) ∈
ℝ+) |
287 | 286 | rpxrd 12772 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (𝑟 / 2) ∈
ℝ*) |
288 | | simpllr 773 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝑦 ∈ 𝑋) |
289 | 9 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝐹:ℕ⟶𝑋) |
290 | | eluznn 12657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑚 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘𝑚)) → 𝑘 ∈ ℕ) |
291 | 290 | ad2ant2lr 745 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑟 ∈ ℝ+
∧ 𝑚 ∈ ℕ)
∧ (𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) → 𝑘 ∈ ℕ) |
292 | 291 | ad2ant2lr 745 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝑘 ∈ ℕ) |
293 | 289, 292 | ffvelrnd 6959 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (𝐹‘𝑘) ∈ 𝑋) |
294 | | elbl3 23543 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑟 / 2) ∈ ℝ*) ∧
(𝑦 ∈ 𝑋 ∧ (𝐹‘𝑘) ∈ 𝑋)) → ((𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) ↔ ((𝐹‘𝑘)𝐷𝑦) < (𝑟 / 2))) |
295 | 284, 287,
288, 293, 294 | syl22anc 836 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) ↔ ((𝐹‘𝑘)𝐷𝑦) < (𝑟 / 2))) |
296 | 283, 295 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((𝐹‘𝑘)𝐷𝑦) < (𝑟 / 2)) |
297 | 2 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝐷 ∈ (Met‘𝑋)) |
298 | | simprr 770 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝑛 ∈ (ℤ≥‘𝑘)) |
299 | | eluznn 12657 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑘 ∈ ℕ ∧ 𝑛 ∈
(ℤ≥‘𝑘)) → 𝑛 ∈ ℕ) |
300 | 292, 298,
299 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝑛 ∈ ℕ) |
301 | 289, 300 | ffvelrnd 6959 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (𝐹‘𝑛) ∈ 𝑋) |
302 | | metcl 23483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑛) ∈ 𝑋) → ((𝐹‘𝑘)𝐷(𝐹‘𝑛)) ∈ ℝ) |
303 | 297, 293,
301, 302 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((𝐹‘𝑘)𝐷(𝐹‘𝑛)) ∈ ℝ) |
304 | | metcl 23483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝐹‘𝑘)𝐷𝑦) ∈ ℝ) |
305 | 297, 293,
288, 304 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((𝐹‘𝑘)𝐷𝑦) ∈ ℝ) |
306 | 286 | rpred 12771 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (𝑟 / 2) ∈ ℝ) |
307 | | lt2add 11460 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐹‘𝑘)𝐷(𝐹‘𝑛)) ∈ ℝ ∧ ((𝐹‘𝑘)𝐷𝑦) ∈ ℝ) ∧ ((𝑟 / 2) ∈ ℝ ∧ (𝑟 / 2) ∈ ℝ)) →
((((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ ((𝐹‘𝑘)𝐷𝑦) < (𝑟 / 2)) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < ((𝑟 / 2) + (𝑟 / 2)))) |
308 | 303, 305,
306, 306, 307 | syl22anc 836 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ ((𝐹‘𝑘)𝐷𝑦) < (𝑟 / 2)) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < ((𝑟 / 2) + (𝑟 / 2)))) |
309 | 296, 308 | mpan2d 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < ((𝑟 / 2) + (𝑟 / 2)))) |
310 | 285 | rpcnd 12773 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝑟 ∈ ℂ) |
311 | 310 | 2halvesd 12219 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((𝑟 / 2) + (𝑟 / 2)) = 𝑟) |
312 | 311 | breq2d 5091 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < ((𝑟 / 2) + (𝑟 / 2)) ↔ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < 𝑟)) |
313 | 309, 312 | sylibd 238 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < 𝑟)) |
314 | | mettri2 23492 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ ((𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑛) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹‘𝑛)𝐷𝑦) ≤ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦))) |
315 | 297, 293,
301, 288, 314 | syl13anc 1371 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((𝐹‘𝑛)𝐷𝑦) ≤ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦))) |
316 | | metcl 23483 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘𝑛) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝐹‘𝑛)𝐷𝑦) ∈ ℝ) |
317 | 297, 301,
288, 316 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((𝐹‘𝑛)𝐷𝑦) ∈ ℝ) |
318 | 303, 305 | readdcld 11005 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) ∈ ℝ) |
319 | 285 | rpred 12771 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝑟 ∈ ℝ) |
320 | | lelttr 11066 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹‘𝑛)𝐷𝑦) ∈ ℝ ∧ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) ∈ ℝ ∧ 𝑟 ∈ ℝ) → ((((𝐹‘𝑛)𝐷𝑦) ≤ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) ∧ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < 𝑟) → ((𝐹‘𝑛)𝐷𝑦) < 𝑟)) |
321 | 317, 318,
319, 320 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((((𝐹‘𝑛)𝐷𝑦) ≤ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) ∧ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < 𝑟) → ((𝐹‘𝑛)𝐷𝑦) < 𝑟)) |
322 | 315, 321 | mpand 692 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < 𝑟 → ((𝐹‘𝑛)𝐷𝑦) < 𝑟)) |
323 | 313, 322 | syld 47 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ((𝐹‘𝑛)𝐷𝑦) < 𝑟)) |
324 | 323 | anassrs 468 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ (𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) ∧ 𝑛 ∈ (ℤ≥‘𝑘)) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ((𝐹‘𝑛)𝐷𝑦) < 𝑟)) |
325 | 324 | ralimdva 3105 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ (𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) → (∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)) |
326 | 325 | expr 457 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ 𝑘 ∈
(ℤ≥‘𝑚)) → ((𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) → (∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))) |
327 | 326 | com23 86 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ 𝑘 ∈
(ℤ≥‘𝑚)) → (∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ((𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) → ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))) |
328 | 327 | impd 411 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ 𝑘 ∈
(ℤ≥‘𝑚)) → ((∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)) |
329 | 328 | reximdva 3205 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) →
(∃𝑘 ∈
(ℤ≥‘𝑚)(∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)) |
330 | | ssrexv 3993 |
. . . . . . . . . . . . 13
⊢
((ℤ≥‘𝑚) ⊆ ℕ → (∃𝑘 ∈
(ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟 → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)) |
331 | 282, 329,
330 | sylsyld 61 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) →
(∃𝑘 ∈
(ℤ≥‘𝑚)(∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)) |
332 | 220, 331 | syldanl 602 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) →
(∃𝑘 ∈
(ℤ≥‘𝑚)(∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)) |
333 | 280, 332 | syl5 34 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) →
((∀𝑘 ∈
(ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ ∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)) |
334 | 279, 333 | mpan2d 691 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) →
(∀𝑘 ∈
(ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)) |
335 | 334 | anassrs 468 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ 𝑟 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) →
(∀𝑘 ∈
(ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)) |
336 | 335 | rexlimdva 3215 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ 𝑟 ∈ ℝ+) →
(∃𝑚 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)) |
337 | 237, 336 | mpd 15 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ 𝑟 ∈ ℝ+) →
∃𝑘 ∈ ℕ
∀𝑛 ∈
(ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟) |
338 | 337 | ralrimiva 3110 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∀𝑟 ∈ ℝ+ ∃𝑘 ∈ ℕ ∀𝑛 ∈
(ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟) |
339 | | eqidd 2741 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) = (𝐹‘𝑛)) |
340 | 5, 4, 129, 222, 339, 9 | lmmbrf 24424 |
. . . . . 6
⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑦 ↔ (𝑦 ∈ 𝑋 ∧ ∀𝑟 ∈ ℝ+ ∃𝑘 ∈ ℕ ∀𝑛 ∈
(ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))) |
341 | 340 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) → (𝐹(⇝𝑡‘𝐽)𝑦 ↔ (𝑦 ∈ 𝑋 ∧ ∀𝑟 ∈ ℝ+ ∃𝑘 ∈ ℕ ∀𝑛 ∈
(ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))) |
342 | 220, 338,
341 | mpbir2and 710 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) → 𝐹(⇝𝑡‘𝐽)𝑦) |
343 | 200, 342 | sylan2br 595 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))}) → 𝐹(⇝𝑡‘𝐽)𝑦) |
344 | | releldm 5852 |
. . 3
⊢ ((Rel
(⇝𝑡‘𝐽) ∧ 𝐹(⇝𝑡‘𝐽)𝑦) → 𝐹 ∈ dom
(⇝𝑡‘𝐽)) |
345 | 189, 343,
344 | sylancr 587 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))}) → 𝐹 ∈ dom
(⇝𝑡‘𝐽)) |
346 | 188, 345 | exlimddv 1942 |
1
⊢ (𝜑 → 𝐹 ∈ dom
(⇝𝑡‘𝐽)) |