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

Theorem heibor1lem 37410
Description: Lemma for heibor1 37411. 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 24284 . . . . . . . . . 10 (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
42, 3syl 17 . . . . . . . . 9 (𝜑𝐷 ∈ (∞Met‘𝑋))
5 heibor.1 . . . . . . . . . 10 𝐽 = (MetOpen‘𝐷)
65mopntop 24390 . . . . . . . . 9 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
74, 6syl 17 . . . . . . . 8 (𝜑𝐽 ∈ Top)
8 imassrn 6075 . . . . . . . . 9 (𝐹𝑢) ⊆ ran 𝐹
9 heibor1.6 . . . . . . . . . . 11 (𝜑𝐹:ℕ⟶𝑋)
109frnd 6731 . . . . . . . . . 10 (𝜑 → ran 𝐹𝑋)
115mopnuni 24391 . . . . . . . . . . 11 (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = 𝐽)
124, 11syl 17 . . . . . . . . . 10 (𝜑𝑋 = 𝐽)
1310, 12sseqtrd 4017 . . . . . . . . 9 (𝜑 → ran 𝐹 𝐽)
148, 13sstrid 3988 . . . . . . . 8 (𝜑 → (𝐹𝑢) ⊆ 𝐽)
15 eqid 2725 . . . . . . . . 9 𝐽 = 𝐽
1615clscld 22995 . . . . . . . 8 ((𝐽 ∈ Top ∧ (𝐹𝑢) ⊆ 𝐽) → ((cls‘𝐽)‘(𝐹𝑢)) ∈ (Clsd‘𝐽))
177, 14, 16syl2anc 582 . . . . . . 7 (𝜑 → ((cls‘𝐽)‘(𝐹𝑢)) ∈ (Clsd‘𝐽))
18 eleq1a 2820 . . . . . . 7 (((cls‘𝐽)‘(𝐹𝑢)) ∈ (Clsd‘𝐽) → (𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑘 ∈ (Clsd‘𝐽)))
1917, 18syl 17 . . . . . 6 (𝜑 → (𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑘 ∈ (Clsd‘𝐽)))
2019rexlimdvw 3149 . . . . 5 (𝜑 → (∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑘 ∈ (Clsd‘𝐽)))
2120abssdv 4061 . . . 4 (𝜑 → {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ⊆ (Clsd‘𝐽))
22 fvex 6909 . . . . 5 (Clsd‘𝐽) ∈ V
2322elpw2 5348 . . . 4 ({𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∈ 𝒫 (Clsd‘𝐽) ↔ {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ⊆ (Clsd‘𝐽))
2421, 23sylibr 233 . . 3 (𝜑 → {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∈ 𝒫 (Clsd‘𝐽))
25 elin 3960 . . . . . . 7 (𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∩ Fin) ↔ (𝑟 ∈ 𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∧ 𝑟 ∈ Fin))
26 velpw 4609 . . . . . . . . 9 (𝑟 ∈ 𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ↔ 𝑟 ⊆ {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))})
27 ssabral 4056 . . . . . . . . 9 (𝑟 ⊆ {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ↔ ∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)))
2826, 27bitri 274 . . . . . . . 8 (𝑟 ∈ 𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ↔ ∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)))
2928anbi1i 622 . . . . . . 7 ((𝑟 ∈ 𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∧ 𝑟 ∈ Fin) ↔ (∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ 𝑟 ∈ Fin))
3025, 29bitri 274 . . . . . 6 (𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∩ Fin) ↔ (∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ 𝑟 ∈ Fin))
31 raleq 3311 . . . . . . . . . . . . . 14 (𝑚 = ∅ → (∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ↔ ∀𝑘 ∈ ∅ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))))
3231anbi2d 628 . . . . . . . . . . . . 13 (𝑚 = ∅ → ((𝜑 ∧ ∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) ↔ (𝜑 ∧ ∀𝑘 ∈ ∅ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)))))
33 inteq 4953 . . . . . . . . . . . . . . 15 (𝑚 = ∅ → 𝑚 = ∅)
3433sseq2d 4009 . . . . . . . . . . . . . 14 (𝑚 = ∅ → ((𝐹𝑘) ⊆ 𝑚 ↔ (𝐹𝑘) ⊆ ∅))
3534rexbidv 3168 . . . . . . . . . . . . 13 (𝑚 = ∅ → (∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑚 ↔ ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ ∅))
3632, 35imbi12d 343 . . . . . . . . . . . 12 (𝑚 = ∅ → (((𝜑 ∧ ∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑚) ↔ ((𝜑 ∧ ∀𝑘 ∈ ∅ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ ∅)))
37 raleq 3311 . . . . . . . . . . . . . 14 (𝑚 = 𝑦 → (∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ↔ ∀𝑘𝑦𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))))
3837anbi2d 628 . . . . . . . . . . . . 13 (𝑚 = 𝑦 → ((𝜑 ∧ ∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) ↔ (𝜑 ∧ ∀𝑘𝑦𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)))))
39 inteq 4953 . . . . . . . . . . . . . . 15 (𝑚 = 𝑦 𝑚 = 𝑦)
4039sseq2d 4009 . . . . . . . . . . . . . 14 (𝑚 = 𝑦 → ((𝐹𝑘) ⊆ 𝑚 ↔ (𝐹𝑘) ⊆ 𝑦))
4140rexbidv 3168 . . . . . . . . . . . . 13 (𝑚 = 𝑦 → (∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑚 ↔ ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑦))
4238, 41imbi12d 343 . . . . . . . . . . . 12 (𝑚 = 𝑦 → (((𝜑 ∧ ∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑚) ↔ ((𝜑 ∧ ∀𝑘𝑦𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑦)))
43 raleq 3311 . . . . . . . . . . . . . 14 (𝑚 = (𝑦 ∪ {𝑛}) → (∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ↔ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))))
4443anbi2d 628 . . . . . . . . . . . . 13 (𝑚 = (𝑦 ∪ {𝑛}) → ((𝜑 ∧ ∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) ↔ (𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)))))
45 inteq 4953 . . . . . . . . . . . . . . 15 (𝑚 = (𝑦 ∪ {𝑛}) → 𝑚 = (𝑦 ∪ {𝑛}))
4645sseq2d 4009 . . . . . . . . . . . . . 14 (𝑚 = (𝑦 ∪ {𝑛}) → ((𝐹𝑘) ⊆ 𝑚 ↔ (𝐹𝑘) ⊆ (𝑦 ∪ {𝑛})))
4746rexbidv 3168 . . . . . . . . . . . . 13 (𝑚 = (𝑦 ∪ {𝑛}) → (∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑚 ↔ ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ (𝑦 ∪ {𝑛})))
4844, 47imbi12d 343 . . . . . . . . . . . 12 (𝑚 = (𝑦 ∪ {𝑛}) → (((𝜑 ∧ ∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑚) ↔ ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ (𝑦 ∪ {𝑛}))))
49 raleq 3311 . . . . . . . . . . . . . 14 (𝑚 = 𝑟 → (∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ↔ ∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))))
5049anbi2d 628 . . . . . . . . . . . . 13 (𝑚 = 𝑟 → ((𝜑 ∧ ∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) ↔ (𝜑 ∧ ∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)))))
51 inteq 4953 . . . . . . . . . . . . . . 15 (𝑚 = 𝑟 𝑚 = 𝑟)
5251sseq2d 4009 . . . . . . . . . . . . . 14 (𝑚 = 𝑟 → ((𝐹𝑘) ⊆ 𝑚 ↔ (𝐹𝑘) ⊆ 𝑟))
5352rexbidv 3168 . . . . . . . . . . . . 13 (𝑚 = 𝑟 → (∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑚 ↔ ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑟))
5450, 53imbi12d 343 . . . . . . . . . . . 12 (𝑚 = 𝑟 → (((𝜑 ∧ ∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑚) ↔ ((𝜑 ∧ ∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑟)))
55 uzf 12858 . . . . . . . . . . . . . . . 16 :ℤ⟶𝒫 ℤ
56 ffn 6723 . . . . . . . . . . . . . . . 16 (ℤ:ℤ⟶𝒫 ℤ → ℤ Fn ℤ)
5755, 56ax-mp 5 . . . . . . . . . . . . . . 15 Fn ℤ
58 0z 12602 . . . . . . . . . . . . . . 15 0 ∈ ℤ
59 fnfvelrn 7089 . . . . . . . . . . . . . . 15 ((ℤ Fn ℤ ∧ 0 ∈ ℤ) → (ℤ‘0) ∈ ran ℤ)
6057, 58, 59mp2an 690 . . . . . . . . . . . . . 14 (ℤ‘0) ∈ ran ℤ
61 ssv 4001 . . . . . . . . . . . . . . 15 (𝐹 “ (ℤ‘0)) ⊆ V
62 int0 4966 . . . . . . . . . . . . . . 15 ∅ = V
6361, 62sseqtrri 4014 . . . . . . . . . . . . . 14 (𝐹 “ (ℤ‘0)) ⊆
64 imaeq2 6060 . . . . . . . . . . . . . . . 16 (𝑘 = (ℤ‘0) → (𝐹𝑘) = (𝐹 “ (ℤ‘0)))
6564sseq1d 4008 . . . . . . . . . . . . . . 15 (𝑘 = (ℤ‘0) → ((𝐹𝑘) ⊆ ∅ ↔ (𝐹 “ (ℤ‘0)) ⊆ ∅))
6665rspcev 3606 . . . . . . . . . . . . . 14 (((ℤ‘0) ∈ ran ℤ ∧ (𝐹 “ (ℤ‘0)) ⊆ ∅) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ ∅)
6760, 63, 66mp2an 690 . . . . . . . . . . . . 13 𝑘 ∈ ran ℤ(𝐹𝑘) ⊆
6867a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ ∀𝑘 ∈ ∅ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ ∅)
69 ssun1 4170 . . . . . . . . . . . . . . . . 17 𝑦 ⊆ (𝑦 ∪ {𝑛})
70 ssralv 4045 . . . . . . . . . . . . . . . . 17 (𝑦 ⊆ (𝑦 ∪ {𝑛}) → (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → ∀𝑘𝑦𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))))
7169, 70ax-mp 5 . . . . . . . . . . . . . . . 16 (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → ∀𝑘𝑦𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)))
7271anim2i 615 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → (𝜑 ∧ ∀𝑘𝑦𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))))
7372imim1i 63 . . . . . . . . . . . . . 14 (((𝜑 ∧ ∀𝑘𝑦𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑦) → ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑦))
74 ssun2 4171 . . . . . . . . . . . . . . . . . 18 {𝑛} ⊆ (𝑦 ∪ {𝑛})
75 ssralv 4045 . . . . . . . . . . . . . . . . . 18 ({𝑛} ⊆ (𝑦 ∪ {𝑛}) → (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → ∀𝑘 ∈ {𝑛}∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))))
7674, 75ax-mp 5 . . . . . . . . . . . . . . . . 17 (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → ∀𝑘 ∈ {𝑛}∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)))
77 vex 3465 . . . . . . . . . . . . . . . . . 18 𝑛 ∈ V
78 eqeq1 2729 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑛 → (𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ↔ 𝑛 = ((cls‘𝐽)‘(𝐹𝑢))))
7978rexbidv 3168 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑛 → (∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ↔ ∃𝑢 ∈ ran ℤ𝑛 = ((cls‘𝐽)‘(𝐹𝑢))))
8077, 79ralsn 4687 . . . . . . . . . . . . . . . . 17 (∀𝑘 ∈ {𝑛}∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ↔ ∃𝑢 ∈ ran ℤ𝑛 = ((cls‘𝐽)‘(𝐹𝑢)))
8176, 80sylib 217 . . . . . . . . . . . . . . . 16 (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → ∃𝑢 ∈ ran ℤ𝑛 = ((cls‘𝐽)‘(𝐹𝑢)))
82 uzin2 15327 . . . . . . . . . . . . . . . . . . . 20 ((𝑢 ∈ ran ℤ𝑘 ∈ ran ℤ) → (𝑢𝑘) ∈ ran ℤ)
838, 10sstrid 3988 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐹𝑢) ⊆ 𝑋)
8483, 12sseqtrd 4017 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐹𝑢) ⊆ 𝐽)
8515sscls 23004 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐽 ∈ Top ∧ (𝐹𝑢) ⊆ 𝐽) → (𝐹𝑢) ⊆ ((cls‘𝐽)‘(𝐹𝑢)))
867, 84, 85syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐹𝑢) ⊆ ((cls‘𝐽)‘(𝐹𝑢)))
87 sseq2 4003 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = ((cls‘𝐽)‘(𝐹𝑢)) → ((𝐹𝑢) ⊆ 𝑛 ↔ (𝐹𝑢) ⊆ ((cls‘𝐽)‘(𝐹𝑢))))
8886, 87syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑛 = ((cls‘𝐽)‘(𝐹𝑢)) → (𝐹𝑢) ⊆ 𝑛))
89 inss2 4228 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑢𝑘) ⊆ 𝑘
90 inss1 4227 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑢𝑘) ⊆ 𝑢
91 imass2 6107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑢𝑘) ⊆ 𝑘 → (𝐹 “ (𝑢𝑘)) ⊆ (𝐹𝑘))
92 imass2 6107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑢𝑘) ⊆ 𝑢 → (𝐹 “ (𝑢𝑘)) ⊆ (𝐹𝑢))
9391, 92anim12i 611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑢𝑘) ⊆ 𝑘 ∧ (𝑢𝑘) ⊆ 𝑢) → ((𝐹 “ (𝑢𝑘)) ⊆ (𝐹𝑘) ∧ (𝐹 “ (𝑢𝑘)) ⊆ (𝐹𝑢)))
94 ssin 4229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐹 “ (𝑢𝑘)) ⊆ (𝐹𝑘) ∧ (𝐹 “ (𝑢𝑘)) ⊆ (𝐹𝑢)) ↔ (𝐹 “ (𝑢𝑘)) ⊆ ((𝐹𝑘) ∩ (𝐹𝑢)))
9593, 94sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑢𝑘) ⊆ 𝑘 ∧ (𝑢𝑘) ⊆ 𝑢) → (𝐹 “ (𝑢𝑘)) ⊆ ((𝐹𝑘) ∩ (𝐹𝑢)))
9689, 90, 95mp2an 690 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹 “ (𝑢𝑘)) ⊆ ((𝐹𝑘) ∩ (𝐹𝑢))
97 ss2in 4235 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐹𝑘) ⊆ 𝑦 ∧ (𝐹𝑢) ⊆ 𝑛) → ((𝐹𝑘) ∩ (𝐹𝑢)) ⊆ ( 𝑦𝑛))
9896, 97sstrid 3988 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐹𝑘) ⊆ 𝑦 ∧ (𝐹𝑢) ⊆ 𝑛) → (𝐹 “ (𝑢𝑘)) ⊆ ( 𝑦𝑛))
9977intunsn 4993 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∪ {𝑛}) = ( 𝑦𝑛)
10098, 99sseqtrrdi 4028 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹𝑘) ⊆ 𝑦 ∧ (𝐹𝑢) ⊆ 𝑛) → (𝐹 “ (𝑢𝑘)) ⊆ (𝑦 ∪ {𝑛}))
101100expcom 412 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹𝑢) ⊆ 𝑛 → ((𝐹𝑘) ⊆ 𝑦 → (𝐹 “ (𝑢𝑘)) ⊆ (𝑦 ∪ {𝑛})))
10288, 101syl6 35 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑛 = ((cls‘𝐽)‘(𝐹𝑢)) → ((𝐹𝑘) ⊆ 𝑦 → (𝐹 “ (𝑢𝑘)) ⊆ (𝑦 ∪ {𝑛}))))
103102impd 409 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝑛 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ (𝐹𝑘) ⊆ 𝑦) → (𝐹 “ (𝑢𝑘)) ⊆ (𝑦 ∪ {𝑛})))
104 imaeq2 6060 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚 = (𝑢𝑘) → (𝐹𝑚) = (𝐹 “ (𝑢𝑘)))
105104sseq1d 4008 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 = (𝑢𝑘) → ((𝐹𝑚) ⊆ (𝑦 ∪ {𝑛}) ↔ (𝐹 “ (𝑢𝑘)) ⊆ (𝑦 ∪ {𝑛})))
106105rspcev 3606 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑢𝑘) ∈ ran ℤ ∧ (𝐹 “ (𝑢𝑘)) ⊆ (𝑦 ∪ {𝑛})) → ∃𝑚 ∈ ran ℤ(𝐹𝑚) ⊆ (𝑦 ∪ {𝑛}))
107106expcom 412 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 “ (𝑢𝑘)) ⊆ (𝑦 ∪ {𝑛}) → ((𝑢𝑘) ∈ ran ℤ → ∃𝑚 ∈ ran ℤ(𝐹𝑚) ⊆ (𝑦 ∪ {𝑛})))
108103, 107syl6 35 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑛 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ (𝐹𝑘) ⊆ 𝑦) → ((𝑢𝑘) ∈ ran ℤ → ∃𝑚 ∈ ran ℤ(𝐹𝑚) ⊆ (𝑦 ∪ {𝑛}))))
109108com23 86 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑢𝑘) ∈ ran ℤ → ((𝑛 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ (𝐹𝑘) ⊆ 𝑦) → ∃𝑚 ∈ ran ℤ(𝐹𝑚) ⊆ (𝑦 ∪ {𝑛}))))
11082, 109syl5 34 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑢 ∈ ran ℤ𝑘 ∈ ran ℤ) → ((𝑛 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ (𝐹𝑘) ⊆ 𝑦) → ∃𝑚 ∈ ran ℤ(𝐹𝑚) ⊆ (𝑦 ∪ {𝑛}))))
111110rexlimdvv 3200 . . . . . . . . . . . . . . . . . 18 (𝜑 → (∃𝑢 ∈ ran ℤ𝑘 ∈ ran ℤ(𝑛 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ (𝐹𝑘) ⊆ 𝑦) → ∃𝑚 ∈ ran ℤ(𝐹𝑚) ⊆ (𝑦 ∪ {𝑛})))
112 reeanv 3216 . . . . . . . . . . . . . . . . . 18 (∃𝑢 ∈ ran ℤ𝑘 ∈ ran ℤ(𝑛 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ (𝐹𝑘) ⊆ 𝑦) ↔ (∃𝑢 ∈ ran ℤ𝑛 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑦))
113 imaeq2 6060 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑘 → (𝐹𝑚) = (𝐹𝑘))
114113sseq1d 4008 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑘 → ((𝐹𝑚) ⊆ (𝑦 ∪ {𝑛}) ↔ (𝐹𝑘) ⊆ (𝑦 ∪ {𝑛})))
115114cbvrexvw 3225 . . . . . . . . . . . . . . . . . 18 (∃𝑚 ∈ ran ℤ(𝐹𝑚) ⊆ (𝑦 ∪ {𝑛}) ↔ ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ (𝑦 ∪ {𝑛}))
116111, 112, 1153imtr3g 294 . . . . . . . . . . . . . . . . 17 (𝜑 → ((∃𝑢 ∈ ran ℤ𝑛 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑦) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ (𝑦 ∪ {𝑛})))
117116expd 414 . . . . . . . . . . . . . . . 16 (𝜑 → (∃𝑢 ∈ ran ℤ𝑛 = ((cls‘𝐽)‘(𝐹𝑢)) → (∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑦 → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ (𝑦 ∪ {𝑛}))))
11881, 117syl5 34 . . . . . . . . . . . . . . 15 (𝜑 → (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → (∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑦 → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ (𝑦 ∪ {𝑛}))))
119118imp 405 . . . . . . . . . . . . . 14 ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → (∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑦 → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ (𝑦 ∪ {𝑛})))
12073, 119sylcom 30 . . . . . . . . . . . . 13 (((𝜑 ∧ ∀𝑘𝑦𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑦) → ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ (𝑦 ∪ {𝑛})))
121120a1i 11 . . . . . . . . . . . 12 (𝑦 ∈ Fin → (((𝜑 ∧ ∀𝑘𝑦𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑦) → ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ (𝑦 ∪ {𝑛}))))
12236, 42, 48, 54, 68, 121findcard2 9189 . . . . . . . . . . 11 (𝑟 ∈ Fin → ((𝜑 ∧ ∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑟))
123122com12 32 . . . . . . . . . 10 ((𝜑 ∧ ∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → (𝑟 ∈ Fin → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑟))
124123impr 453 . . . . . . . . 9 ((𝜑 ∧ (∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ 𝑟 ∈ Fin)) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑟)
1259ffnd 6724 . . . . . . . . . . 11 (𝜑𝐹 Fn ℕ)
126 inss1 4227 . . . . . . . . . . . . . . 15 (𝑘 ∩ ℕ) ⊆ 𝑘
127 imass2 6107 . . . . . . . . . . . . . . 15 ((𝑘 ∩ ℕ) ⊆ 𝑘 → (𝐹 “ (𝑘 ∩ ℕ)) ⊆ (𝐹𝑘))
128126, 127ax-mp 5 . . . . . . . . . . . . . 14 (𝐹 “ (𝑘 ∩ ℕ)) ⊆ (𝐹𝑘)
129 nnuz 12898 . . . . . . . . . . . . . . . . . . . 20 ℕ = (ℤ‘1)
130 1z 12625 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℤ
131 fnfvelrn 7089 . . . . . . . . . . . . . . . . . . . . 21 ((ℤ Fn ℤ ∧ 1 ∈ ℤ) → (ℤ‘1) ∈ ran ℤ)
13257, 130, 131mp2an 690 . . . . . . . . . . . . . . . . . . . 20 (ℤ‘1) ∈ ran ℤ
133129, 132eqeltri 2821 . . . . . . . . . . . . . . . . . . 19 ℕ ∈ ran ℤ
134 uzin2 15327 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ran ℤ ∧ ℕ ∈ ran ℤ) → (𝑘 ∩ ℕ) ∈ ran ℤ)
135133, 134mpan2 689 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ran ℤ → (𝑘 ∩ ℕ) ∈ ran ℤ)
136 uzn0 12872 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∩ ℕ) ∈ ran ℤ → (𝑘 ∩ ℕ) ≠ ∅)
137135, 136syl 17 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ran ℤ → (𝑘 ∩ ℕ) ≠ ∅)
138 n0 4346 . . . . . . . . . . . . . . . . 17 ((𝑘 ∩ ℕ) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝑘 ∩ ℕ))
139137, 138sylib 217 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ran ℤ → ∃𝑦 𝑦 ∈ (𝑘 ∩ ℕ))
140 fnfun 6655 . . . . . . . . . . . . . . . . . . 19 (𝐹 Fn ℕ → Fun 𝐹)
141 inss2 4228 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∩ ℕ) ⊆ ℕ
142 fndm 6658 . . . . . . . . . . . . . . . . . . . 20 (𝐹 Fn ℕ → dom 𝐹 = ℕ)
143141, 142sseqtrrid 4030 . . . . . . . . . . . . . . . . . . 19 (𝐹 Fn ℕ → (𝑘 ∩ ℕ) ⊆ dom 𝐹)
144 funfvima2 7243 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝐹 ∧ (𝑘 ∩ ℕ) ⊆ dom 𝐹) → (𝑦 ∈ (𝑘 ∩ ℕ) → (𝐹𝑦) ∈ (𝐹 “ (𝑘 ∩ ℕ))))
145140, 143, 144syl2anc 582 . . . . . . . . . . . . . . . . . 18 (𝐹 Fn ℕ → (𝑦 ∈ (𝑘 ∩ ℕ) → (𝐹𝑦) ∈ (𝐹 “ (𝑘 ∩ ℕ))))
146 ne0i 4334 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑦) ∈ (𝐹 “ (𝑘 ∩ ℕ)) → (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅)
147145, 146syl6 35 . . . . . . . . . . . . . . . . 17 (𝐹 Fn ℕ → (𝑦 ∈ (𝑘 ∩ ℕ) → (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅))
148147exlimdv 1928 . . . . . . . . . . . . . . . 16 (𝐹 Fn ℕ → (∃𝑦 𝑦 ∈ (𝑘 ∩ ℕ) → (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅))
149139, 148syl5 34 . . . . . . . . . . . . . . 15 (𝐹 Fn ℕ → (𝑘 ∈ ran ℤ → (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅))
150149imp 405 . . . . . . . . . . . . . 14 ((𝐹 Fn ℕ ∧ 𝑘 ∈ ran ℤ) → (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅)
151 ssn0 4402 . . . . . . . . . . . . . 14 (((𝐹 “ (𝑘 ∩ ℕ)) ⊆ (𝐹𝑘) ∧ (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅) → (𝐹𝑘) ≠ ∅)
152128, 150, 151sylancr 585 . . . . . . . . . . . . 13 ((𝐹 Fn ℕ ∧ 𝑘 ∈ ran ℤ) → (𝐹𝑘) ≠ ∅)
153 ssn0 4402 . . . . . . . . . . . . . 14 (((𝐹𝑘) ⊆ 𝑟 ∧ (𝐹𝑘) ≠ ∅) → 𝑟 ≠ ∅)
154153expcom 412 . . . . . . . . . . . . 13 ((𝐹𝑘) ≠ ∅ → ((𝐹𝑘) ⊆ 𝑟 𝑟 ≠ ∅))
155152, 154syl 17 . . . . . . . . . . . 12 ((𝐹 Fn ℕ ∧ 𝑘 ∈ ran ℤ) → ((𝐹𝑘) ⊆ 𝑟 𝑟 ≠ ∅))
156155rexlimdva 3144 . . . . . . . . . . 11 (𝐹 Fn ℕ → (∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑟 𝑟 ≠ ∅))
157125, 156syl 17 . . . . . . . . . 10 (𝜑 → (∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑟 𝑟 ≠ ∅))
158157adantr 479 . . . . . . . . 9 ((𝜑 ∧ (∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ 𝑟 ∈ Fin)) → (∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑟 𝑟 ≠ ∅))
159124, 158mpd 15 . . . . . . . 8 ((𝜑 ∧ (∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ 𝑟 ∈ Fin)) → 𝑟 ≠ ∅)
160159necomd 2985 . . . . . . 7 ((𝜑 ∧ (∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ 𝑟 ∈ Fin)) → ∅ ≠ 𝑟)
161160neneqd 2934 . . . . . 6 ((𝜑 ∧ (∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ 𝑟 ∈ Fin)) → ¬ ∅ = 𝑟)
16230, 161sylan2b 592 . . . . 5 ((𝜑𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∩ Fin)) → ¬ ∅ = 𝑟)
163162nrexdv 3138 . . . 4 (𝜑 → ¬ ∃𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∩ Fin)∅ = 𝑟)
164 0ex 5308 . . . . 5 ∅ ∈ V
165 zex 12600 . . . . . . . 8 ℤ ∈ V
166165pwex 5380 . . . . . . 7 𝒫 ℤ ∈ V
167 frn 6730 . . . . . . . 8 (ℤ:ℤ⟶𝒫 ℤ → ran ℤ ⊆ 𝒫 ℤ)
16855, 167ax-mp 5 . . . . . . 7 ran ℤ ⊆ 𝒫 ℤ
169166, 168ssexi 5323 . . . . . 6 ran ℤ ∈ V
170169abrexex 7967 . . . . 5 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∈ V
171 elfi 9438 . . . . 5 ((∅ ∈ V ∧ {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∈ V) → (∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}) ↔ ∃𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∩ Fin)∅ = 𝑟))
172164, 170, 171mp2an 690 . . . 4 (∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}) ↔ ∃𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∩ Fin)∅ = 𝑟)
173163, 172sylnibr 328 . . 3 (𝜑 → ¬ ∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}))
174 cmptop 23343 . . . . . 6 (𝐽 ∈ Comp → 𝐽 ∈ Top)
175 cmpfi 23356 . . . . . 6 (𝐽 ∈ Top → (𝐽 ∈ Comp ↔ ∀𝑚 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑚) → 𝑚 ≠ ∅)))
176174, 175syl 17 . . . . 5 (𝐽 ∈ Comp → (𝐽 ∈ Comp ↔ ∀𝑚 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑚) → 𝑚 ≠ ∅)))
177176ibi 266 . . . 4 (𝐽 ∈ Comp → ∀𝑚 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑚) → 𝑚 ≠ ∅))
178 fveq2 6896 . . . . . . . 8 (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} → (fi‘𝑚) = (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}))
179178eleq2d 2811 . . . . . . 7 (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} → (∅ ∈ (fi‘𝑚) ↔ ∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))})))
180179notbid 317 . . . . . 6 (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} → (¬ ∅ ∈ (fi‘𝑚) ↔ ¬ ∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))})))
181 inteq 4953 . . . . . . . 8 (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} → 𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))})
182181neeq1d 2989 . . . . . . 7 (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} → ( 𝑚 ≠ ∅ ↔ {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ≠ ∅))
183 n0 4346 . . . . . . 7 ( {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ≠ ∅ ↔ ∃𝑦 𝑦 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))})
184182, 183bitrdi 286 . . . . . 6 (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} → ( 𝑚 ≠ ∅ ↔ ∃𝑦 𝑦 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}))
185180, 184imbi12d 343 . . . . 5 (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} → ((¬ ∅ ∈ (fi‘𝑚) → 𝑚 ≠ ∅) ↔ (¬ ∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}) → ∃𝑦 𝑦 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))})))
186185rspccv 3603 . . . 4 (∀𝑚 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑚) → 𝑚 ≠ ∅) → ({𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∈ 𝒫 (Clsd‘𝐽) → (¬ ∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}) → ∃𝑦 𝑦 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))})))
187177, 186syl 17 . . 3 (𝐽 ∈ Comp → ({𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∈ 𝒫 (Clsd‘𝐽) → (¬ ∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}) → ∃𝑦 𝑦 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))})))
1881, 24, 173, 187syl3c 66 . 2 (𝜑 → ∃𝑦 𝑦 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))})
189 lmrel 23178 . . 3 Rel (⇝𝑡𝐽)
190 r19.23v 3172 . . . . . 6 (∀𝑢 ∈ ran ℤ(𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑦𝑘) ↔ (∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑦𝑘))
191190albii 1813 . . . . 5 (∀𝑘𝑢 ∈ ran ℤ(𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑦𝑘) ↔ ∀𝑘(∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑦𝑘))
192 fvex 6909 . . . . . . . 8 ((cls‘𝐽)‘(𝐹𝑢)) ∈ V
193 eleq2 2814 . . . . . . . 8 (𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → (𝑦𝑘𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))))
194192, 193ceqsalv 3500 . . . . . . 7 (∀𝑘(𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑦𝑘) ↔ 𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢)))
195194ralbii 3082 . . . . . 6 (∀𝑢 ∈ ran ℤ𝑘(𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑦𝑘) ↔ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢)))
196 ralcom4 3273 . . . . . 6 (∀𝑢 ∈ ran ℤ𝑘(𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑦𝑘) ↔ ∀𝑘𝑢 ∈ ran ℤ(𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑦𝑘))
197195, 196bitr3i 276 . . . . 5 (∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢)) ↔ ∀𝑘𝑢 ∈ ran ℤ(𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑦𝑘))
198 vex 3465 . . . . . 6 𝑦 ∈ V
199198elintab 4962 . . . . 5 (𝑦 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ↔ ∀𝑘(∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑦𝑘))
200191, 197, 1993bitr4i 302 . . . 4 (∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢)) ↔ 𝑦 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))})
201 eqid 2725 . . . . . . . . . . 11 ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ ℕ))
202 imaeq2 6060 . . . . . . . . . . . . 13 (𝑢 = ℕ → (𝐹𝑢) = (𝐹 “ ℕ))
203202fveq2d 6900 . . . . . . . . . . . 12 (𝑢 = ℕ → ((cls‘𝐽)‘(𝐹𝑢)) = ((cls‘𝐽)‘(𝐹 “ ℕ)))
204203rspceeqv 3628 . . . . . . . . . . 11 ((ℕ ∈ ran ℤ ∧ ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ ℕ))) → ∃𝑢 ∈ ran ℤ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹𝑢)))
205133, 201, 204mp2an 690 . . . . . . . . . 10 𝑢 ∈ ran ℤ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹𝑢))
206 fvex 6909 . . . . . . . . . . 11 ((cls‘𝐽)‘(𝐹 “ ℕ)) ∈ V
207 eqeq1 2729 . . . . . . . . . . . 12 (𝑘 = ((cls‘𝐽)‘(𝐹 “ ℕ)) → (𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ↔ ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹𝑢))))
208207rexbidv 3168 . . . . . . . . . . 11 (𝑘 = ((cls‘𝐽)‘(𝐹 “ ℕ)) → (∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ↔ ∃𝑢 ∈ ran ℤ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹𝑢))))
209206, 208elab 3664 . . . . . . . . . 10 (((cls‘𝐽)‘(𝐹 “ ℕ)) ∈ {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ↔ ∃𝑢 ∈ ran ℤ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹𝑢)))
210205, 209mpbir 230 . . . . . . . . 9 ((cls‘𝐽)‘(𝐹 “ ℕ)) ∈ {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}
211 intss1 4967 . . . . . . . . 9 (((cls‘𝐽)‘(𝐹 “ ℕ)) ∈ {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} → {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ⊆ ((cls‘𝐽)‘(𝐹 “ ℕ)))
212210, 211ax-mp 5 . . . . . . . 8 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ⊆ ((cls‘𝐽)‘(𝐹 “ ℕ))
213 imassrn 6075 . . . . . . . . . . 11 (𝐹 “ ℕ) ⊆ ran 𝐹
214213, 13sstrid 3988 . . . . . . . . . 10 (𝜑 → (𝐹 “ ℕ) ⊆ 𝐽)
21515clsss3 23007 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ (𝐹 “ ℕ) ⊆ 𝐽) → ((cls‘𝐽)‘(𝐹 “ ℕ)) ⊆ 𝐽)
2167, 214, 215syl2anc 582 . . . . . . . . 9 (𝜑 → ((cls‘𝐽)‘(𝐹 “ ℕ)) ⊆ 𝐽)
217216, 12sseqtrrd 4018 . . . . . . . 8 (𝜑 → ((cls‘𝐽)‘(𝐹 “ ℕ)) ⊆ 𝑋)
218212, 217sstrid 3988 . . . . . . 7 (𝜑 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ⊆ 𝑋)
219218sselda 3976 . . . . . 6 ((𝜑𝑦 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}) → 𝑦𝑋)
220200, 219sylan2b 592 . . . . 5 ((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) → 𝑦𝑋)
221 heibor1.5 . . . . . . . . . . . 12 (𝜑𝐹 ∈ (Cau‘𝐷))
222 1zzd 12626 . . . . . . . . . . . . 13 (𝜑 → 1 ∈ ℤ)
223129, 4, 222iscau3 25250 . . . . . . . . . . . 12 (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋pm ℂ) ∧ ∀𝑦 ∈ ℝ+𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦))))
224221, 223mpbid 231 . . . . . . . . . . 11 (𝜑 → (𝐹 ∈ (𝑋pm ℂ) ∧ ∀𝑦 ∈ ℝ+𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦)))
225224simprd 494 . . . . . . . . . 10 (𝜑 → ∀𝑦 ∈ ℝ+𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦))
226 simp3 1135 . . . . . . . . . . . . 13 ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦) → ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦)
227226ralimi 3072 . . . . . . . . . . . 12 (∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦) → ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦)
228227reximi 3073 . . . . . . . . . . 11 (∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦) → ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦)
229228ralimi 3072 . . . . . . . . . 10 (∀𝑦 ∈ ℝ+𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦) → ∀𝑦 ∈ ℝ+𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦)
230225, 229syl 17 . . . . . . . . 9 (𝜑 → ∀𝑦 ∈ ℝ+𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦)
231230adantr 479 . . . . . . . 8 ((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) → ∀𝑦 ∈ ℝ+𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦)
232 rphalfcl 13036 . . . . . . . 8 (𝑟 ∈ ℝ+ → (𝑟 / 2) ∈ ℝ+)
233 breq2 5153 . . . . . . . . . . 11 (𝑦 = (𝑟 / 2) → (((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦 ↔ ((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2)))
2342332ralbidv 3208 . . . . . . . . . 10 (𝑦 = (𝑟 / 2) → (∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦 ↔ ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2)))
235234rexbidv 3168 . . . . . . . . 9 (𝑦 = (𝑟 / 2) → (∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦 ↔ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2)))
236235rspccva 3605 . . . . . . . 8 ((∀𝑦 ∈ ℝ+𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦 ∧ (𝑟 / 2) ∈ ℝ+) → ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2))
237231, 232, 236syl2an 594 . . . . . . 7 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ 𝑟 ∈ ℝ+) → ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2))
2389ffund 6727 . . . . . . . . . . . 12 (𝜑 → Fun 𝐹)
239238ad2antrr 724 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → Fun 𝐹)
2407ad2antrr 724 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → 𝐽 ∈ Top)
241 imassrn 6075 . . . . . . . . . . . . . 14 (𝐹 “ (ℤ𝑚)) ⊆ ran 𝐹
242241, 13sstrid 3988 . . . . . . . . . . . . 13 (𝜑 → (𝐹 “ (ℤ𝑚)) ⊆ 𝐽)
243242ad2antrr 724 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → (𝐹 “ (ℤ𝑚)) ⊆ 𝐽)
244 nnz 12612 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ → 𝑚 ∈ ℤ)
245 fnfvelrn 7089 . . . . . . . . . . . . . . 15 ((ℤ Fn ℤ ∧ 𝑚 ∈ ℤ) → (ℤ𝑚) ∈ ran ℤ)
24657, 244, 245sylancr 585 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ → (ℤ𝑚) ∈ ran ℤ)
247246ad2antll 727 . . . . . . . . . . . . 13 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → (ℤ𝑚) ∈ ran ℤ)
248 simplr 767 . . . . . . . . . . . . 13 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢)))
249 imaeq2 6060 . . . . . . . . . . . . . . . 16 (𝑢 = (ℤ𝑚) → (𝐹𝑢) = (𝐹 “ (ℤ𝑚)))
250249fveq2d 6900 . . . . . . . . . . . . . . 15 (𝑢 = (ℤ𝑚) → ((cls‘𝐽)‘(𝐹𝑢)) = ((cls‘𝐽)‘(𝐹 “ (ℤ𝑚))))
251250eleq2d 2811 . . . . . . . . . . . . . 14 (𝑢 = (ℤ𝑚) → (𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢)) ↔ 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ (ℤ𝑚)))))
252251rspcv 3602 . . . . . . . . . . . . 13 ((ℤ𝑚) ∈ ran ℤ → (∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢)) → 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ (ℤ𝑚)))))
253247, 248, 252sylc 65 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ (ℤ𝑚))))
2544ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → 𝐷 ∈ (∞Met‘𝑋))
255220adantr 479 . . . . . . . . . . . . 13 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → 𝑦𝑋)
256232ad2antrl 726 . . . . . . . . . . . . . 14 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → (𝑟 / 2) ∈ ℝ+)
257256rpxrd 13052 . . . . . . . . . . . . 13 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → (𝑟 / 2) ∈ ℝ*)
2585blopn 24453 . . . . . . . . . . . . 13 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦𝑋 ∧ (𝑟 / 2) ∈ ℝ*) → (𝑦(ball‘𝐷)(𝑟 / 2)) ∈ 𝐽)
259254, 255, 257, 258syl3anc 1368 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → (𝑦(ball‘𝐷)(𝑟 / 2)) ∈ 𝐽)
260 blcntr 24363 . . . . . . . . . . . . 13 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦𝑋 ∧ (𝑟 / 2) ∈ ℝ+) → 𝑦 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
261254, 255, 256, 260syl3anc 1368 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → 𝑦 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
26215clsndisj 23023 . . . . . . . . . . . 12 (((𝐽 ∈ Top ∧ (𝐹 “ (ℤ𝑚)) ⊆ 𝐽𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ (ℤ𝑚)))) ∧ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∈ 𝐽𝑦 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) → ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚))) ≠ ∅)
263240, 243, 253, 259, 261, 262syl32anc 1375 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚))) ≠ ∅)
264 n0 4346 . . . . . . . . . . . 12 (((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚))) ≠ ∅ ↔ ∃𝑛 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚))))
265 inss2 4228 . . . . . . . . . . . . . . . . 17 ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚))) ⊆ (𝐹 “ (ℤ𝑚))
266265sseli 3972 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚))) → 𝑛 ∈ (𝐹 “ (ℤ𝑚)))
267 fvelima 6963 . . . . . . . . . . . . . . . 16 ((Fun 𝐹𝑛 ∈ (𝐹 “ (ℤ𝑚))) → ∃𝑘 ∈ (ℤ𝑚)(𝐹𝑘) = 𝑛)
268266, 267sylan2 591 . . . . . . . . . . . . . . 15 ((Fun 𝐹𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚)))) → ∃𝑘 ∈ (ℤ𝑚)(𝐹𝑘) = 𝑛)
269 inss1 4227 . . . . . . . . . . . . . . . . . . 19 ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚))) ⊆ (𝑦(ball‘𝐷)(𝑟 / 2))
270269sseli 3972 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚))) → 𝑛 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
271270adantl 480 . . . . . . . . . . . . . . . . 17 ((Fun 𝐹𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚)))) → 𝑛 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
272 eleq1a 2820 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) → ((𝐹𝑘) = 𝑛 → (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
273271, 272syl 17 . . . . . . . . . . . . . . . 16 ((Fun 𝐹𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚)))) → ((𝐹𝑘) = 𝑛 → (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
274273reximdv 3159 . . . . . . . . . . . . . . 15 ((Fun 𝐹𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚)))) → (∃𝑘 ∈ (ℤ𝑚)(𝐹𝑘) = 𝑛 → ∃𝑘 ∈ (ℤ𝑚)(𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
275268, 274mpd 15 . . . . . . . . . . . . . 14 ((Fun 𝐹𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚)))) → ∃𝑘 ∈ (ℤ𝑚)(𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
276275ex 411 . . . . . . . . . . . . 13 (Fun 𝐹 → (𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚))) → ∃𝑘 ∈ (ℤ𝑚)(𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
277276exlimdv 1928 . . . . . . . . . . . 12 (Fun 𝐹 → (∃𝑛 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚))) → ∃𝑘 ∈ (ℤ𝑚)(𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
278264, 277biimtrid 241 . . . . . . . . . . 11 (Fun 𝐹 → (((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚))) ≠ ∅ → ∃𝑘 ∈ (ℤ𝑚)(𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
279239, 263, 278sylc 65 . . . . . . . . . 10 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → ∃𝑘 ∈ (ℤ𝑚)(𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
280 r19.29 3103 . . . . . . . . . . 11 ((∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) ∧ ∃𝑘 ∈ (ℤ𝑚)(𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ (ℤ𝑚)(∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
281 uznnssnn 12912 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ → (ℤ𝑚) ⊆ ℕ)
282281ad2antll 727 . . . . . . . . . . . . 13 (((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → (ℤ𝑚) ⊆ ℕ)
283 simprlr 778 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
2844ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → 𝐷 ∈ (∞Met‘𝑋))
285 simplrl 775 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → 𝑟 ∈ ℝ+)
286285, 232syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → (𝑟 / 2) ∈ ℝ+)
287286rpxrd 13052 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → (𝑟 / 2) ∈ ℝ*)
288 simpllr 774 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → 𝑦𝑋)
2899ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → 𝐹:ℕ⟶𝑋)
290 eluznn 12935 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑚 ∈ ℕ ∧ 𝑘 ∈ (ℤ𝑚)) → 𝑘 ∈ ℕ)
291290ad2ant2lr 746 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑟 ∈ ℝ+𝑚 ∈ ℕ) ∧ (𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) → 𝑘 ∈ ℕ)
292291ad2ant2lr 746 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → 𝑘 ∈ ℕ)
293289, 292ffvelcdmd 7094 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → (𝐹𝑘) ∈ 𝑋)
294 elbl3 24342 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑟 / 2) ∈ ℝ*) ∧ (𝑦𝑋 ∧ (𝐹𝑘) ∈ 𝑋)) → ((𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) ↔ ((𝐹𝑘)𝐷𝑦) < (𝑟 / 2)))
295284, 287, 288, 293, 294syl22anc 837 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → ((𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) ↔ ((𝐹𝑘)𝐷𝑦) < (𝑟 / 2)))
296283, 295mpbid 231 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → ((𝐹𝑘)𝐷𝑦) < (𝑟 / 2))
2972ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → 𝐷 ∈ (Met‘𝑋))
298 simprr 771 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → 𝑛 ∈ (ℤ𝑘))
299 eluznn 12935 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑘 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑘)) → 𝑛 ∈ ℕ)
300292, 298, 299syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → 𝑛 ∈ ℕ)
301289, 300ffvelcdmd 7094 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → (𝐹𝑛) ∈ 𝑋)
302 metcl 24282 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑛) ∈ 𝑋) → ((𝐹𝑘)𝐷(𝐹𝑛)) ∈ ℝ)
303297, 293, 301, 302syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → ((𝐹𝑘)𝐷(𝐹𝑛)) ∈ ℝ)
304 metcl 24282 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹𝑘) ∈ 𝑋𝑦𝑋) → ((𝐹𝑘)𝐷𝑦) ∈ ℝ)
305297, 293, 288, 304syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → ((𝐹𝑘)𝐷𝑦) ∈ ℝ)
306286rpred 13051 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → (𝑟 / 2) ∈ ℝ)
307 lt2add 11731 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐹𝑘)𝐷(𝐹𝑛)) ∈ ℝ ∧ ((𝐹𝑘)𝐷𝑦) ∈ ℝ) ∧ ((𝑟 / 2) ∈ ℝ ∧ (𝑟 / 2) ∈ ℝ)) → ((((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) ∧ ((𝐹𝑘)𝐷𝑦) < (𝑟 / 2)) → (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) < ((𝑟 / 2) + (𝑟 / 2))))
308303, 305, 306, 306, 307syl22anc 837 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → ((((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) ∧ ((𝐹𝑘)𝐷𝑦) < (𝑟 / 2)) → (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) < ((𝑟 / 2) + (𝑟 / 2))))
309296, 308mpan2d 692 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → (((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) → (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) < ((𝑟 / 2) + (𝑟 / 2))))
310285rpcnd 13053 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → 𝑟 ∈ ℂ)
3113102halvesd 12491 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → ((𝑟 / 2) + (𝑟 / 2)) = 𝑟)
312311breq2d 5161 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → ((((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) < ((𝑟 / 2) + (𝑟 / 2)) ↔ (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) < 𝑟))
313309, 312sylibd 238 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → (((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) → (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) < 𝑟))
314 mettri2 24291 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐷 ∈ (Met‘𝑋) ∧ ((𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑛) ∈ 𝑋𝑦𝑋)) → ((𝐹𝑛)𝐷𝑦) ≤ (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)))
315297, 293, 301, 288, 314syl13anc 1369 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → ((𝐹𝑛)𝐷𝑦) ≤ (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)))
316 metcl 24282 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹𝑛) ∈ 𝑋𝑦𝑋) → ((𝐹𝑛)𝐷𝑦) ∈ ℝ)
317297, 301, 288, 316syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → ((𝐹𝑛)𝐷𝑦) ∈ ℝ)
318303, 305readdcld 11275 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) ∈ ℝ)
319285rpred 13051 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → 𝑟 ∈ ℝ)
320 lelttr 11336 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑛)𝐷𝑦) ∈ ℝ ∧ (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) ∈ ℝ ∧ 𝑟 ∈ ℝ) → ((((𝐹𝑛)𝐷𝑦) ≤ (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) ∧ (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) < 𝑟) → ((𝐹𝑛)𝐷𝑦) < 𝑟))
321317, 318, 319, 320syl3anc 1368 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → ((((𝐹𝑛)𝐷𝑦) ≤ (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) ∧ (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) < 𝑟) → ((𝐹𝑛)𝐷𝑦) < 𝑟))
322315, 321mpand 693 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → ((((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) < 𝑟 → ((𝐹𝑛)𝐷𝑦) < 𝑟))
323313, 322syld 47 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → (((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) → ((𝐹𝑛)𝐷𝑦) < 𝑟))
324323anassrs 466 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ (𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) ∧ 𝑛 ∈ (ℤ𝑘)) → (((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) → ((𝐹𝑛)𝐷𝑦) < 𝑟))
325324ralimdva 3156 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ (𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) → (∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) → ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟))
326325expr 455 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ 𝑘 ∈ (ℤ𝑚)) → ((𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) → (∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) → ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟)))
327326com23 86 . . . . . . . . . . . . . . 15 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ 𝑘 ∈ (ℤ𝑚)) → (∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) → ((𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) → ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟)))
328327impd 409 . . . . . . . . . . . . . 14 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ 𝑘 ∈ (ℤ𝑚)) → ((∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟))
329328reximdva 3157 . . . . . . . . . . . . 13 (((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → (∃𝑘 ∈ (ℤ𝑚)(∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟))
330 ssrexv 4046 . . . . . . . . . . . . 13 ((ℤ𝑚) ⊆ ℕ → (∃𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟 → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟))
331282, 329, 330sylsyld 61 . . . . . . . . . . . 12 (((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → (∃𝑘 ∈ (ℤ𝑚)(∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟))
332220, 331syldanl 600 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → (∃𝑘 ∈ (ℤ𝑚)(∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟))
333280, 332syl5 34 . . . . . . . . . 10 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → ((∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) ∧ ∃𝑘 ∈ (ℤ𝑚)(𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟))
334279, 333mpan2d 692 . . . . . . . . 9 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → (∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟))
335334anassrs 466 . . . . . . . 8 ((((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ 𝑟 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) → (∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟))
336335rexlimdva 3144 . . . . . . 7 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ 𝑟 ∈ ℝ+) → (∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟))
337237, 336mpd 15 . . . . . 6 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ 𝑟 ∈ ℝ+) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟)
338337ralrimiva 3135 . . . . 5 ((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) → ∀𝑟 ∈ ℝ+𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟)
339 eqidd 2726 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) = (𝐹𝑛))
3405, 4, 129, 222, 339, 9lmmbrf 25234 . . . . . 6 (𝜑 → (𝐹(⇝𝑡𝐽)𝑦 ↔ (𝑦𝑋 ∧ ∀𝑟 ∈ ℝ+𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟)))
341340adantr 479 . . . . 5 ((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) → (𝐹(⇝𝑡𝐽)𝑦 ↔ (𝑦𝑋 ∧ ∀𝑟 ∈ ℝ+𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟)))
342220, 338, 341mpbir2and 711 . . . 4 ((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) → 𝐹(⇝𝑡𝐽)𝑦)
343200, 342sylan2br 593 . . 3 ((𝜑𝑦 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}) → 𝐹(⇝𝑡𝐽)𝑦)
344 releldm 5946 . . 3 ((Rel (⇝𝑡𝐽) ∧ 𝐹(⇝𝑡𝐽)𝑦) → 𝐹 ∈ dom (⇝𝑡𝐽))
345189, 343, 344sylancr 585 . 2 ((𝜑𝑦 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}) → 𝐹 ∈ dom (⇝𝑡𝐽))
346188, 345exlimddv 1930 1 (𝜑𝐹 ∈ dom (⇝𝑡𝐽))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  w3a 1084  wal 1531   = wceq 1533  wex 1773  wcel 2098  {cab 2702  wne 2929  wral 3050  wrex 3059  Vcvv 3461  cun 3942  cin 3943  wss 3944  c0 4322  𝒫 cpw 4604  {csn 4630   cuni 4909   cint 4950   class class class wbr 5149  dom cdm 5678  ran crn 5679  cima 5681  Rel wrel 5683  Fun wfun 6543   Fn wfn 6544  wf 6545  cfv 6549  (class class class)co 7419  pm cpm 8846  Fincfn 8964  ficfi 9435  cc 11138  cr 11139  0cc0 11140  1c1 11141   + caddc 11143  *cxr 11279   < clt 11280  cle 11281   / cdiv 11903  cn 12245  2c2 12300  cz 12591  cuz 12855  +crp 13009  ∞Metcxmet 21281  Metcmet 21282  ballcbl 21283  MetOpencmopn 21286  Topctop 22839  Clsdccld 22964  clsccl 22966  𝑡clm 23174  Compccmp 23334  Cauccau 25225
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-cnex 11196  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-mulcom 11204  ax-addass 11205  ax-mulass 11206  ax-distr 11207  ax-i2m1 11208  ax-1ne0 11209  ax-1rid 11210  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213  ax-pre-lttri 11214  ax-pre-lttrn 11215  ax-pre-ltadd 11216  ax-pre-mulgt0 11217  ax-pre-sup 11218
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-int 4951  df-iun 4999  df-iin 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7872  df-1st 7994  df-2nd 7995  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-er 8725  df-map 8847  df-pm 8848  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-fi 9436  df-sup 9467  df-inf 9468  df-pnf 11282  df-mnf 11283  df-xr 11284  df-ltxr 11285  df-le 11286  df-sub 11478  df-neg 11479  df-div 11904  df-nn 12246  df-2 12308  df-n0 12506  df-z 12592  df-uz 12856  df-q 12966  df-rp 13010  df-xneg 13127  df-xadd 13128  df-xmul 13129  df-topgen 17428  df-psmet 21288  df-xmet 21289  df-met 21290  df-bl 21291  df-mopn 21292  df-top 22840  df-topon 22857  df-bases 22893  df-cld 22967  df-ntr 22968  df-cls 22969  df-lm 23177  df-cmp 23335  df-cau 25228
This theorem is referenced by:  heibor1  37411
  Copyright terms: Public domain W3C validator