| Step | Hyp | Ref
| Expression |
| 1 | | heibor1.4 |
. . 3
⊢ (𝜑 → 𝐽 ∈ Comp) |
| 2 | | heibor1.3 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) |
| 3 | | metxmet 24344 |
. . . . . . . . . 10
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
| 4 | 2, 3 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) |
| 5 | | heibor.1 |
. . . . . . . . . 10
⊢ 𝐽 = (MetOpen‘𝐷) |
| 6 | 5 | mopntop 24450 |
. . . . . . . . 9
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top) |
| 7 | 4, 6 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ Top) |
| 8 | | imassrn 6089 |
. . . . . . . . 9
⊢ (𝐹 “ 𝑢) ⊆ ran 𝐹 |
| 9 | | heibor1.6 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:ℕ⟶𝑋) |
| 10 | 9 | frnd 6744 |
. . . . . . . . . 10
⊢ (𝜑 → ran 𝐹 ⊆ 𝑋) |
| 11 | 5 | mopnuni 24451 |
. . . . . . . . . . 11
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽) |
| 12 | 4, 11 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 = ∪ 𝐽) |
| 13 | 10, 12 | sseqtrd 4020 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝐹 ⊆ ∪ 𝐽) |
| 14 | 8, 13 | sstrid 3995 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 “ 𝑢) ⊆ ∪ 𝐽) |
| 15 | | eqid 2737 |
. . . . . . . . 9
⊢ ∪ 𝐽 =
∪ 𝐽 |
| 16 | 15 | clscld 23055 |
. . . . . . . 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 3160 |
. . . . 5
⊢ (𝜑 → (∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑘 ∈ (Clsd‘𝐽))) |
| 21 | 20 | abssdv 4068 |
. . . 4
⊢ (𝜑 → {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ⊆ (Clsd‘𝐽)) |
| 22 | | fvex 6919 |
. . . . 5
⊢
(Clsd‘𝐽)
∈ V |
| 23 | 22 | elpw2 5334 |
. . . 4
⊢ ({𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ∈ 𝒫 (Clsd‘𝐽) ↔ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ⊆ (Clsd‘𝐽)) |
| 24 | 21, 23 | sylibr 234 |
. . 3
⊢ (𝜑 → {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∈ 𝒫 (Clsd‘𝐽)) |
| 25 | | elin 3967 |
. . . . . . 7
⊢ (𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ∩ Fin) ↔ (𝑟 ∈ 𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∧ 𝑟 ∈ Fin)) |
| 26 | | velpw 4605 |
. . . . . . . . 9
⊢ (𝑟 ∈ 𝒫 {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ↔ 𝑟 ⊆ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))}) |
| 27 | | ssabral 4065 |
. . . . . . . . 9
⊢ (𝑟 ⊆ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ↔ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) |
| 28 | 26, 27 | bitri 275 |
. . . . . . . 8
⊢ (𝑟 ∈ 𝒫 {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ↔ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) |
| 29 | 28 | anbi1i 624 |
. . . . . . 7
⊢ ((𝑟 ∈ 𝒫 {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ∧ 𝑟 ∈ Fin) ↔ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin)) |
| 30 | 25, 29 | bitri 275 |
. . . . . 6
⊢ (𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ∩ Fin) ↔ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin)) |
| 31 | | raleq 3323 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = ∅ → (∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∀𝑘 ∈ ∅ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))) |
| 32 | 31 | anbi2d 630 |
. . . . . . . . . . . . 13
⊢ (𝑚 = ∅ → ((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) ↔ (𝜑 ∧ ∀𝑘 ∈ ∅ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))))) |
| 33 | | inteq 4949 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = ∅ → ∩ 𝑚 =
∩ ∅) |
| 34 | 33 | sseq2d 4016 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = ∅ → ((𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ (𝐹 “ 𝑘) ⊆ ∩
∅)) |
| 35 | 34 | rexbidv 3179 |
. . . . . . . . . . . . 13
⊢ (𝑚 = ∅ → (∃𝑘 ∈ ran
ℤ≥(𝐹
“ 𝑘) ⊆ ∩ 𝑚
↔ ∃𝑘 ∈ ran
ℤ≥(𝐹
“ 𝑘) ⊆ ∩ ∅)) |
| 36 | 32, 35 | imbi12d 344 |
. . . . . . . . . . . 12
⊢ (𝑚 = ∅ → (((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚) ↔ ((𝜑 ∧ ∀𝑘 ∈ ∅ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩
∅))) |
| 37 | | raleq 3323 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑦 → (∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∀𝑘 ∈ 𝑦 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))) |
| 38 | 37 | anbi2d 630 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑦 → ((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) ↔ (𝜑 ∧ ∀𝑘 ∈ 𝑦 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))))) |
| 39 | | inteq 4949 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑦 → ∩ 𝑚 = ∩
𝑦) |
| 40 | 39 | sseq2d 4016 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑦 → ((𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ (𝐹 “ 𝑘) ⊆ ∩ 𝑦)) |
| 41 | 40 | rexbidv 3179 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑦 → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ ∃𝑘 ∈ ran
ℤ≥(𝐹
“ 𝑘) ⊆ ∩ 𝑦)) |
| 42 | 38, 41 | imbi12d 344 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑦 → (((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚) ↔ ((𝜑 ∧ ∀𝑘 ∈ 𝑦 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦))) |
| 43 | | raleq 3323 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑦 ∪ {𝑛}) → (∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))) |
| 44 | 43 | anbi2d 630 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (𝑦 ∪ {𝑛}) → ((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) ↔ (𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))))) |
| 45 | | inteq 4949 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = (𝑦 ∪ {𝑛}) → ∩ 𝑚 = ∩
(𝑦 ∪ {𝑛})) |
| 46 | 45 | sseq2d 4016 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑦 ∪ {𝑛}) → ((𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ (𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛}))) |
| 47 | 46 | rexbidv 3179 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (𝑦 ∪ {𝑛}) → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ ∃𝑘 ∈ ran
ℤ≥(𝐹
“ 𝑘) ⊆ ∩ (𝑦
∪ {𝑛}))) |
| 48 | 44, 47 | imbi12d 344 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑦 ∪ {𝑛}) → (((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚) ↔ ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛})))) |
| 49 | | raleq 3323 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑟 → (∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))) |
| 50 | 49 | anbi2d 630 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑟 → ((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) ↔ (𝜑 ∧ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))))) |
| 51 | | inteq 4949 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑟 → ∩ 𝑚 = ∩
𝑟) |
| 52 | 51 | sseq2d 4016 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑟 → ((𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ (𝐹 “ 𝑘) ⊆ ∩ 𝑟)) |
| 53 | 52 | rexbidv 3179 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑟 → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ ∃𝑘 ∈ ran
ℤ≥(𝐹
“ 𝑘) ⊆ ∩ 𝑟)) |
| 54 | 50, 53 | imbi12d 344 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑟 → (((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚) ↔ ((𝜑 ∧ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑟))) |
| 55 | | uzf 12881 |
. . . . . . . . . . . . . . . 16
⊢
ℤ≥:ℤ⟶𝒫 ℤ |
| 56 | | ffn 6736 |
. . . . . . . . . . . . . . . 16
⊢
(ℤ≥:ℤ⟶𝒫 ℤ →
ℤ≥ Fn ℤ) |
| 57 | 55, 56 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
ℤ≥ Fn ℤ |
| 58 | | 0z 12624 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℤ |
| 59 | | fnfvelrn 7100 |
. . . . . . . . . . . . . . 15
⊢
((ℤ≥ Fn ℤ ∧ 0 ∈ ℤ) →
(ℤ≥‘0) ∈ ran
ℤ≥) |
| 60 | 57, 58, 59 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢
(ℤ≥‘0) ∈ ran
ℤ≥ |
| 61 | | ssv 4008 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 “
(ℤ≥‘0)) ⊆ V |
| 62 | | int0 4962 |
. . . . . . . . . . . . . . 15
⊢ ∩ ∅ = V |
| 63 | 61, 62 | sseqtrri 4033 |
. . . . . . . . . . . . . 14
⊢ (𝐹 “
(ℤ≥‘0)) ⊆ ∩
∅ |
| 64 | | imaeq2 6074 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 =
(ℤ≥‘0) → (𝐹 “ 𝑘) = (𝐹 “
(ℤ≥‘0))) |
| 65 | 64 | sseq1d 4015 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 =
(ℤ≥‘0) → ((𝐹 “ 𝑘) ⊆ ∩
∅ ↔ (𝐹 “
(ℤ≥‘0)) ⊆ ∩
∅)) |
| 66 | 65 | rspcev 3622 |
. . . . . . . . . . . . . 14
⊢
(((ℤ≥‘0) ∈ ran ℤ≥
∧ (𝐹 “
(ℤ≥‘0)) ⊆ ∩ ∅)
→ ∃𝑘 ∈ ran
ℤ≥(𝐹
“ 𝑘) ⊆ ∩ ∅) |
| 67 | 60, 63, 66 | mp2an 692 |
. . . . . . . . . . . . 13
⊢
∃𝑘 ∈ ran
ℤ≥(𝐹
“ 𝑘) ⊆ ∩ ∅ |
| 68 | 67 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ∀𝑘 ∈ ∅ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩
∅) |
| 69 | | ssun1 4178 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑦 ⊆ (𝑦 ∪ {𝑛}) |
| 70 | | ssralv 4052 |
. . . . . . . . . . . . . . . . 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 4179 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑛} ⊆ (𝑦 ∪ {𝑛}) |
| 75 | | ssralv 4052 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝑛} ⊆ (𝑦 ∪ {𝑛}) → (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → ∀𝑘 ∈ {𝑛}∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))) |
| 76 | 74, 75 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑘 ∈
(𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → ∀𝑘 ∈ {𝑛}∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) |
| 77 | | vex 3484 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑛 ∈ V |
| 78 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑛 → (𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ 𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))) |
| 79 | 78 | rexbidv 3179 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑛 → (∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∃𝑢 ∈ ran ℤ≥𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))) |
| 80 | 77, 79 | ralsn 4681 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑘 ∈
{𝑛}∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∃𝑢 ∈ ran ℤ≥𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) |
| 81 | 76, 80 | sylib 218 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑘 ∈
(𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → ∃𝑢 ∈ ran ℤ≥𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) |
| 82 | | uzin2 15383 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑢 ∈ ran
ℤ≥ ∧ 𝑘 ∈ ran ℤ≥) →
(𝑢 ∩ 𝑘) ∈ ran
ℤ≥) |
| 83 | 8, 10 | sstrid 3995 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝐹 “ 𝑢) ⊆ 𝑋) |
| 84 | 83, 12 | sseqtrd 4020 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝐹 “ 𝑢) ⊆ ∪ 𝐽) |
| 85 | 15 | sscls 23064 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐽 ∈ Top ∧ (𝐹 “ 𝑢) ⊆ ∪ 𝐽) → (𝐹 “ 𝑢) ⊆ ((cls‘𝐽)‘(𝐹 “ 𝑢))) |
| 86 | 7, 84, 85 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝐹 “ 𝑢) ⊆ ((cls‘𝐽)‘(𝐹 “ 𝑢))) |
| 87 | | sseq2 4010 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → ((𝐹 “ 𝑢) ⊆ 𝑛 ↔ (𝐹 “ 𝑢) ⊆ ((cls‘𝐽)‘(𝐹 “ 𝑢)))) |
| 88 | 86, 87 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → (𝐹 “ 𝑢) ⊆ 𝑛)) |
| 89 | | inss2 4238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑢 ∩ 𝑘) ⊆ 𝑘 |
| 90 | | inss1 4237 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑢 ∩ 𝑘) ⊆ 𝑢 |
| 91 | | imass2 6120 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑢 ∩ 𝑘) ⊆ 𝑘 → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (𝐹 “ 𝑘)) |
| 92 | | imass2 6120 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑢 ∩ 𝑘) ⊆ 𝑢 → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (𝐹 “ 𝑢)) |
| 93 | 91, 92 | anim12i 613 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑢 ∩ 𝑘) ⊆ 𝑘 ∧ (𝑢 ∩ 𝑘) ⊆ 𝑢) → ((𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (𝐹 “ 𝑘) ∧ (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (𝐹 “ 𝑢))) |
| 94 | | ssin 4239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (𝐹 “ 𝑘) ∧ (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (𝐹 “ 𝑢)) ↔ (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ((𝐹 “ 𝑘) ∩ (𝐹 “ 𝑢))) |
| 95 | 93, 94 | sylib 218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑢 ∩ 𝑘) ⊆ 𝑘 ∧ (𝑢 ∩ 𝑘) ⊆ 𝑢) → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ((𝐹 “ 𝑘) ∩ (𝐹 “ 𝑢))) |
| 96 | 89, 90, 95 | mp2an 692 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ((𝐹 “ 𝑘) ∩ (𝐹 “ 𝑢)) |
| 97 | | ss2in 4245 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐹 “ 𝑘) ⊆ ∩ 𝑦 ∧ (𝐹 “ 𝑢) ⊆ 𝑛) → ((𝐹 “ 𝑘) ∩ (𝐹 “ 𝑢)) ⊆ (∩
𝑦 ∩ 𝑛)) |
| 98 | 96, 97 | sstrid 3995 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐹 “ 𝑘) ⊆ ∩ 𝑦 ∧ (𝐹 “ 𝑢) ⊆ 𝑛) → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (∩
𝑦 ∩ 𝑛)) |
| 99 | 77 | intunsn 4987 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ∩ (𝑦
∪ {𝑛}) = (∩ 𝑦
∩ 𝑛) |
| 100 | 98, 99 | sseqtrrdi 4025 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐹 “ 𝑘) ⊆ ∩ 𝑦 ∧ (𝐹 “ 𝑢) ⊆ 𝑛) → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ∩
(𝑦 ∪ {𝑛})) |
| 101 | 100 | expcom 413 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹 “ 𝑢) ⊆ 𝑛 → ((𝐹 “ 𝑘) ⊆ ∩ 𝑦 → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ∩
(𝑦 ∪ {𝑛}))) |
| 102 | 88, 101 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → ((𝐹 “ 𝑘) ⊆ ∩ 𝑦 → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ∩
(𝑦 ∪ {𝑛})))) |
| 103 | 102 | impd 410 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ (𝐹 “ 𝑘) ⊆ ∩ 𝑦) → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ∩
(𝑦 ∪ {𝑛}))) |
| 104 | | imaeq2 6074 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑚 = (𝑢 ∩ 𝑘) → (𝐹 “ 𝑚) = (𝐹 “ (𝑢 ∩ 𝑘))) |
| 105 | 104 | sseq1d 4015 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑚 = (𝑢 ∩ 𝑘) → ((𝐹 “ 𝑚) ⊆ ∩ (𝑦 ∪ {𝑛}) ↔ (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ∩
(𝑦 ∪ {𝑛}))) |
| 106 | 105 | rspcev 3622 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑢 ∩ 𝑘) ∈ ran ℤ≥ ∧
(𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ∩
(𝑦 ∪ {𝑛})) → ∃𝑚 ∈ ran
ℤ≥(𝐹
“ 𝑚) ⊆ ∩ (𝑦
∪ {𝑛})) |
| 107 | 106 | expcom 413 |
. . . . . . . . . . . . . . . . . . . . . 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 3212 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (∃𝑢 ∈ ran
ℤ≥∃𝑘 ∈ ran ℤ≥(𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ (𝐹 “ 𝑘) ⊆ ∩ 𝑦) → ∃𝑚 ∈ ran
ℤ≥(𝐹
“ 𝑚) ⊆ ∩ (𝑦
∪ {𝑛}))) |
| 112 | | reeanv 3229 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑢 ∈ ran
ℤ≥∃𝑘 ∈ ran ℤ≥(𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ (𝐹 “ 𝑘) ⊆ ∩ 𝑦) ↔ (∃𝑢 ∈ ran
ℤ≥𝑛 =
((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦)) |
| 113 | | imaeq2 6074 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 = 𝑘 → (𝐹 “ 𝑚) = (𝐹 “ 𝑘)) |
| 114 | 113 | sseq1d 4015 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 = 𝑘 → ((𝐹 “ 𝑚) ⊆ ∩ (𝑦 ∪ {𝑛}) ↔ (𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛}))) |
| 115 | 114 | cbvrexvw 3238 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑚 ∈ ran
ℤ≥(𝐹
“ 𝑚) ⊆ ∩ (𝑦
∪ {𝑛}) ↔
∃𝑘 ∈ ran
ℤ≥(𝐹
“ 𝑘) ⊆ ∩ (𝑦
∪ {𝑛})) |
| 116 | 111, 112,
115 | 3imtr3g 295 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((∃𝑢 ∈ ran
ℤ≥𝑛 =
((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦) → ∃𝑘 ∈ ran
ℤ≥(𝐹
“ 𝑘) ⊆ ∩ (𝑦
∪ {𝑛}))) |
| 117 | 116 | expd 415 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (∃𝑢 ∈ ran ℤ≥𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦 → ∃𝑘 ∈ ran
ℤ≥(𝐹
“ 𝑘) ⊆ ∩ (𝑦
∪ {𝑛})))) |
| 118 | 81, 117 | syl5 34 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦 → ∃𝑘 ∈ ran
ℤ≥(𝐹
“ 𝑘) ⊆ ∩ (𝑦
∪ {𝑛})))) |
| 119 | 118 | imp 406 |
. . . . . . . . . . . . . 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 9204 |
. . . . . . . . . . 11
⊢ (𝑟 ∈ Fin → ((𝜑 ∧ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑟)) |
| 123 | 122 | com12 32 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → (𝑟 ∈ Fin → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑟)) |
| 124 | 123 | impr 454 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin)) → ∃𝑘 ∈ ran
ℤ≥(𝐹
“ 𝑘) ⊆ ∩ 𝑟) |
| 125 | 9 | ffnd 6737 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 Fn ℕ) |
| 126 | | inss1 4237 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∩ ℕ) ⊆ 𝑘 |
| 127 | | imass2 6120 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∩ ℕ) ⊆ 𝑘 → (𝐹 “ (𝑘 ∩ ℕ)) ⊆ (𝐹 “ 𝑘)) |
| 128 | 126, 127 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (𝐹 “ (𝑘 ∩ ℕ)) ⊆ (𝐹 “ 𝑘) |
| 129 | | nnuz 12921 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ℕ =
(ℤ≥‘1) |
| 130 | | 1z 12647 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
ℤ |
| 131 | | fnfvelrn 7100 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((ℤ≥ Fn ℤ ∧ 1 ∈ ℤ) →
(ℤ≥‘1) ∈ ran
ℤ≥) |
| 132 | 57, 130, 131 | mp2an 692 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(ℤ≥‘1) ∈ ran
ℤ≥ |
| 133 | 129, 132 | eqeltri 2837 |
. . . . . . . . . . . . . . . . . . 19
⊢ ℕ
∈ ran ℤ≥ |
| 134 | | uzin2 15383 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ran
ℤ≥ ∧ ℕ ∈ ran ℤ≥) →
(𝑘 ∩ ℕ) ∈
ran ℤ≥) |
| 135 | 133, 134 | mpan2 691 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ran
ℤ≥ → (𝑘 ∩ ℕ) ∈ ran
ℤ≥) |
| 136 | | uzn0 12895 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∩ ℕ) ∈ ran
ℤ≥ → (𝑘 ∩ ℕ) ≠
∅) |
| 137 | 135, 136 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ran
ℤ≥ → (𝑘 ∩ ℕ) ≠
∅) |
| 138 | | n0 4353 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∩ ℕ) ≠ ∅
↔ ∃𝑦 𝑦 ∈ (𝑘 ∩ ℕ)) |
| 139 | 137, 138 | sylib 218 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ran
ℤ≥ → ∃𝑦 𝑦 ∈ (𝑘 ∩ ℕ)) |
| 140 | | fnfun 6668 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 Fn ℕ → Fun 𝐹) |
| 141 | | inss2 4238 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∩ ℕ) ⊆
ℕ |
| 142 | | fndm 6671 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐹 Fn ℕ → dom 𝐹 = ℕ) |
| 143 | 141, 142 | sseqtrrid 4027 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 Fn ℕ → (𝑘 ∩ ℕ) ⊆ dom
𝐹) |
| 144 | | funfvima2 7251 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((Fun
𝐹 ∧ (𝑘 ∩ ℕ) ⊆ dom 𝐹) → (𝑦 ∈ (𝑘 ∩ ℕ) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑘 ∩ ℕ)))) |
| 145 | 140, 143,
144 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 Fn ℕ → (𝑦 ∈ (𝑘 ∩ ℕ) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑘 ∩ ℕ)))) |
| 146 | | ne0i 4341 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑦) ∈ (𝐹 “ (𝑘 ∩ ℕ)) → (𝐹 “ (𝑘 ∩ ℕ)) ≠
∅) |
| 147 | 145, 146 | syl6 35 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 Fn ℕ → (𝑦 ∈ (𝑘 ∩ ℕ) → (𝐹 “ (𝑘 ∩ ℕ)) ≠
∅)) |
| 148 | 147 | exlimdv 1933 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 Fn ℕ → (∃𝑦 𝑦 ∈ (𝑘 ∩ ℕ) → (𝐹 “ (𝑘 ∩ ℕ)) ≠
∅)) |
| 149 | 139, 148 | syl5 34 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 Fn ℕ → (𝑘 ∈ ran
ℤ≥ → (𝐹 “ (𝑘 ∩ ℕ)) ≠
∅)) |
| 150 | 149 | imp 406 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 Fn ℕ ∧ 𝑘 ∈ ran
ℤ≥) → (𝐹 “ (𝑘 ∩ ℕ)) ≠
∅) |
| 151 | | ssn0 4404 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 “ (𝑘 ∩ ℕ)) ⊆ (𝐹 “ 𝑘) ∧ (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅) → (𝐹 “ 𝑘) ≠ ∅) |
| 152 | 128, 150,
151 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ ((𝐹 Fn ℕ ∧ 𝑘 ∈ ran
ℤ≥) → (𝐹 “ 𝑘) ≠ ∅) |
| 153 | | ssn0 4404 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 “ 𝑘) ⊆ ∩ 𝑟 ∧ (𝐹 “ 𝑘) ≠ ∅) → ∩ 𝑟
≠ ∅) |
| 154 | 153 | expcom 413 |
. . . . . . . . . . . . 13
⊢ ((𝐹 “ 𝑘) ≠ ∅ → ((𝐹 “ 𝑘) ⊆ ∩ 𝑟 → ∩ 𝑟
≠ ∅)) |
| 155 | 152, 154 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐹 Fn ℕ ∧ 𝑘 ∈ ran
ℤ≥) → ((𝐹 “ 𝑘) ⊆ ∩ 𝑟 → ∩ 𝑟
≠ ∅)) |
| 156 | 155 | rexlimdva 3155 |
. . . . . . . . . . 11
⊢ (𝐹 Fn ℕ → (∃𝑘 ∈ ran
ℤ≥(𝐹
“ 𝑘) ⊆ ∩ 𝑟
→ ∩ 𝑟 ≠ ∅)) |
| 157 | 125, 156 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑟 → ∩ 𝑟
≠ ∅)) |
| 158 | 157 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin)) → (∃𝑘 ∈ ran
ℤ≥(𝐹
“ 𝑘) ⊆ ∩ 𝑟
→ ∩ 𝑟 ≠ ∅)) |
| 159 | 124, 158 | mpd 15 |
. . . . . . . 8
⊢ ((𝜑 ∧ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin)) → ∩ 𝑟
≠ ∅) |
| 160 | 159 | necomd 2996 |
. . . . . . 7
⊢ ((𝜑 ∧ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin)) → ∅ ≠ ∩ 𝑟) |
| 161 | 160 | neneqd 2945 |
. . . . . 6
⊢ ((𝜑 ∧ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin)) → ¬ ∅ = ∩ 𝑟) |
| 162 | 30, 161 | sylan2b 594 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∩ Fin)) → ¬ ∅ = ∩ 𝑟) |
| 163 | 162 | nrexdv 3149 |
. . . 4
⊢ (𝜑 → ¬ ∃𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ∩ Fin)∅ = ∩ 𝑟) |
| 164 | | 0ex 5307 |
. . . . 5
⊢ ∅
∈ V |
| 165 | | zex 12622 |
. . . . . . . 8
⊢ ℤ
∈ V |
| 166 | 165 | pwex 5380 |
. . . . . . 7
⊢ 𝒫
ℤ ∈ V |
| 167 | | frn 6743 |
. . . . . . . 8
⊢
(ℤ≥:ℤ⟶𝒫 ℤ → ran
ℤ≥ ⊆ 𝒫 ℤ) |
| 168 | 55, 167 | ax-mp 5 |
. . . . . . 7
⊢ ran
ℤ≥ ⊆ 𝒫 ℤ |
| 169 | 166, 168 | ssexi 5322 |
. . . . . 6
⊢ ran
ℤ≥ ∈ V |
| 170 | 169 | abrexex 7987 |
. . . . 5
⊢ {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ∈ V |
| 171 | | elfi 9453 |
. . . . 5
⊢ ((∅
∈ V ∧ {𝑘 ∣
∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ∈ V) → (∅ ∈
(fi‘{𝑘 ∣
∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))}) ↔ ∃𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∩ Fin)∅ = ∩ 𝑟)) |
| 172 | 164, 170,
171 | mp2an 692 |
. . . 4
⊢ (∅
∈ (fi‘{𝑘 ∣
∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))}) ↔ ∃𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∩ Fin)∅ = ∩ 𝑟) |
| 173 | 163, 172 | sylnibr 329 |
. . 3
⊢ (𝜑 → ¬ ∅ ∈
(fi‘{𝑘 ∣
∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))})) |
| 174 | | cmptop 23403 |
. . . . . 6
⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top) |
| 175 | | cmpfi 23416 |
. . . . . 6
⊢ (𝐽 ∈ Top → (𝐽 ∈ Comp ↔
∀𝑚 ∈ 𝒫
(Clsd‘𝐽)(¬
∅ ∈ (fi‘𝑚)
→ ∩ 𝑚 ≠ ∅))) |
| 176 | 174, 175 | syl 17 |
. . . . 5
⊢ (𝐽 ∈ Comp → (𝐽 ∈ Comp ↔
∀𝑚 ∈ 𝒫
(Clsd‘𝐽)(¬
∅ ∈ (fi‘𝑚)
→ ∩ 𝑚 ≠ ∅))) |
| 177 | 176 | ibi 267 |
. . . 4
⊢ (𝐽 ∈ Comp →
∀𝑚 ∈ 𝒫
(Clsd‘𝐽)(¬
∅ ∈ (fi‘𝑚)
→ ∩ 𝑚 ≠ ∅)) |
| 178 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → (fi‘𝑚) = (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))})) |
| 179 | 178 | eleq2d 2827 |
. . . . . . 7
⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → (∅ ∈ (fi‘𝑚) ↔ ∅ ∈
(fi‘{𝑘 ∣
∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))}))) |
| 180 | 179 | notbid 318 |
. . . . . 6
⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → (¬ ∅ ∈
(fi‘𝑚) ↔ ¬
∅ ∈ (fi‘{𝑘
∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))}))) |
| 181 | | inteq 4949 |
. . . . . . . 8
⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → ∩ 𝑚 = ∩
{𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))}) |
| 182 | 181 | neeq1d 3000 |
. . . . . . 7
⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → (∩
𝑚 ≠ ∅ ↔ ∩ {𝑘
∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ≠ ∅)) |
| 183 | | n0 4353 |
. . . . . . 7
⊢ (∩ {𝑘
∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ≠ ∅ ↔ ∃𝑦 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))}) |
| 184 | 182, 183 | bitrdi 287 |
. . . . . 6
⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → (∩
𝑚 ≠ ∅ ↔
∃𝑦 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))})) |
| 185 | 180, 184 | imbi12d 344 |
. . . . 5
⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → ((¬ ∅ ∈
(fi‘𝑚) → ∩ 𝑚
≠ ∅) ↔ (¬ ∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))}) → ∃𝑦 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))}))) |
| 186 | 185 | rspccv 3619 |
. . . 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 23238 |
. . 3
⊢ Rel
(⇝𝑡‘𝐽) |
| 190 | | r19.23v 3183 |
. . . . . 6
⊢
(∀𝑢 ∈
ran ℤ≥(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘) ↔ (∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘)) |
| 191 | 190 | albii 1819 |
. . . . 5
⊢
(∀𝑘∀𝑢 ∈ ran ℤ≥(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘) ↔ ∀𝑘(∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘)) |
| 192 | | fvex 6919 |
. . . . . . . 8
⊢
((cls‘𝐽)‘(𝐹 “ 𝑢)) ∈ V |
| 193 | | eleq2 2830 |
. . . . . . . 8
⊢ (𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → (𝑦 ∈ 𝑘 ↔ 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢)))) |
| 194 | 192, 193 | ceqsalv 3521 |
. . . . . . 7
⊢
(∀𝑘(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘) ↔ 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) |
| 195 | 194 | ralbii 3093 |
. . . . . 6
⊢
(∀𝑢 ∈
ran ℤ≥∀𝑘(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘) ↔ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) |
| 196 | | ralcom4 3286 |
. . . . . 6
⊢
(∀𝑢 ∈
ran ℤ≥∀𝑘(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘) ↔ ∀𝑘∀𝑢 ∈ ran ℤ≥(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘)) |
| 197 | 195, 196 | bitr3i 277 |
. . . . 5
⊢
(∀𝑢 ∈
ran ℤ≥𝑦
∈ ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∀𝑘∀𝑢 ∈ ran ℤ≥(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘)) |
| 198 | | vex 3484 |
. . . . . 6
⊢ 𝑦 ∈ V |
| 199 | 198 | elintab 4958 |
. . . . 5
⊢ (𝑦 ∈ ∩ {𝑘
∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ↔ ∀𝑘(∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘)) |
| 200 | 191, 197,
199 | 3bitr4i 303 |
. . . 4
⊢
(∀𝑢 ∈
ran ℤ≥𝑦
∈ ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))}) |
| 201 | | eqid 2737 |
. . . . . . . . . . 11
⊢
((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ ℕ)) |
| 202 | | imaeq2 6074 |
. . . . . . . . . . . . 13
⊢ (𝑢 = ℕ → (𝐹 “ 𝑢) = (𝐹 “ ℕ)) |
| 203 | 202 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ (𝑢 = ℕ →
((cls‘𝐽)‘(𝐹 “ 𝑢)) = ((cls‘𝐽)‘(𝐹 “ ℕ))) |
| 204 | 203 | rspceeqv 3645 |
. . . . . . . . . . 11
⊢ ((ℕ
∈ ran ℤ≥ ∧ ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ ℕ))) → ∃𝑢 ∈ ran
ℤ≥((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ 𝑢))) |
| 205 | 133, 201,
204 | mp2an 692 |
. . . . . . . . . 10
⊢
∃𝑢 ∈ ran
ℤ≥((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ 𝑢)) |
| 206 | | fvex 6919 |
. . . . . . . . . . 11
⊢
((cls‘𝐽)‘(𝐹 “ ℕ)) ∈ V |
| 207 | | eqeq1 2741 |
. . . . . . . . . . . 12
⊢ (𝑘 = ((cls‘𝐽)‘(𝐹 “ ℕ)) → (𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ 𝑢)))) |
| 208 | 207 | rexbidv 3179 |
. . . . . . . . . . 11
⊢ (𝑘 = ((cls‘𝐽)‘(𝐹 “ ℕ)) → (∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∃𝑢 ∈ ran
ℤ≥((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ 𝑢)))) |
| 209 | 206, 208 | elab 3679 |
. . . . . . . . . 10
⊢
(((cls‘𝐽)‘(𝐹 “ ℕ)) ∈ {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ↔ ∃𝑢 ∈ ran
ℤ≥((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ 𝑢))) |
| 210 | 205, 209 | mpbir 231 |
. . . . . . . . 9
⊢
((cls‘𝐽)‘(𝐹 “ ℕ)) ∈ {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} |
| 211 | | intss1 4963 |
. . . . . . . . 9
⊢
(((cls‘𝐽)‘(𝐹 “ ℕ)) ∈ {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} → ∩
{𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ⊆ ((cls‘𝐽)‘(𝐹 “ ℕ))) |
| 212 | 210, 211 | ax-mp 5 |
. . . . . . . 8
⊢ ∩ {𝑘
∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ⊆ ((cls‘𝐽)‘(𝐹 “ ℕ)) |
| 213 | | imassrn 6089 |
. . . . . . . . . . 11
⊢ (𝐹 “ ℕ) ⊆ ran
𝐹 |
| 214 | 213, 13 | sstrid 3995 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 “ ℕ) ⊆ ∪ 𝐽) |
| 215 | 15 | clsss3 23067 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ (𝐹 “ ℕ) ⊆ ∪ 𝐽)
→ ((cls‘𝐽)‘(𝐹 “ ℕ)) ⊆ ∪ 𝐽) |
| 216 | 7, 214, 215 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → ((cls‘𝐽)‘(𝐹 “ ℕ)) ⊆ ∪ 𝐽) |
| 217 | 216, 12 | sseqtrrd 4021 |
. . . . . . . 8
⊢ (𝜑 → ((cls‘𝐽)‘(𝐹 “ ℕ)) ⊆ 𝑋) |
| 218 | 212, 217 | sstrid 3995 |
. . . . . . 7
⊢ (𝜑 → ∩ {𝑘
∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))} ⊆ 𝑋) |
| 219 | 218 | sselda 3983 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))}) → 𝑦 ∈ 𝑋) |
| 220 | 200, 219 | sylan2b 594 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) → 𝑦 ∈ 𝑋) |
| 221 | | heibor1.5 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 ∈ (Cau‘𝐷)) |
| 222 | | 1zzd 12648 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 ∈
ℤ) |
| 223 | 129, 4, 222 | iscau3 25312 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧
∀𝑦 ∈
ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦)))) |
| 224 | 221, 223 | mpbid 232 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹 ∈ (𝑋 ↑pm ℂ) ∧
∀𝑦 ∈
ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦))) |
| 225 | 224 | simprd 495 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑦 ∈ ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦)) |
| 226 | | simp3 1139 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦) → ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦) |
| 227 | 226 | ralimi 3083 |
. . . . . . . . . . . 12
⊢
(∀𝑘 ∈
(ℤ≥‘𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦) → ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦) |
| 228 | 227 | reximi 3084 |
. . . . . . . . . . 11
⊢
(∃𝑚 ∈
ℕ ∀𝑘 ∈
(ℤ≥‘𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦) → ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦) |
| 229 | 228 | ralimi 3083 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦) → ∀𝑦 ∈ ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦) |
| 230 | 225, 229 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑦 ∈ ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦) |
| 231 | 230 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∀𝑦 ∈ ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦) |
| 232 | | rphalfcl 13062 |
. . . . . . . 8
⊢ (𝑟 ∈ ℝ+
→ (𝑟 / 2) ∈
ℝ+) |
| 233 | | breq2 5147 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑟 / 2) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦 ↔ ((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2))) |
| 234 | 233 | 2ralbidv 3221 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑟 / 2) → (∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦 ↔ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2))) |
| 235 | 234 | rexbidv 3179 |
. . . . . . . . 9
⊢ (𝑦 = (𝑟 / 2) → (∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦 ↔ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2))) |
| 236 | 235 | rspccva 3621 |
. . . . . . . 8
⊢
((∀𝑦 ∈
ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦 ∧ (𝑟 / 2) ∈ ℝ+) →
∃𝑚 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2)) |
| 237 | 231, 232,
236 | syl2an 596 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ 𝑟 ∈ ℝ+) →
∃𝑚 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2)) |
| 238 | 9 | ffund 6740 |
. . . . . . . . . . . 12
⊢ (𝜑 → Fun 𝐹) |
| 239 | 238 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → Fun
𝐹) |
| 240 | 7 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → 𝐽 ∈ Top) |
| 241 | | imassrn 6089 |
. . . . . . . . . . . . . 14
⊢ (𝐹 “
(ℤ≥‘𝑚)) ⊆ ran 𝐹 |
| 242 | 241, 13 | sstrid 3995 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹 “ (ℤ≥‘𝑚)) ⊆ ∪ 𝐽) |
| 243 | 242 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (𝐹 “
(ℤ≥‘𝑚)) ⊆ ∪ 𝐽) |
| 244 | | nnz 12634 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℤ) |
| 245 | | fnfvelrn 7100 |
. . . . . . . . . . . . . . 15
⊢
((ℤ≥ Fn ℤ ∧ 𝑚 ∈ ℤ) →
(ℤ≥‘𝑚) ∈ ran
ℤ≥) |
| 246 | 57, 244, 245 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ →
(ℤ≥‘𝑚) ∈ ran
ℤ≥) |
| 247 | 246 | ad2antll 729 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) →
(ℤ≥‘𝑚) ∈ ran
ℤ≥) |
| 248 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) →
∀𝑢 ∈ ran
ℤ≥𝑦
∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) |
| 249 | | imaeq2 6074 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 =
(ℤ≥‘𝑚) → (𝐹 “ 𝑢) = (𝐹 “ (ℤ≥‘𝑚))) |
| 250 | 249 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 =
(ℤ≥‘𝑚) → ((cls‘𝐽)‘(𝐹 “ 𝑢)) = ((cls‘𝐽)‘(𝐹 “ (ℤ≥‘𝑚)))) |
| 251 | 250 | eleq2d 2827 |
. . . . . . . . . . . . . 14
⊢ (𝑢 =
(ℤ≥‘𝑚) → (𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ (ℤ≥‘𝑚))))) |
| 252 | 251 | rspcv 3618 |
. . . . . . . . . . . . 13
⊢
((ℤ≥‘𝑚) ∈ ran ℤ≥ →
(∀𝑢 ∈ ran
ℤ≥𝑦
∈ ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ (ℤ≥‘𝑚))))) |
| 253 | 247, 248,
252 | sylc 65 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ (ℤ≥‘𝑚)))) |
| 254 | 4 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → 𝐷 ∈ (∞Met‘𝑋)) |
| 255 | 220 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → 𝑦 ∈ 𝑋) |
| 256 | 232 | ad2antrl 728 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (𝑟 / 2) ∈
ℝ+) |
| 257 | 256 | rpxrd 13078 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (𝑟 / 2) ∈
ℝ*) |
| 258 | 5 | blopn 24513 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ (𝑟 / 2) ∈ ℝ*) →
(𝑦(ball‘𝐷)(𝑟 / 2)) ∈ 𝐽) |
| 259 | 254, 255,
257, 258 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (𝑦(ball‘𝐷)(𝑟 / 2)) ∈ 𝐽) |
| 260 | | blcntr 24423 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ (𝑟 / 2) ∈ ℝ+) →
𝑦 ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) |
| 261 | 254, 255,
256, 260 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → 𝑦 ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) |
| 262 | 15 | clsndisj 23083 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ (𝐹 “
(ℤ≥‘𝑚)) ⊆ ∪ 𝐽 ∧ 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ (ℤ≥‘𝑚)))) ∧ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∈ 𝐽 ∧ 𝑦 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) → ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) ≠
∅) |
| 263 | 240, 243,
253, 259, 261, 262 | syl32anc 1380 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) ≠
∅) |
| 264 | | n0 4353 |
. . . . . . . . . . . 12
⊢ (((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) ≠ ∅ ↔
∃𝑛 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚)))) |
| 265 | | inss2 4238 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) ⊆ (𝐹 “ (ℤ≥‘𝑚)) |
| 266 | 265 | sseli 3979 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) → 𝑛 ∈ (𝐹 “ (ℤ≥‘𝑚))) |
| 267 | | fvelima 6974 |
. . . . . . . . . . . . . . . 16
⊢ ((Fun
𝐹 ∧ 𝑛 ∈ (𝐹 “ (ℤ≥‘𝑚))) → ∃𝑘 ∈
(ℤ≥‘𝑚)(𝐹‘𝑘) = 𝑛) |
| 268 | 266, 267 | sylan2 593 |
. . . . . . . . . . . . . . 15
⊢ ((Fun
𝐹 ∧ 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚)))) → ∃𝑘 ∈
(ℤ≥‘𝑚)(𝐹‘𝑘) = 𝑛) |
| 269 | | inss1 4237 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) ⊆ (𝑦(ball‘𝐷)(𝑟 / 2)) |
| 270 | 269 | sseli 3979 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) → 𝑛 ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) |
| 271 | 270 | adantl 481 |
. . . . . . . . . . . . . . . . 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 3170 |
. . . . . . . . . . . . . . 15
⊢ ((Fun
𝐹 ∧ 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚)))) → (∃𝑘 ∈
(ℤ≥‘𝑚)(𝐹‘𝑘) = 𝑛 → ∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) |
| 275 | 268, 274 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ ((Fun
𝐹 ∧ 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚)))) → ∃𝑘 ∈
(ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) |
| 276 | 275 | ex 412 |
. . . . . . . . . . . . 13
⊢ (Fun
𝐹 → (𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) → ∃𝑘 ∈
(ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) |
| 277 | 276 | exlimdv 1933 |
. . . . . . . . . . . 12
⊢ (Fun
𝐹 → (∃𝑛 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) → ∃𝑘 ∈
(ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) |
| 278 | 264, 277 | biimtrid 242 |
. . . . . . . . . . 11
⊢ (Fun
𝐹 → (((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) ≠ ∅ →
∃𝑘 ∈
(ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) |
| 279 | 239, 263,
278 | sylc 65 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) →
∃𝑘 ∈
(ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) |
| 280 | | r19.29 3114 |
. . . . . . . . . . 11
⊢
((∀𝑘 ∈
(ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ ∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ (ℤ≥‘𝑚)(∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) |
| 281 | | uznnssnn 12937 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ →
(ℤ≥‘𝑚) ⊆ ℕ) |
| 282 | 281 | ad2antll 729 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) →
(ℤ≥‘𝑚) ⊆ ℕ) |
| 283 | | simprlr 780 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) |
| 284 | 4 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝐷 ∈ (∞Met‘𝑋)) |
| 285 | | simplrl 777 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝑟 ∈ ℝ+) |
| 286 | 285, 232 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (𝑟 / 2) ∈
ℝ+) |
| 287 | 286 | rpxrd 13078 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (𝑟 / 2) ∈
ℝ*) |
| 288 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝑦 ∈ 𝑋) |
| 289 | 9 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝐹:ℕ⟶𝑋) |
| 290 | | eluznn 12960 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑚 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘𝑚)) → 𝑘 ∈ ℕ) |
| 291 | 290 | ad2ant2lr 748 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑟 ∈ ℝ+
∧ 𝑚 ∈ ℕ)
∧ (𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) → 𝑘 ∈ ℕ) |
| 292 | 291 | ad2ant2lr 748 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝑘 ∈ ℕ) |
| 293 | 289, 292 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (𝐹‘𝑘) ∈ 𝑋) |
| 294 | | elbl3 24402 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑟 / 2) ∈ ℝ*) ∧
(𝑦 ∈ 𝑋 ∧ (𝐹‘𝑘) ∈ 𝑋)) → ((𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) ↔ ((𝐹‘𝑘)𝐷𝑦) < (𝑟 / 2))) |
| 295 | 284, 287,
288, 293, 294 | syl22anc 839 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) ↔ ((𝐹‘𝑘)𝐷𝑦) < (𝑟 / 2))) |
| 296 | 283, 295 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((𝐹‘𝑘)𝐷𝑦) < (𝑟 / 2)) |
| 297 | 2 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝐷 ∈ (Met‘𝑋)) |
| 298 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝑛 ∈ (ℤ≥‘𝑘)) |
| 299 | | eluznn 12960 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑘 ∈ ℕ ∧ 𝑛 ∈
(ℤ≥‘𝑘)) → 𝑛 ∈ ℕ) |
| 300 | 292, 298,
299 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝑛 ∈ ℕ) |
| 301 | 289, 300 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (𝐹‘𝑛) ∈ 𝑋) |
| 302 | | metcl 24342 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑛) ∈ 𝑋) → ((𝐹‘𝑘)𝐷(𝐹‘𝑛)) ∈ ℝ) |
| 303 | 297, 293,
301, 302 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((𝐹‘𝑘)𝐷(𝐹‘𝑛)) ∈ ℝ) |
| 304 | | metcl 24342 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝐹‘𝑘)𝐷𝑦) ∈ ℝ) |
| 305 | 297, 293,
288, 304 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((𝐹‘𝑘)𝐷𝑦) ∈ ℝ) |
| 306 | 286 | rpred 13077 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (𝑟 / 2) ∈ ℝ) |
| 307 | | lt2add 11748 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝐹‘𝑘)𝐷(𝐹‘𝑛)) ∈ ℝ ∧ ((𝐹‘𝑘)𝐷𝑦) ∈ ℝ) ∧ ((𝑟 / 2) ∈ ℝ ∧ (𝑟 / 2) ∈ ℝ)) →
((((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ ((𝐹‘𝑘)𝐷𝑦) < (𝑟 / 2)) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < ((𝑟 / 2) + (𝑟 / 2)))) |
| 308 | 303, 305,
306, 306, 307 | syl22anc 839 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ ((𝐹‘𝑘)𝐷𝑦) < (𝑟 / 2)) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < ((𝑟 / 2) + (𝑟 / 2)))) |
| 309 | 296, 308 | mpan2d 694 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < ((𝑟 / 2) + (𝑟 / 2)))) |
| 310 | 285 | rpcnd 13079 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝑟 ∈ ℂ) |
| 311 | 310 | 2halvesd 12512 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((𝑟 / 2) + (𝑟 / 2)) = 𝑟) |
| 312 | 311 | breq2d 5155 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < ((𝑟 / 2) + (𝑟 / 2)) ↔ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < 𝑟)) |
| 313 | 309, 312 | sylibd 239 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < 𝑟)) |
| 314 | | mettri2 24351 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ ((𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑛) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹‘𝑛)𝐷𝑦) ≤ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦))) |
| 315 | 297, 293,
301, 288, 314 | syl13anc 1374 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((𝐹‘𝑛)𝐷𝑦) ≤ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦))) |
| 316 | | metcl 24342 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘𝑛) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝐹‘𝑛)𝐷𝑦) ∈ ℝ) |
| 317 | 297, 301,
288, 316 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((𝐹‘𝑛)𝐷𝑦) ∈ ℝ) |
| 318 | 303, 305 | readdcld 11290 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) ∈ ℝ) |
| 319 | 285 | rpred 13077 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝑟 ∈ ℝ) |
| 320 | | lelttr 11351 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐹‘𝑛)𝐷𝑦) ∈ ℝ ∧ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) ∈ ℝ ∧ 𝑟 ∈ ℝ) → ((((𝐹‘𝑛)𝐷𝑦) ≤ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) ∧ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < 𝑟) → ((𝐹‘𝑛)𝐷𝑦) < 𝑟)) |
| 321 | 317, 318,
319, 320 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((((𝐹‘𝑛)𝐷𝑦) ≤ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) ∧ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < 𝑟) → ((𝐹‘𝑛)𝐷𝑦) < 𝑟)) |
| 322 | 315, 321 | mpand 695 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < 𝑟 → ((𝐹‘𝑛)𝐷𝑦) < 𝑟)) |
| 323 | 313, 322 | syld 47 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ((𝐹‘𝑛)𝐷𝑦) < 𝑟)) |
| 324 | 323 | anassrs 467 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ (𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) ∧ 𝑛 ∈ (ℤ≥‘𝑘)) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ((𝐹‘𝑛)𝐷𝑦) < 𝑟)) |
| 325 | 324 | ralimdva 3167 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ (𝑘 ∈
(ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) → (∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)) |
| 326 | 325 | expr 456 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ 𝑘 ∈
(ℤ≥‘𝑚)) → ((𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) → (∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))) |
| 327 | 326 | com23 86 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ 𝑘 ∈
(ℤ≥‘𝑚)) → (∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ((𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) → ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))) |
| 328 | 327 | impd 410 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ 𝑘 ∈
(ℤ≥‘𝑚)) → ((∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)) |
| 329 | 328 | reximdva 3168 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) →
(∃𝑘 ∈
(ℤ≥‘𝑚)(∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)) |
| 330 | | ssrexv 4053 |
. . . . . . . . . . . . 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 694 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) →
(∀𝑘 ∈
(ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)) |
| 335 | 334 | anassrs 467 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ 𝑟 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) →
(∀𝑘 ∈
(ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)) |
| 336 | 335 | rexlimdva 3155 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ 𝑟 ∈ ℝ+) →
(∃𝑚 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)) |
| 337 | 237, 336 | mpd 15 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ 𝑟 ∈ ℝ+) →
∃𝑘 ∈ ℕ
∀𝑛 ∈
(ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟) |
| 338 | 337 | ralrimiva 3146 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∀𝑟 ∈ ℝ+ ∃𝑘 ∈ ℕ ∀𝑛 ∈
(ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟) |
| 339 | | eqidd 2738 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) = (𝐹‘𝑛)) |
| 340 | 5, 4, 129, 222, 339, 9 | lmmbrf 25296 |
. . . . . 6
⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑦 ↔ (𝑦 ∈ 𝑋 ∧ ∀𝑟 ∈ ℝ+ ∃𝑘 ∈ ℕ ∀𝑛 ∈
(ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))) |
| 341 | 340 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) → (𝐹(⇝𝑡‘𝐽)𝑦 ↔ (𝑦 ∈ 𝑋 ∧ ∀𝑟 ∈ ℝ+ ∃𝑘 ∈ ℕ ∀𝑛 ∈
(ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))) |
| 342 | 220, 338,
341 | mpbir2and 713 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) → 𝐹(⇝𝑡‘𝐽)𝑦) |
| 343 | 200, 342 | sylan2br 595 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))}) → 𝐹(⇝𝑡‘𝐽)𝑦) |
| 344 | | releldm 5955 |
. . 3
⊢ ((Rel
(⇝𝑡‘𝐽) ∧ 𝐹(⇝𝑡‘𝐽)𝑦) → 𝐹 ∈ dom
(⇝𝑡‘𝐽)) |
| 345 | 189, 343,
344 | sylancr 587 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran
ℤ≥𝑘 =
((cls‘𝐽)‘(𝐹 “ 𝑢))}) → 𝐹 ∈ dom
(⇝𝑡‘𝐽)) |
| 346 | 188, 345 | exlimddv 1935 |
1
⊢ (𝜑 → 𝐹 ∈ dom
(⇝𝑡‘𝐽)) |