Mathbox for Jeff Madsen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  heibor1lem Structured version   Visualization version   GIF version

Theorem heibor1lem 32778
 Description: Lemma for heibor1 32779. A compact metric space is complete. This proof works by considering the collection cls(𝐹 “ (ℤ≥‘𝑛)) for each 𝑛 ∈ ℕ, which has the finite intersection property because any finite intersection of upper integer sets is another upper integer set, so any finite intersection of the image closures will contain (𝐹 “ (ℤ≥‘𝑚)) for some 𝑚. Thus, by compactness, the intersection contains a point 𝑦, which must then be the convergent point of 𝐹. (Contributed by Jeff Madsen, 17-Jan-2014.) (Revised by Mario Carneiro, 5-Jun-2014.)
Hypotheses
Ref Expression
heibor.1 𝐽 = (MetOpen‘𝐷)
heibor1.3 (𝜑𝐷 ∈ (Met‘𝑋))
heibor1.4 (𝜑𝐽 ∈ Comp)
heibor1.5 (𝜑𝐹 ∈ (Cau‘𝐷))
heibor1.6 (𝜑𝐹:ℕ⟶𝑋)
Assertion
Ref Expression
heibor1lem (𝜑𝐹 ∈ dom (⇝𝑡𝐽))

Proof of Theorem heibor1lem
Dummy variables 𝑛 𝑦 𝑘 𝑟 𝑢 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 heibor1.4 . . 3 (𝜑𝐽 ∈ Comp)
2 heibor1.3 . . . . . . . . . 10 (𝜑𝐷 ∈ (Met‘𝑋))
3 metxmet 21949 . . . . . . . . . 10 (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
42, 3syl 17 . . . . . . . . 9 (𝜑𝐷 ∈ (∞Met‘𝑋))
5 heibor.1 . . . . . . . . . 10 𝐽 = (MetOpen‘𝐷)
65mopntop 22055 . . . . . . . . 9 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
74, 6syl 17 . . . . . . . 8 (𝜑𝐽 ∈ Top)
8 imassrn 5396 . . . . . . . . 9 (𝐹𝑢) ⊆ ran 𝐹
9 heibor1.6 . . . . . . . . . . 11 (𝜑𝐹:ℕ⟶𝑋)
10 frn 5966 . . . . . . . . . . 11 (𝐹:ℕ⟶𝑋 → ran 𝐹𝑋)
119, 10syl 17 . . . . . . . . . 10 (𝜑 → ran 𝐹𝑋)
125mopnuni 22056 . . . . . . . . . . 11 (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = 𝐽)
134, 12syl 17 . . . . . . . . . 10 (𝜑𝑋 = 𝐽)
1411, 13sseqtrd 3604 . . . . . . . . 9 (𝜑 → ran 𝐹 𝐽)
158, 14syl5ss 3579 . . . . . . . 8 (𝜑 → (𝐹𝑢) ⊆ 𝐽)
16 eqid 2610 . . . . . . . . 9 𝐽 = 𝐽
1716clscld 20661 . . . . . . . 8 ((𝐽 ∈ Top ∧ (𝐹𝑢) ⊆ 𝐽) → ((cls‘𝐽)‘(𝐹𝑢)) ∈ (Clsd‘𝐽))
187, 15, 17syl2anc 691 . . . . . . 7 (𝜑 → ((cls‘𝐽)‘(𝐹𝑢)) ∈ (Clsd‘𝐽))
19 eleq1a 2683 . . . . . . 7 (((cls‘𝐽)‘(𝐹𝑢)) ∈ (Clsd‘𝐽) → (𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑘 ∈ (Clsd‘𝐽)))
2018, 19syl 17 . . . . . 6 (𝜑 → (𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑘 ∈ (Clsd‘𝐽)))
2120rexlimdvw 3016 . . . . 5 (𝜑 → (∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑘 ∈ (Clsd‘𝐽)))
2221abssdv 3639 . . . 4 (𝜑 → {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ⊆ (Clsd‘𝐽))
23 fvex 6113 . . . . 5 (Clsd‘𝐽) ∈ V
2423elpw2 4755 . . . 4 ({𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∈ 𝒫 (Clsd‘𝐽) ↔ {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ⊆ (Clsd‘𝐽))
2522, 24sylibr 223 . . 3 (𝜑 → {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∈ 𝒫 (Clsd‘𝐽))
26 elin 3758 . . . . . . 7 (𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∩ Fin) ↔ (𝑟 ∈ 𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∧ 𝑟 ∈ Fin))
27 selpw 4115 . . . . . . . . 9 (𝑟 ∈ 𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ↔ 𝑟 ⊆ {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))})
28 ssabral 3636 . . . . . . . . 9 (𝑟 ⊆ {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ↔ ∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)))
2927, 28bitri 263 . . . . . . . 8 (𝑟 ∈ 𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ↔ ∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)))
3029anbi1i 727 . . . . . . 7 ((𝑟 ∈ 𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∧ 𝑟 ∈ Fin) ↔ (∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ 𝑟 ∈ Fin))
3126, 30bitri 263 . . . . . 6 (𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∩ Fin) ↔ (∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ 𝑟 ∈ Fin))
32 raleq 3115 . . . . . . . . . . . . . 14 (𝑚 = ∅ → (∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ↔ ∀𝑘 ∈ ∅ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))))
3332anbi2d 736 . . . . . . . . . . . . 13 (𝑚 = ∅ → ((𝜑 ∧ ∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) ↔ (𝜑 ∧ ∀𝑘 ∈ ∅ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)))))
34 inteq 4413 . . . . . . . . . . . . . . 15 (𝑚 = ∅ → 𝑚 = ∅)
3534sseq2d 3596 . . . . . . . . . . . . . 14 (𝑚 = ∅ → ((𝐹𝑘) ⊆ 𝑚 ↔ (𝐹𝑘) ⊆ ∅))
3635rexbidv 3034 . . . . . . . . . . . . 13 (𝑚 = ∅ → (∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑚 ↔ ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ ∅))
3733, 36imbi12d 333 . . . . . . . . . . . 12 (𝑚 = ∅ → (((𝜑 ∧ ∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑚) ↔ ((𝜑 ∧ ∀𝑘 ∈ ∅ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ ∅)))
38 raleq 3115 . . . . . . . . . . . . . 14 (𝑚 = 𝑦 → (∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ↔ ∀𝑘𝑦𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))))
3938anbi2d 736 . . . . . . . . . . . . 13 (𝑚 = 𝑦 → ((𝜑 ∧ ∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) ↔ (𝜑 ∧ ∀𝑘𝑦𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)))))
40 inteq 4413 . . . . . . . . . . . . . . 15 (𝑚 = 𝑦 𝑚 = 𝑦)
4140sseq2d 3596 . . . . . . . . . . . . . 14 (𝑚 = 𝑦 → ((𝐹𝑘) ⊆ 𝑚 ↔ (𝐹𝑘) ⊆ 𝑦))
4241rexbidv 3034 . . . . . . . . . . . . 13 (𝑚 = 𝑦 → (∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑚 ↔ ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑦))
4339, 42imbi12d 333 . . . . . . . . . . . 12 (𝑚 = 𝑦 → (((𝜑 ∧ ∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑚) ↔ ((𝜑 ∧ ∀𝑘𝑦𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑦)))
44 raleq 3115 . . . . . . . . . . . . . 14 (𝑚 = (𝑦 ∪ {𝑛}) → (∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ↔ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))))
4544anbi2d 736 . . . . . . . . . . . . 13 (𝑚 = (𝑦 ∪ {𝑛}) → ((𝜑 ∧ ∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) ↔ (𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)))))
46 inteq 4413 . . . . . . . . . . . . . . 15 (𝑚 = (𝑦 ∪ {𝑛}) → 𝑚 = (𝑦 ∪ {𝑛}))
4746sseq2d 3596 . . . . . . . . . . . . . 14 (𝑚 = (𝑦 ∪ {𝑛}) → ((𝐹𝑘) ⊆ 𝑚 ↔ (𝐹𝑘) ⊆ (𝑦 ∪ {𝑛})))
4847rexbidv 3034 . . . . . . . . . . . . 13 (𝑚 = (𝑦 ∪ {𝑛}) → (∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑚 ↔ ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ (𝑦 ∪ {𝑛})))
4945, 48imbi12d 333 . . . . . . . . . . . 12 (𝑚 = (𝑦 ∪ {𝑛}) → (((𝜑 ∧ ∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑚) ↔ ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ (𝑦 ∪ {𝑛}))))
50 raleq 3115 . . . . . . . . . . . . . 14 (𝑚 = 𝑟 → (∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ↔ ∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))))
5150anbi2d 736 . . . . . . . . . . . . 13 (𝑚 = 𝑟 → ((𝜑 ∧ ∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) ↔ (𝜑 ∧ ∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)))))
52 inteq 4413 . . . . . . . . . . . . . . 15 (𝑚 = 𝑟 𝑚 = 𝑟)
5352sseq2d 3596 . . . . . . . . . . . . . 14 (𝑚 = 𝑟 → ((𝐹𝑘) ⊆ 𝑚 ↔ (𝐹𝑘) ⊆ 𝑟))
5453rexbidv 3034 . . . . . . . . . . . . 13 (𝑚 = 𝑟 → (∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑚 ↔ ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑟))
5551, 54imbi12d 333 . . . . . . . . . . . 12 (𝑚 = 𝑟 → (((𝜑 ∧ ∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑚) ↔ ((𝜑 ∧ ∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑟)))
56 uzf 11566 . . . . . . . . . . . . . . . 16 :ℤ⟶𝒫 ℤ
57 ffn 5958 . . . . . . . . . . . . . . . 16 (ℤ:ℤ⟶𝒫 ℤ → ℤ Fn ℤ)
5856, 57ax-mp 5 . . . . . . . . . . . . . . 15 Fn ℤ
59 0z 11265 . . . . . . . . . . . . . . 15 0 ∈ ℤ
60 fnfvelrn 6264 . . . . . . . . . . . . . . 15 ((ℤ Fn ℤ ∧ 0 ∈ ℤ) → (ℤ‘0) ∈ ran ℤ)
6158, 59, 60mp2an 704 . . . . . . . . . . . . . 14 (ℤ‘0) ∈ ran ℤ
62 ssv 3588 . . . . . . . . . . . . . . 15 (𝐹 “ (ℤ‘0)) ⊆ V
63 int0 4425 . . . . . . . . . . . . . . 15 ∅ = V
6462, 63sseqtr4i 3601 . . . . . . . . . . . . . 14 (𝐹 “ (ℤ‘0)) ⊆
65 imaeq2 5381 . . . . . . . . . . . . . . . 16 (𝑘 = (ℤ‘0) → (𝐹𝑘) = (𝐹 “ (ℤ‘0)))
6665sseq1d 3595 . . . . . . . . . . . . . . 15 (𝑘 = (ℤ‘0) → ((𝐹𝑘) ⊆ ∅ ↔ (𝐹 “ (ℤ‘0)) ⊆ ∅))
6766rspcev 3282 . . . . . . . . . . . . . 14 (((ℤ‘0) ∈ ran ℤ ∧ (𝐹 “ (ℤ‘0)) ⊆ ∅) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ ∅)
6861, 64, 67mp2an 704 . . . . . . . . . . . . 13 𝑘 ∈ ran ℤ(𝐹𝑘) ⊆
6968a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ ∀𝑘 ∈ ∅ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ ∅)
70 ssun1 3738 . . . . . . . . . . . . . . . . 17 𝑦 ⊆ (𝑦 ∪ {𝑛})
71 ssralv 3629 . . . . . . . . . . . . . . . . 17 (𝑦 ⊆ (𝑦 ∪ {𝑛}) → (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → ∀𝑘𝑦𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))))
7270, 71ax-mp 5 . . . . . . . . . . . . . . . 16 (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → ∀𝑘𝑦𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)))
7372anim2i 591 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → (𝜑 ∧ ∀𝑘𝑦𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))))
7473imim1i 61 . . . . . . . . . . . . . 14 (((𝜑 ∧ ∀𝑘𝑦𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑦) → ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑦))
75 ssun2 3739 . . . . . . . . . . . . . . . . . 18 {𝑛} ⊆ (𝑦 ∪ {𝑛})
76 ssralv 3629 . . . . . . . . . . . . . . . . . 18 ({𝑛} ⊆ (𝑦 ∪ {𝑛}) → (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → ∀𝑘 ∈ {𝑛}∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))))
7775, 76ax-mp 5 . . . . . . . . . . . . . . . . 17 (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → ∀𝑘 ∈ {𝑛}∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)))
78 vex 3176 . . . . . . . . . . . . . . . . . 18 𝑛 ∈ V
79 eqeq1 2614 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑛 → (𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ↔ 𝑛 = ((cls‘𝐽)‘(𝐹𝑢))))
8079rexbidv 3034 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑛 → (∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ↔ ∃𝑢 ∈ ran ℤ𝑛 = ((cls‘𝐽)‘(𝐹𝑢))))
8178, 80ralsn 4169 . . . . . . . . . . . . . . . . 17 (∀𝑘 ∈ {𝑛}∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ↔ ∃𝑢 ∈ ran ℤ𝑛 = ((cls‘𝐽)‘(𝐹𝑢)))
8277, 81sylib 207 . . . . . . . . . . . . . . . 16 (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → ∃𝑢 ∈ ran ℤ𝑛 = ((cls‘𝐽)‘(𝐹𝑢)))
83 uzin2 13932 . . . . . . . . . . . . . . . . . . . 20 ((𝑢 ∈ ran ℤ𝑘 ∈ ran ℤ) → (𝑢𝑘) ∈ ran ℤ)
848, 11syl5ss 3579 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐹𝑢) ⊆ 𝑋)
8584, 13sseqtrd 3604 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐹𝑢) ⊆ 𝐽)
8616sscls 20670 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐽 ∈ Top ∧ (𝐹𝑢) ⊆ 𝐽) → (𝐹𝑢) ⊆ ((cls‘𝐽)‘(𝐹𝑢)))
877, 85, 86syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐹𝑢) ⊆ ((cls‘𝐽)‘(𝐹𝑢)))
88 sseq2 3590 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = ((cls‘𝐽)‘(𝐹𝑢)) → ((𝐹𝑢) ⊆ 𝑛 ↔ (𝐹𝑢) ⊆ ((cls‘𝐽)‘(𝐹𝑢))))
8987, 88syl5ibrcom 236 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑛 = ((cls‘𝐽)‘(𝐹𝑢)) → (𝐹𝑢) ⊆ 𝑛))
90 inss2 3796 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑢𝑘) ⊆ 𝑘
91 inss1 3795 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑢𝑘) ⊆ 𝑢
92 imass2 5420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑢𝑘) ⊆ 𝑘 → (𝐹 “ (𝑢𝑘)) ⊆ (𝐹𝑘))
93 imass2 5420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑢𝑘) ⊆ 𝑢 → (𝐹 “ (𝑢𝑘)) ⊆ (𝐹𝑢))
9492, 93anim12i 588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑢𝑘) ⊆ 𝑘 ∧ (𝑢𝑘) ⊆ 𝑢) → ((𝐹 “ (𝑢𝑘)) ⊆ (𝐹𝑘) ∧ (𝐹 “ (𝑢𝑘)) ⊆ (𝐹𝑢)))
95 ssin 3797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐹 “ (𝑢𝑘)) ⊆ (𝐹𝑘) ∧ (𝐹 “ (𝑢𝑘)) ⊆ (𝐹𝑢)) ↔ (𝐹 “ (𝑢𝑘)) ⊆ ((𝐹𝑘) ∩ (𝐹𝑢)))
9694, 95sylib 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑢𝑘) ⊆ 𝑘 ∧ (𝑢𝑘) ⊆ 𝑢) → (𝐹 “ (𝑢𝑘)) ⊆ ((𝐹𝑘) ∩ (𝐹𝑢)))
9790, 91, 96mp2an 704 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹 “ (𝑢𝑘)) ⊆ ((𝐹𝑘) ∩ (𝐹𝑢))
98 ss2in 3802 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐹𝑘) ⊆ 𝑦 ∧ (𝐹𝑢) ⊆ 𝑛) → ((𝐹𝑘) ∩ (𝐹𝑢)) ⊆ ( 𝑦𝑛))
9997, 98syl5ss 3579 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐹𝑘) ⊆ 𝑦 ∧ (𝐹𝑢) ⊆ 𝑛) → (𝐹 “ (𝑢𝑘)) ⊆ ( 𝑦𝑛))
10078intunsn 4451 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∪ {𝑛}) = ( 𝑦𝑛)
10199, 100syl6sseqr 3615 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹𝑘) ⊆ 𝑦 ∧ (𝐹𝑢) ⊆ 𝑛) → (𝐹 “ (𝑢𝑘)) ⊆ (𝑦 ∪ {𝑛}))
102101expcom 450 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹𝑢) ⊆ 𝑛 → ((𝐹𝑘) ⊆ 𝑦 → (𝐹 “ (𝑢𝑘)) ⊆ (𝑦 ∪ {𝑛})))
10389, 102syl6 34 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑛 = ((cls‘𝐽)‘(𝐹𝑢)) → ((𝐹𝑘) ⊆ 𝑦 → (𝐹 “ (𝑢𝑘)) ⊆ (𝑦 ∪ {𝑛}))))
104103impd 446 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝑛 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ (𝐹𝑘) ⊆ 𝑦) → (𝐹 “ (𝑢𝑘)) ⊆ (𝑦 ∪ {𝑛})))
105 imaeq2 5381 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚 = (𝑢𝑘) → (𝐹𝑚) = (𝐹 “ (𝑢𝑘)))
106105sseq1d 3595 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 = (𝑢𝑘) → ((𝐹𝑚) ⊆ (𝑦 ∪ {𝑛}) ↔ (𝐹 “ (𝑢𝑘)) ⊆ (𝑦 ∪ {𝑛})))
107106rspcev 3282 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑢𝑘) ∈ ran ℤ ∧ (𝐹 “ (𝑢𝑘)) ⊆ (𝑦 ∪ {𝑛})) → ∃𝑚 ∈ ran ℤ(𝐹𝑚) ⊆ (𝑦 ∪ {𝑛}))
108107expcom 450 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 “ (𝑢𝑘)) ⊆ (𝑦 ∪ {𝑛}) → ((𝑢𝑘) ∈ ran ℤ → ∃𝑚 ∈ ran ℤ(𝐹𝑚) ⊆ (𝑦 ∪ {𝑛})))
109104, 108syl6 34 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑛 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ (𝐹𝑘) ⊆ 𝑦) → ((𝑢𝑘) ∈ ran ℤ → ∃𝑚 ∈ ran ℤ(𝐹𝑚) ⊆ (𝑦 ∪ {𝑛}))))
110109com23 84 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑢𝑘) ∈ ran ℤ → ((𝑛 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ (𝐹𝑘) ⊆ 𝑦) → ∃𝑚 ∈ ran ℤ(𝐹𝑚) ⊆ (𝑦 ∪ {𝑛}))))
11183, 110syl5 33 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑢 ∈ ran ℤ𝑘 ∈ ran ℤ) → ((𝑛 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ (𝐹𝑘) ⊆ 𝑦) → ∃𝑚 ∈ ran ℤ(𝐹𝑚) ⊆ (𝑦 ∪ {𝑛}))))
112111rexlimdvv 3019 . . . . . . . . . . . . . . . . . 18 (𝜑 → (∃𝑢 ∈ ran ℤ𝑘 ∈ ran ℤ(𝑛 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ (𝐹𝑘) ⊆ 𝑦) → ∃𝑚 ∈ ran ℤ(𝐹𝑚) ⊆ (𝑦 ∪ {𝑛})))
113 reeanv 3086 . . . . . . . . . . . . . . . . . 18 (∃𝑢 ∈ ran ℤ𝑘 ∈ ran ℤ(𝑛 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ (𝐹𝑘) ⊆ 𝑦) ↔ (∃𝑢 ∈ ran ℤ𝑛 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑦))
114 imaeq2 5381 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑘 → (𝐹𝑚) = (𝐹𝑘))
115114sseq1d 3595 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑘 → ((𝐹𝑚) ⊆ (𝑦 ∪ {𝑛}) ↔ (𝐹𝑘) ⊆ (𝑦 ∪ {𝑛})))
116115cbvrexv 3148 . . . . . . . . . . . . . . . . . 18 (∃𝑚 ∈ ran ℤ(𝐹𝑚) ⊆ (𝑦 ∪ {𝑛}) ↔ ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ (𝑦 ∪ {𝑛}))
117112, 113, 1163imtr3g 283 . . . . . . . . . . . . . . . . 17 (𝜑 → ((∃𝑢 ∈ ran ℤ𝑛 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑦) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ (𝑦 ∪ {𝑛})))
118117expd 451 . . . . . . . . . . . . . . . 16 (𝜑 → (∃𝑢 ∈ ran ℤ𝑛 = ((cls‘𝐽)‘(𝐹𝑢)) → (∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑦 → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ (𝑦 ∪ {𝑛}))))
11982, 118syl5 33 . . . . . . . . . . . . . . 15 (𝜑 → (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → (∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑦 → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ (𝑦 ∪ {𝑛}))))
120119imp 444 . . . . . . . . . . . . . 14 ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → (∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑦 → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ (𝑦 ∪ {𝑛})))
12174, 120sylcom 30 . . . . . . . . . . . . 13 (((𝜑 ∧ ∀𝑘𝑦𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑦) → ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ (𝑦 ∪ {𝑛})))
122121a1i 11 . . . . . . . . . . . 12 (𝑦 ∈ Fin → (((𝜑 ∧ ∀𝑘𝑦𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑦) → ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ (𝑦 ∪ {𝑛}))))
12337, 43, 49, 55, 69, 122findcard2 8085 . . . . . . . . . . 11 (𝑟 ∈ Fin → ((𝜑 ∧ ∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑟))
124123com12 32 . . . . . . . . . 10 ((𝜑 ∧ ∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → (𝑟 ∈ Fin → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑟))
125124impr 647 . . . . . . . . 9 ((𝜑 ∧ (∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ 𝑟 ∈ Fin)) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑟)
126 ffn 5958 . . . . . . . . . . . 12 (𝐹:ℕ⟶𝑋𝐹 Fn ℕ)
1279, 126syl 17 . . . . . . . . . . 11 (𝜑𝐹 Fn ℕ)
128 inss1 3795 . . . . . . . . . . . . . . 15 (𝑘 ∩ ℕ) ⊆ 𝑘
129 imass2 5420 . . . . . . . . . . . . . . 15 ((𝑘 ∩ ℕ) ⊆ 𝑘 → (𝐹 “ (𝑘 ∩ ℕ)) ⊆ (𝐹𝑘))
130128, 129ax-mp 5 . . . . . . . . . . . . . 14 (𝐹 “ (𝑘 ∩ ℕ)) ⊆ (𝐹𝑘)
131 nnuz 11599 . . . . . . . . . . . . . . . . . . . 20 ℕ = (ℤ‘1)
132 1z 11284 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℤ
133 fnfvelrn 6264 . . . . . . . . . . . . . . . . . . . . 21 ((ℤ Fn ℤ ∧ 1 ∈ ℤ) → (ℤ‘1) ∈ ran ℤ)
13458, 132, 133mp2an 704 . . . . . . . . . . . . . . . . . . . 20 (ℤ‘1) ∈ ran ℤ
135131, 134eqeltri 2684 . . . . . . . . . . . . . . . . . . 19 ℕ ∈ ran ℤ
136 uzin2 13932 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ran ℤ ∧ ℕ ∈ ran ℤ) → (𝑘 ∩ ℕ) ∈ ran ℤ)
137135, 136mpan2 703 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ran ℤ → (𝑘 ∩ ℕ) ∈ ran ℤ)
138 uzn0 11579 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∩ ℕ) ∈ ran ℤ → (𝑘 ∩ ℕ) ≠ ∅)
139137, 138syl 17 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ran ℤ → (𝑘 ∩ ℕ) ≠ ∅)
140 n0 3890 . . . . . . . . . . . . . . . . 17 ((𝑘 ∩ ℕ) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝑘 ∩ ℕ))
141139, 140sylib 207 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ran ℤ → ∃𝑦 𝑦 ∈ (𝑘 ∩ ℕ))
142 fnfun 5902 . . . . . . . . . . . . . . . . . . 19 (𝐹 Fn ℕ → Fun 𝐹)
143 inss2 3796 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∩ ℕ) ⊆ ℕ
144 fndm 5904 . . . . . . . . . . . . . . . . . . . 20 (𝐹 Fn ℕ → dom 𝐹 = ℕ)
145143, 144syl5sseqr 3617 . . . . . . . . . . . . . . . . . . 19 (𝐹 Fn ℕ → (𝑘 ∩ ℕ) ⊆ dom 𝐹)
146 funfvima2 6397 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝐹 ∧ (𝑘 ∩ ℕ) ⊆ dom 𝐹) → (𝑦 ∈ (𝑘 ∩ ℕ) → (𝐹𝑦) ∈ (𝐹 “ (𝑘 ∩ ℕ))))
147142, 145, 146syl2anc 691 . . . . . . . . . . . . . . . . . 18 (𝐹 Fn ℕ → (𝑦 ∈ (𝑘 ∩ ℕ) → (𝐹𝑦) ∈ (𝐹 “ (𝑘 ∩ ℕ))))
148 ne0i 3880 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑦) ∈ (𝐹 “ (𝑘 ∩ ℕ)) → (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅)
149147, 148syl6 34 . . . . . . . . . . . . . . . . 17 (𝐹 Fn ℕ → (𝑦 ∈ (𝑘 ∩ ℕ) → (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅))
150149exlimdv 1848 . . . . . . . . . . . . . . . 16 (𝐹 Fn ℕ → (∃𝑦 𝑦 ∈ (𝑘 ∩ ℕ) → (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅))
151141, 150syl5 33 . . . . . . . . . . . . . . 15 (𝐹 Fn ℕ → (𝑘 ∈ ran ℤ → (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅))
152151imp 444 . . . . . . . . . . . . . 14 ((𝐹 Fn ℕ ∧ 𝑘 ∈ ran ℤ) → (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅)
153 ssn0 3928 . . . . . . . . . . . . . 14 (((𝐹 “ (𝑘 ∩ ℕ)) ⊆ (𝐹𝑘) ∧ (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅) → (𝐹𝑘) ≠ ∅)
154130, 152, 153sylancr 694 . . . . . . . . . . . . 13 ((𝐹 Fn ℕ ∧ 𝑘 ∈ ran ℤ) → (𝐹𝑘) ≠ ∅)
155 ssn0 3928 . . . . . . . . . . . . . 14 (((𝐹𝑘) ⊆ 𝑟 ∧ (𝐹𝑘) ≠ ∅) → 𝑟 ≠ ∅)
156155expcom 450 . . . . . . . . . . . . 13 ((𝐹𝑘) ≠ ∅ → ((𝐹𝑘) ⊆ 𝑟 𝑟 ≠ ∅))
157154, 156syl 17 . . . . . . . . . . . 12 ((𝐹 Fn ℕ ∧ 𝑘 ∈ ran ℤ) → ((𝐹𝑘) ⊆ 𝑟 𝑟 ≠ ∅))
158157rexlimdva 3013 . . . . . . . . . . 11 (𝐹 Fn ℕ → (∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑟 𝑟 ≠ ∅))
159127, 158syl 17 . . . . . . . . . 10 (𝜑 → (∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑟 𝑟 ≠ ∅))
160159adantr 480 . . . . . . . . 9 ((𝜑 ∧ (∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ 𝑟 ∈ Fin)) → (∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑟 𝑟 ≠ ∅))
161125, 160mpd 15 . . . . . . . 8 ((𝜑 ∧ (∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ 𝑟 ∈ Fin)) → 𝑟 ≠ ∅)
162161necomd 2837 . . . . . . 7 ((𝜑 ∧ (∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ 𝑟 ∈ Fin)) → ∅ ≠ 𝑟)
163162neneqd 2787 . . . . . 6 ((𝜑 ∧ (∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ 𝑟 ∈ Fin)) → ¬ ∅ = 𝑟)
16431, 163sylan2b 491 . . . . 5 ((𝜑𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∩ Fin)) → ¬ ∅ = 𝑟)
165164nrexdv 2984 . . . 4 (𝜑 → ¬ ∃𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∩ Fin)∅ = 𝑟)
166 0ex 4718 . . . . 5 ∅ ∈ V
167 zex 11263 . . . . . . . 8 ℤ ∈ V
168167pwex 4774 . . . . . . 7 𝒫 ℤ ∈ V
169 frn 5966 . . . . . . . 8 (ℤ:ℤ⟶𝒫 ℤ → ran ℤ ⊆ 𝒫 ℤ)
17056, 169ax-mp 5 . . . . . . 7 ran ℤ ⊆ 𝒫 ℤ
171168, 170ssexi 4731 . . . . . 6 ran ℤ ∈ V
172171abrexex 7033 . . . . 5 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∈ V
173 elfi 8202 . . . . 5 ((∅ ∈ V ∧ {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∈ V) → (∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}) ↔ ∃𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∩ Fin)∅ = 𝑟))
174166, 172, 173mp2an 704 . . . 4 (∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}) ↔ ∃𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∩ Fin)∅ = 𝑟)
175165, 174sylnibr 318 . . 3 (𝜑 → ¬ ∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}))
176 cmptop 21008 . . . . . 6 (𝐽 ∈ Comp → 𝐽 ∈ Top)
177 cmpfi 21021 . . . . . 6 (𝐽 ∈ Top → (𝐽 ∈ Comp ↔ ∀𝑚 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑚) → 𝑚 ≠ ∅)))
178176, 177syl 17 . . . . 5 (𝐽 ∈ Comp → (𝐽 ∈ Comp ↔ ∀𝑚 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑚) → 𝑚 ≠ ∅)))
179178ibi 255 . . . 4 (𝐽 ∈ Comp → ∀𝑚 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑚) → 𝑚 ≠ ∅))
180 fveq2 6103 . . . . . . . 8 (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} → (fi‘𝑚) = (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}))
181180eleq2d 2673 . . . . . . 7 (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} → (∅ ∈ (fi‘𝑚) ↔ ∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))})))
182181notbid 307 . . . . . 6 (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} → (¬ ∅ ∈ (fi‘𝑚) ↔ ¬ ∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))})))
183 inteq 4413 . . . . . . . 8 (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} → 𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))})
184183neeq1d 2841 . . . . . . 7 (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} → ( 𝑚 ≠ ∅ ↔ {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ≠ ∅))
185 n0 3890 . . . . . . 7 ( {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ≠ ∅ ↔ ∃𝑦 𝑦 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))})
186184, 185syl6bb 275 . . . . . 6 (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} → ( 𝑚 ≠ ∅ ↔ ∃𝑦 𝑦 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}))
187182, 186imbi12d 333 . . . . 5 (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} → ((¬ ∅ ∈ (fi‘𝑚) → 𝑚 ≠ ∅) ↔ (¬ ∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}) → ∃𝑦 𝑦 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))})))
188187rspccv 3279 . . . 4 (∀𝑚 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑚) → 𝑚 ≠ ∅) → ({𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∈ 𝒫 (Clsd‘𝐽) → (¬ ∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}) → ∃𝑦 𝑦 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))})))
189179, 188syl 17 . . 3 (𝐽 ∈ Comp → ({𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∈ 𝒫 (Clsd‘𝐽) → (¬ ∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}) → ∃𝑦 𝑦 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))})))
1901, 25, 175, 189syl3c 64 . 2 (𝜑 → ∃𝑦 𝑦 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))})
191 lmrel 20844 . . 3 Rel (⇝𝑡𝐽)
192 r19.23v 3005 . . . . . 6 (∀𝑢 ∈ ran ℤ(𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑦𝑘) ↔ (∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑦𝑘))
193192albii 1737 . . . . 5 (∀𝑘𝑢 ∈ ran ℤ(𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑦𝑘) ↔ ∀𝑘(∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑦𝑘))
194 fvex 6113 . . . . . . . 8 ((cls‘𝐽)‘(𝐹𝑢)) ∈ V
195 eleq2 2677 . . . . . . . 8 (𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → (𝑦𝑘𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))))
196194, 195ceqsalv 3206 . . . . . . 7 (∀𝑘(𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑦𝑘) ↔ 𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢)))
197196ralbii 2963 . . . . . 6 (∀𝑢 ∈ ran ℤ𝑘(𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑦𝑘) ↔ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢)))
198 ralcom4 3197 . . . . . 6 (∀𝑢 ∈ ran ℤ𝑘(𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑦𝑘) ↔ ∀𝑘𝑢 ∈ ran ℤ(𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑦𝑘))
199197, 198bitr3i 265 . . . . 5 (∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢)) ↔ ∀𝑘𝑢 ∈ ran ℤ(𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑦𝑘))
200 vex 3176 . . . . . 6 𝑦 ∈ V
201200elintab 4422 . . . . 5 (𝑦 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ↔ ∀𝑘(∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑦𝑘))
202193, 199, 2013bitr4i 291 . . . 4 (∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢)) ↔ 𝑦 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))})
203 eqid 2610 . . . . . . . . . . 11 ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ ℕ))
204 imaeq2 5381 . . . . . . . . . . . . . 14 (𝑢 = ℕ → (𝐹𝑢) = (𝐹 “ ℕ))
205204fveq2d 6107 . . . . . . . . . . . . 13 (𝑢 = ℕ → ((cls‘𝐽)‘(𝐹𝑢)) = ((cls‘𝐽)‘(𝐹 “ ℕ)))
206205eqeq2d 2620 . . . . . . . . . . . 12 (𝑢 = ℕ → (((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹𝑢)) ↔ ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ ℕ))))
207206rspcev 3282 . . . . . . . . . . 11 ((ℕ ∈ ran ℤ ∧ ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ ℕ))) → ∃𝑢 ∈ ran ℤ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹𝑢)))
208135, 203, 207mp2an 704 . . . . . . . . . 10 𝑢 ∈ ran ℤ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹𝑢))
209 fvex 6113 . . . . . . . . . . 11 ((cls‘𝐽)‘(𝐹 “ ℕ)) ∈ V
210 eqeq1 2614 . . . . . . . . . . . 12 (𝑘 = ((cls‘𝐽)‘(𝐹 “ ℕ)) → (𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ↔ ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹𝑢))))
211210rexbidv 3034 . . . . . . . . . . 11 (𝑘 = ((cls‘𝐽)‘(𝐹 “ ℕ)) → (∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ↔ ∃𝑢 ∈ ran ℤ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹𝑢))))
212209, 211elab 3319 . . . . . . . . . 10 (((cls‘𝐽)‘(𝐹 “ ℕ)) ∈ {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ↔ ∃𝑢 ∈ ran ℤ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹𝑢)))
213208, 212mpbir 220 . . . . . . . . 9 ((cls‘𝐽)‘(𝐹 “ ℕ)) ∈ {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}
214 intss1 4427 . . . . . . . . 9 (((cls‘𝐽)‘(𝐹 “ ℕ)) ∈ {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} → {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ⊆ ((cls‘𝐽)‘(𝐹 “ ℕ)))
215213, 214ax-mp 5 . . . . . . . 8 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ⊆ ((cls‘𝐽)‘(𝐹 “ ℕ))
216 imassrn 5396 . . . . . . . . . . 11 (𝐹 “ ℕ) ⊆ ran 𝐹
217216, 14syl5ss 3579 . . . . . . . . . 10 (𝜑 → (𝐹 “ ℕ) ⊆ 𝐽)
21816clsss3 20673 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ (𝐹 “ ℕ) ⊆ 𝐽) → ((cls‘𝐽)‘(𝐹 “ ℕ)) ⊆ 𝐽)
2197, 217, 218syl2anc 691 . . . . . . . . 9 (𝜑 → ((cls‘𝐽)‘(𝐹 “ ℕ)) ⊆ 𝐽)
220219, 13sseqtr4d 3605 . . . . . . . 8 (𝜑 → ((cls‘𝐽)‘(𝐹 “ ℕ)) ⊆ 𝑋)
221215, 220syl5ss 3579 . . . . . . 7 (𝜑 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ⊆ 𝑋)
222221sselda 3568 . . . . . 6 ((𝜑𝑦 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}) → 𝑦𝑋)
223202, 222sylan2b 491 . . . . 5 ((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) → 𝑦𝑋)
224 heibor1.5 . . . . . . . . . . . 12 (𝜑𝐹 ∈ (Cau‘𝐷))
225 1zzd 11285 . . . . . . . . . . . . 13 (𝜑 → 1 ∈ ℤ)
226131, 4, 225iscau3 22884 . . . . . . . . . . . 12 (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋pm ℂ) ∧ ∀𝑦 ∈ ℝ+𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦))))
227224, 226mpbid 221 . . . . . . . . . . 11 (𝜑 → (𝐹 ∈ (𝑋pm ℂ) ∧ ∀𝑦 ∈ ℝ+𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦)))
228227simprd 478 . . . . . . . . . 10 (𝜑 → ∀𝑦 ∈ ℝ+𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦))
229 simp3 1056 . . . . . . . . . . . . 13 ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦) → ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦)
230229ralimi 2936 . . . . . . . . . . . 12 (∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦) → ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦)
231230reximi 2994 . . . . . . . . . . 11 (∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦) → ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦)
232231ralimi 2936 . . . . . . . . . 10 (∀𝑦 ∈ ℝ+𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦) → ∀𝑦 ∈ ℝ+𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦)
233228, 232syl 17 . . . . . . . . 9 (𝜑 → ∀𝑦 ∈ ℝ+𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦)
234233adantr 480 . . . . . . . 8 ((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) → ∀𝑦 ∈ ℝ+𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦)
235 rphalfcl 11734 . . . . . . . 8 (𝑟 ∈ ℝ+ → (𝑟 / 2) ∈ ℝ+)
236 breq2 4587 . . . . . . . . . . 11 (𝑦 = (𝑟 / 2) → (((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦 ↔ ((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2)))
2372362ralbidv 2972 . . . . . . . . . 10 (𝑦 = (𝑟 / 2) → (∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦 ↔ ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2)))
238237rexbidv 3034 . . . . . . . . 9 (𝑦 = (𝑟 / 2) → (∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦 ↔ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2)))
239238rspccva 3281 . . . . . . . 8 ((∀𝑦 ∈ ℝ+𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦 ∧ (𝑟 / 2) ∈ ℝ+) → ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2))
240234, 235, 239syl2an 493 . . . . . . 7 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ 𝑟 ∈ ℝ+) → ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2))
241 ffun 5961 . . . . . . . . . . . . 13 (𝐹:ℕ⟶𝑋 → Fun 𝐹)
2429, 241syl 17 . . . . . . . . . . . 12 (𝜑 → Fun 𝐹)
243242ad2antrr 758 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → Fun 𝐹)
2447ad2antrr 758 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → 𝐽 ∈ Top)
245 imassrn 5396 . . . . . . . . . . . . . 14 (𝐹 “ (ℤ𝑚)) ⊆ ran 𝐹
246245, 14syl5ss 3579 . . . . . . . . . . . . 13 (𝜑 → (𝐹 “ (ℤ𝑚)) ⊆ 𝐽)
247246ad2antrr 758 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → (𝐹 “ (ℤ𝑚)) ⊆ 𝐽)
248 nnz 11276 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ → 𝑚 ∈ ℤ)
249 fnfvelrn 6264 . . . . . . . . . . . . . . 15 ((ℤ Fn ℤ ∧ 𝑚 ∈ ℤ) → (ℤ𝑚) ∈ ran ℤ)
25058, 248, 249sylancr 694 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ → (ℤ𝑚) ∈ ran ℤ)
251250ad2antll 761 . . . . . . . . . . . . 13 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → (ℤ𝑚) ∈ ran ℤ)
252 simplr 788 . . . . . . . . . . . . 13 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢)))
253 imaeq2 5381 . . . . . . . . . . . . . . . 16 (𝑢 = (ℤ𝑚) → (𝐹𝑢) = (𝐹 “ (ℤ𝑚)))
254253fveq2d 6107 . . . . . . . . . . . . . . 15 (𝑢 = (ℤ𝑚) → ((cls‘𝐽)‘(𝐹𝑢)) = ((cls‘𝐽)‘(𝐹 “ (ℤ𝑚))))
255254eleq2d 2673 . . . . . . . . . . . . . 14 (𝑢 = (ℤ𝑚) → (𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢)) ↔ 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ (ℤ𝑚)))))
256255rspcv 3278 . . . . . . . . . . . . 13 ((ℤ𝑚) ∈ ran ℤ → (∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢)) → 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ (ℤ𝑚)))))
257251, 252, 256sylc 63 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ (ℤ𝑚))))
2584ad2antrr 758 . . . . . . . . . . . . 13 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → 𝐷 ∈ (∞Met‘𝑋))
259223adantr 480 . . . . . . . . . . . . 13 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → 𝑦𝑋)
260235ad2antrl 760 . . . . . . . . . . . . . 14 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → (𝑟 / 2) ∈ ℝ+)
261260rpxrd 11749 . . . . . . . . . . . . 13 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → (𝑟 / 2) ∈ ℝ*)
2625blopn 22115 . . . . . . . . . . . . 13 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦𝑋 ∧ (𝑟 / 2) ∈ ℝ*) → (𝑦(ball‘𝐷)(𝑟 / 2)) ∈ 𝐽)
263258, 259, 261, 262syl3anc 1318 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → (𝑦(ball‘𝐷)(𝑟 / 2)) ∈ 𝐽)
264 blcntr 22028 . . . . . . . . . . . . 13 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦𝑋 ∧ (𝑟 / 2) ∈ ℝ+) → 𝑦 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
265258, 259, 260, 264syl3anc 1318 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → 𝑦 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
26616clsndisj 20689 . . . . . . . . . . . 12 (((𝐽 ∈ Top ∧ (𝐹 “ (ℤ𝑚)) ⊆ 𝐽𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ (ℤ𝑚)))) ∧ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∈ 𝐽𝑦 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) → ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚))) ≠ ∅)
267244, 247, 257, 263, 265, 266syl32anc 1326 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚))) ≠ ∅)
268 n0 3890 . . . . . . . . . . . 12 (((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚))) ≠ ∅ ↔ ∃𝑛 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚))))
269 inss2 3796 . . . . . . . . . . . . . . . . 17 ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚))) ⊆ (𝐹 “ (ℤ𝑚))
270269sseli 3564 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚))) → 𝑛 ∈ (𝐹 “ (ℤ𝑚)))
271 fvelima 6158 . . . . . . . . . . . . . . . 16 ((Fun 𝐹𝑛 ∈ (𝐹 “ (ℤ𝑚))) → ∃𝑘 ∈ (ℤ𝑚)(𝐹𝑘) = 𝑛)
272270, 271sylan2 490 . . . . . . . . . . . . . . 15 ((Fun 𝐹𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚)))) → ∃𝑘 ∈ (ℤ𝑚)(𝐹𝑘) = 𝑛)
273 inss1 3795 . . . . . . . . . . . . . . . . . . 19 ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚))) ⊆ (𝑦(ball‘𝐷)(𝑟 / 2))
274273sseli 3564 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚))) → 𝑛 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
275274adantl 481 . . . . . . . . . . . . . . . . 17 ((Fun 𝐹𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚)))) → 𝑛 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
276 eleq1a 2683 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) → ((𝐹𝑘) = 𝑛 → (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
277275, 276syl 17 . . . . . . . . . . . . . . . 16 ((Fun 𝐹𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚)))) → ((𝐹𝑘) = 𝑛 → (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
278277reximdv 2999 . . . . . . . . . . . . . . 15 ((Fun 𝐹𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚)))) → (∃𝑘 ∈ (ℤ𝑚)(𝐹𝑘) = 𝑛 → ∃𝑘 ∈ (ℤ𝑚)(𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
279272, 278mpd 15 . . . . . . . . . . . . . 14 ((Fun 𝐹𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚)))) → ∃𝑘 ∈ (ℤ𝑚)(𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
280279ex 449 . . . . . . . . . . . . 13 (Fun 𝐹 → (𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚))) → ∃𝑘 ∈ (ℤ𝑚)(𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
281280exlimdv 1848 . . . . . . . . . . . 12 (Fun 𝐹 → (∃𝑛 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚))) → ∃𝑘 ∈ (ℤ𝑚)(𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
282268, 281syl5bi 231 . . . . . . . . . . 11 (Fun 𝐹 → (((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚))) ≠ ∅ → ∃𝑘 ∈ (ℤ𝑚)(𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
283243, 267, 282sylc 63 . . . . . . . . . 10 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → ∃𝑘 ∈ (ℤ𝑚)(𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
284 r19.29 3054 . . . . . . . . . . 11 ((∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) ∧ ∃𝑘 ∈ (ℤ𝑚)(𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ (ℤ𝑚)(∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
285 uznnssnn 11611 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ → (ℤ𝑚) ⊆ ℕ)
286285ad2antll 761 . . . . . . . . . . . . 13 (((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → (ℤ𝑚) ⊆ ℕ)
287 simprlr 799 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
2884ad3antrrr 762 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → 𝐷 ∈ (∞Met‘𝑋))
289 simplrl 796 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → 𝑟 ∈ ℝ+)
290289, 235syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → (𝑟 / 2) ∈ ℝ+)
291290rpxrd 11749 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → (𝑟 / 2) ∈ ℝ*)
292 simpllr 795 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → 𝑦𝑋)
2939ad3antrrr 762 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → 𝐹:ℕ⟶𝑋)
294 eluznn 11634 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑚 ∈ ℕ ∧ 𝑘 ∈ (ℤ𝑚)) → 𝑘 ∈ ℕ)
295294ad2ant2lr 780 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑟 ∈ ℝ+𝑚 ∈ ℕ) ∧ (𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) → 𝑘 ∈ ℕ)
296295ad2ant2lr 780 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → 𝑘 ∈ ℕ)
297293, 296ffvelrnd 6268 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → (𝐹𝑘) ∈ 𝑋)
298 elbl3 22007 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑟 / 2) ∈ ℝ*) ∧ (𝑦𝑋 ∧ (𝐹𝑘) ∈ 𝑋)) → ((𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) ↔ ((𝐹𝑘)𝐷𝑦) < (𝑟 / 2)))
299288, 291, 292, 297, 298syl22anc 1319 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → ((𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) ↔ ((𝐹𝑘)𝐷𝑦) < (𝑟 / 2)))
300287, 299mpbid 221 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → ((𝐹𝑘)𝐷𝑦) < (𝑟 / 2))
3012ad3antrrr 762 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → 𝐷 ∈ (Met‘𝑋))
302 simprr 792 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → 𝑛 ∈ (ℤ𝑘))
303 eluznn 11634 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑘 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑘)) → 𝑛 ∈ ℕ)
304296, 302, 303syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → 𝑛 ∈ ℕ)
305293, 304ffvelrnd 6268 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → (𝐹𝑛) ∈ 𝑋)
306 metcl 21947 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑛) ∈ 𝑋) → ((𝐹𝑘)𝐷(𝐹𝑛)) ∈ ℝ)
307301, 297, 305, 306syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → ((𝐹𝑘)𝐷(𝐹𝑛)) ∈ ℝ)
308 metcl 21947 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹𝑘) ∈ 𝑋𝑦𝑋) → ((𝐹𝑘)𝐷𝑦) ∈ ℝ)
309301, 297, 292, 308syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → ((𝐹𝑘)𝐷𝑦) ∈ ℝ)
310290rpred 11748 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → (𝑟 / 2) ∈ ℝ)
311 lt2add 10392 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐹𝑘)𝐷(𝐹𝑛)) ∈ ℝ ∧ ((𝐹𝑘)𝐷𝑦) ∈ ℝ) ∧ ((𝑟 / 2) ∈ ℝ ∧ (𝑟 / 2) ∈ ℝ)) → ((((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) ∧ ((𝐹𝑘)𝐷𝑦) < (𝑟 / 2)) → (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) < ((𝑟 / 2) + (𝑟 / 2))))
312307, 309, 310, 310, 311syl22anc 1319 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → ((((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) ∧ ((𝐹𝑘)𝐷𝑦) < (𝑟 / 2)) → (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) < ((𝑟 / 2) + (𝑟 / 2))))
313300, 312mpan2d 706 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → (((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) → (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) < ((𝑟 / 2) + (𝑟 / 2))))
314289rpcnd 11750 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → 𝑟 ∈ ℂ)
3153142halvesd 11155 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → ((𝑟 / 2) + (𝑟 / 2)) = 𝑟)
316315breq2d 4595 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → ((((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) < ((𝑟 / 2) + (𝑟 / 2)) ↔ (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) < 𝑟))
317313, 316sylibd 228 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → (((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) → (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) < 𝑟))
318 mettri2 21956 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐷 ∈ (Met‘𝑋) ∧ ((𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑛) ∈ 𝑋𝑦𝑋)) → ((𝐹𝑛)𝐷𝑦) ≤ (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)))
319301, 297, 305, 292, 318syl13anc 1320 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → ((𝐹𝑛)𝐷𝑦) ≤ (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)))
320 metcl 21947 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹𝑛) ∈ 𝑋𝑦𝑋) → ((𝐹𝑛)𝐷𝑦) ∈ ℝ)
321301, 305, 292, 320syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → ((𝐹𝑛)𝐷𝑦) ∈ ℝ)
322307, 309readdcld 9948 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) ∈ ℝ)
323289rpred 11748 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → 𝑟 ∈ ℝ)
324 lelttr 10007 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑛)𝐷𝑦) ∈ ℝ ∧ (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) ∈ ℝ ∧ 𝑟 ∈ ℝ) → ((((𝐹𝑛)𝐷𝑦) ≤ (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) ∧ (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) < 𝑟) → ((𝐹𝑛)𝐷𝑦) < 𝑟))
325321, 322, 323, 324syl3anc 1318 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → ((((𝐹𝑛)𝐷𝑦) ≤ (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) ∧ (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) < 𝑟) → ((𝐹𝑛)𝐷𝑦) < 𝑟))
326319, 325mpand 707 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → ((((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) < 𝑟 → ((𝐹𝑛)𝐷𝑦) < 𝑟))
327317, 326syld 46 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → (((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) → ((𝐹𝑛)𝐷𝑦) < 𝑟))
328327anassrs 678 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ (𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) ∧ 𝑛 ∈ (ℤ𝑘)) → (((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) → ((𝐹𝑛)𝐷𝑦) < 𝑟))
329328ralimdva 2945 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ (𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) → (∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) → ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟))
330329expr 641 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ 𝑘 ∈ (ℤ𝑚)) → ((𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) → (∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) → ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟)))
331330com23 84 . . . . . . . . . . . . . . 15 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ 𝑘 ∈ (ℤ𝑚)) → (∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) → ((𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) → ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟)))
332331impd 446 . . . . . . . . . . . . . 14 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ 𝑘 ∈ (ℤ𝑚)) → ((∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟))
333332reximdva 3000 . . . . . . . . . . . . 13 (((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → (∃𝑘 ∈ (ℤ𝑚)(∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟))
334 ssrexv 3630 . . . . . . . . . . . . 13 ((ℤ𝑚) ⊆ ℕ → (∃𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟 → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟))
335286, 333, 334sylsyld 59 . . . . . . . . . . . 12 (((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → (∃𝑘 ∈ (ℤ𝑚)(∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟))
336223, 335syldanl 731 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → (∃𝑘 ∈ (ℤ𝑚)(∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟))
337284, 336syl5 33 . . . . . . . . . 10 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → ((∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) ∧ ∃𝑘 ∈ (ℤ𝑚)(𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟))
338283, 337mpan2d 706 . . . . . . . . 9 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → (∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟))
339338anassrs 678 . . . . . . . 8 ((((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ 𝑟 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) → (∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟))
340339rexlimdva 3013 . . . . . . 7 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ 𝑟 ∈ ℝ+) → (∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟))
341240, 340mpd 15 . . . . . 6 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ 𝑟 ∈ ℝ+) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟)
342341ralrimiva 2949 . . . . 5 ((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) → ∀𝑟 ∈ ℝ+𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟)
343 eqidd 2611 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) = (𝐹𝑛))
3445, 4, 131, 225, 343, 9lmmbrf 22868 . . . . . 6 (𝜑 → (𝐹(⇝𝑡𝐽)𝑦 ↔ (𝑦𝑋 ∧ ∀𝑟 ∈ ℝ+𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟)))
345344adantr 480 . . . . 5 ((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) → (𝐹(⇝𝑡𝐽)𝑦 ↔ (𝑦𝑋 ∧ ∀𝑟 ∈ ℝ+𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟)))
346223, 342, 345mpbir2and 959 . . . 4 ((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) → 𝐹(⇝𝑡𝐽)𝑦)
347202, 346sylan2br 492 . . 3 ((𝜑𝑦 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}) → 𝐹(⇝𝑡𝐽)𝑦)
348 releldm 5279 . . 3 ((Rel (⇝𝑡𝐽) ∧ 𝐹(⇝𝑡𝐽)𝑦) → 𝐹 ∈ dom (⇝𝑡𝐽))
349191, 347, 348sylancr 694 . 2 ((𝜑𝑦 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}) → 𝐹 ∈ dom (⇝𝑡𝐽))
350190, 349exlimddv 1850 1 (𝜑𝐹 ∈ dom (⇝𝑡𝐽))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031  ∀wal 1473   = wceq 1475  ∃wex 1695   ∈ wcel 1977  {cab 2596   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108  {csn 4125  ∪ cuni 4372  ∩ cint 4410   class class class wbr 4583  dom cdm 5038  ran crn 5039   “ cima 5041  Rel wrel 5043  Fun wfun 5798   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ↑pm cpm 7745  Fincfn 7841  ficfi 8199  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818  ℝ*cxr 9952   < clt 9953   ≤ cle 9954   / cdiv 10563  ℕcn 10897  2c2 10947  ℤcz 11254  ℤ≥cuz 11563  ℝ+crp 11708  ∞Metcxmt 19552  Metcme 19553  ballcbl 19554  MetOpencmopn 19557  Topctop 20517  Clsdccld 20630  clsccl 20632  ⇝𝑡clm 20840  Compccmp 20999  Caucca 22859 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fi 8200  df-sup 8231  df-inf 8232  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-n0 11170  df-z 11255  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-topgen 15927  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-top 20521  df-bases 20522  df-topon 20523  df-cld 20633  df-ntr 20634  df-cls 20635  df-lm 20843  df-cmp 21000  df-cau 22862 This theorem is referenced by:  heibor1  32779
 Copyright terms: Public domain W3C validator