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 34968
Description: Lemma for heibor1 34969. 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 22871 . . . . . . . . . 10 (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
42, 3syl 17 . . . . . . . . 9 (𝜑𝐷 ∈ (∞Met‘𝑋))
5 heibor.1 . . . . . . . . . 10 𝐽 = (MetOpen‘𝐷)
65mopntop 22977 . . . . . . . . 9 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
74, 6syl 17 . . . . . . . 8 (𝜑𝐽 ∈ Top)
8 imassrn 5933 . . . . . . . . 9 (𝐹𝑢) ⊆ ran 𝐹
9 heibor1.6 . . . . . . . . . . 11 (𝜑𝐹:ℕ⟶𝑋)
109frnd 6514 . . . . . . . . . 10 (𝜑 → ran 𝐹𝑋)
115mopnuni 22978 . . . . . . . . . . 11 (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = 𝐽)
124, 11syl 17 . . . . . . . . . 10 (𝜑𝑋 = 𝐽)
1310, 12sseqtrd 4004 . . . . . . . . 9 (𝜑 → ran 𝐹 𝐽)
148, 13sstrid 3975 . . . . . . . 8 (𝜑 → (𝐹𝑢) ⊆ 𝐽)
15 eqid 2818 . . . . . . . . 9 𝐽 = 𝐽
1615clscld 21583 . . . . . . . 8 ((𝐽 ∈ Top ∧ (𝐹𝑢) ⊆ 𝐽) → ((cls‘𝐽)‘(𝐹𝑢)) ∈ (Clsd‘𝐽))
177, 14, 16syl2anc 584 . . . . . . 7 (𝜑 → ((cls‘𝐽)‘(𝐹𝑢)) ∈ (Clsd‘𝐽))
18 eleq1a 2905 . . . . . . 7 (((cls‘𝐽)‘(𝐹𝑢)) ∈ (Clsd‘𝐽) → (𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑘 ∈ (Clsd‘𝐽)))
1917, 18syl 17 . . . . . 6 (𝜑 → (𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑘 ∈ (Clsd‘𝐽)))
2019rexlimdvw 3287 . . . . 5 (𝜑 → (∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑘 ∈ (Clsd‘𝐽)))
2120abssdv 4042 . . . 4 (𝜑 → {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ⊆ (Clsd‘𝐽))
22 fvex 6676 . . . . 5 (Clsd‘𝐽) ∈ V
2322elpw2 5239 . . . 4 ({𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∈ 𝒫 (Clsd‘𝐽) ↔ {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ⊆ (Clsd‘𝐽))
2421, 23sylibr 235 . . 3 (𝜑 → {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∈ 𝒫 (Clsd‘𝐽))
25 elin 4166 . . . . . . 7 (𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∩ Fin) ↔ (𝑟 ∈ 𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∧ 𝑟 ∈ Fin))
26 velpw 4543 . . . . . . . . 9 (𝑟 ∈ 𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ↔ 𝑟 ⊆ {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))})
27 ssabral 4039 . . . . . . . . 9 (𝑟 ⊆ {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ↔ ∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)))
2826, 27bitri 276 . . . . . . . 8 (𝑟 ∈ 𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ↔ ∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)))
2928anbi1i 623 . . . . . . 7 ((𝑟 ∈ 𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∧ 𝑟 ∈ Fin) ↔ (∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ 𝑟 ∈ Fin))
3025, 29bitri 276 . . . . . 6 (𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∩ Fin) ↔ (∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ 𝑟 ∈ Fin))
31 raleq 3403 . . . . . . . . . . . . . 14 (𝑚 = ∅ → (∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ↔ ∀𝑘 ∈ ∅ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))))
3231anbi2d 628 . . . . . . . . . . . . 13 (𝑚 = ∅ → ((𝜑 ∧ ∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) ↔ (𝜑 ∧ ∀𝑘 ∈ ∅ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)))))
33 inteq 4870 . . . . . . . . . . . . . . 15 (𝑚 = ∅ → 𝑚 = ∅)
3433sseq2d 3996 . . . . . . . . . . . . . 14 (𝑚 = ∅ → ((𝐹𝑘) ⊆ 𝑚 ↔ (𝐹𝑘) ⊆ ∅))
3534rexbidv 3294 . . . . . . . . . . . . 13 (𝑚 = ∅ → (∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑚 ↔ ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ ∅))
3632, 35imbi12d 346 . . . . . . . . . . . 12 (𝑚 = ∅ → (((𝜑 ∧ ∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑚) ↔ ((𝜑 ∧ ∀𝑘 ∈ ∅ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ ∅)))
37 raleq 3403 . . . . . . . . . . . . . 14 (𝑚 = 𝑦 → (∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ↔ ∀𝑘𝑦𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))))
3837anbi2d 628 . . . . . . . . . . . . 13 (𝑚 = 𝑦 → ((𝜑 ∧ ∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) ↔ (𝜑 ∧ ∀𝑘𝑦𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)))))
39 inteq 4870 . . . . . . . . . . . . . . 15 (𝑚 = 𝑦 𝑚 = 𝑦)
4039sseq2d 3996 . . . . . . . . . . . . . 14 (𝑚 = 𝑦 → ((𝐹𝑘) ⊆ 𝑚 ↔ (𝐹𝑘) ⊆ 𝑦))
4140rexbidv 3294 . . . . . . . . . . . . 13 (𝑚 = 𝑦 → (∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑚 ↔ ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑦))
4238, 41imbi12d 346 . . . . . . . . . . . 12 (𝑚 = 𝑦 → (((𝜑 ∧ ∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑚) ↔ ((𝜑 ∧ ∀𝑘𝑦𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑦)))
43 raleq 3403 . . . . . . . . . . . . . 14 (𝑚 = (𝑦 ∪ {𝑛}) → (∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ↔ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))))
4443anbi2d 628 . . . . . . . . . . . . 13 (𝑚 = (𝑦 ∪ {𝑛}) → ((𝜑 ∧ ∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) ↔ (𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)))))
45 inteq 4870 . . . . . . . . . . . . . . 15 (𝑚 = (𝑦 ∪ {𝑛}) → 𝑚 = (𝑦 ∪ {𝑛}))
4645sseq2d 3996 . . . . . . . . . . . . . 14 (𝑚 = (𝑦 ∪ {𝑛}) → ((𝐹𝑘) ⊆ 𝑚 ↔ (𝐹𝑘) ⊆ (𝑦 ∪ {𝑛})))
4746rexbidv 3294 . . . . . . . . . . . . 13 (𝑚 = (𝑦 ∪ {𝑛}) → (∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑚 ↔ ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ (𝑦 ∪ {𝑛})))
4844, 47imbi12d 346 . . . . . . . . . . . 12 (𝑚 = (𝑦 ∪ {𝑛}) → (((𝜑 ∧ ∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑚) ↔ ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ (𝑦 ∪ {𝑛}))))
49 raleq 3403 . . . . . . . . . . . . . 14 (𝑚 = 𝑟 → (∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ↔ ∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))))
5049anbi2d 628 . . . . . . . . . . . . 13 (𝑚 = 𝑟 → ((𝜑 ∧ ∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) ↔ (𝜑 ∧ ∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)))))
51 inteq 4870 . . . . . . . . . . . . . . 15 (𝑚 = 𝑟 𝑚 = 𝑟)
5251sseq2d 3996 . . . . . . . . . . . . . 14 (𝑚 = 𝑟 → ((𝐹𝑘) ⊆ 𝑚 ↔ (𝐹𝑘) ⊆ 𝑟))
5352rexbidv 3294 . . . . . . . . . . . . 13 (𝑚 = 𝑟 → (∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑚 ↔ ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑟))
5450, 53imbi12d 346 . . . . . . . . . . . 12 (𝑚 = 𝑟 → (((𝜑 ∧ ∀𝑘𝑚𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑚) ↔ ((𝜑 ∧ ∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑟)))
55 uzf 12234 . . . . . . . . . . . . . . . 16 :ℤ⟶𝒫 ℤ
56 ffn 6507 . . . . . . . . . . . . . . . 16 (ℤ:ℤ⟶𝒫 ℤ → ℤ Fn ℤ)
5755, 56ax-mp 5 . . . . . . . . . . . . . . 15 Fn ℤ
58 0z 11980 . . . . . . . . . . . . . . 15 0 ∈ ℤ
59 fnfvelrn 6840 . . . . . . . . . . . . . . 15 ((ℤ Fn ℤ ∧ 0 ∈ ℤ) → (ℤ‘0) ∈ ran ℤ)
6057, 58, 59mp2an 688 . . . . . . . . . . . . . 14 (ℤ‘0) ∈ ran ℤ
61 ssv 3988 . . . . . . . . . . . . . . 15 (𝐹 “ (ℤ‘0)) ⊆ V
62 int0 4881 . . . . . . . . . . . . . . 15 ∅ = V
6361, 62sseqtrri 4001 . . . . . . . . . . . . . 14 (𝐹 “ (ℤ‘0)) ⊆
64 imaeq2 5918 . . . . . . . . . . . . . . . 16 (𝑘 = (ℤ‘0) → (𝐹𝑘) = (𝐹 “ (ℤ‘0)))
6564sseq1d 3995 . . . . . . . . . . . . . . 15 (𝑘 = (ℤ‘0) → ((𝐹𝑘) ⊆ ∅ ↔ (𝐹 “ (ℤ‘0)) ⊆ ∅))
6665rspcev 3620 . . . . . . . . . . . . . 14 (((ℤ‘0) ∈ ran ℤ ∧ (𝐹 “ (ℤ‘0)) ⊆ ∅) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ ∅)
6760, 63, 66mp2an 688 . . . . . . . . . . . . 13 𝑘 ∈ ran ℤ(𝐹𝑘) ⊆
6867a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ ∀𝑘 ∈ ∅ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ ∅)
69 ssun1 4145 . . . . . . . . . . . . . . . . 17 𝑦 ⊆ (𝑦 ∪ {𝑛})
70 ssralv 4030 . . . . . . . . . . . . . . . . 17 (𝑦 ⊆ (𝑦 ∪ {𝑛}) → (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → ∀𝑘𝑦𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))))
7169, 70ax-mp 5 . . . . . . . . . . . . . . . 16 (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → ∀𝑘𝑦𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)))
7271anim2i 616 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → (𝜑 ∧ ∀𝑘𝑦𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))))
7372imim1i 63 . . . . . . . . . . . . . 14 (((𝜑 ∧ ∀𝑘𝑦𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑦) → ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑦))
74 ssun2 4146 . . . . . . . . . . . . . . . . . 18 {𝑛} ⊆ (𝑦 ∪ {𝑛})
75 ssralv 4030 . . . . . . . . . . . . . . . . . 18 ({𝑛} ⊆ (𝑦 ∪ {𝑛}) → (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → ∀𝑘 ∈ {𝑛}∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))))
7674, 75ax-mp 5 . . . . . . . . . . . . . . . . 17 (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → ∀𝑘 ∈ {𝑛}∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)))
77 vex 3495 . . . . . . . . . . . . . . . . . 18 𝑛 ∈ V
78 eqeq1 2822 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑛 → (𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ↔ 𝑛 = ((cls‘𝐽)‘(𝐹𝑢))))
7978rexbidv 3294 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑛 → (∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ↔ ∃𝑢 ∈ ran ℤ𝑛 = ((cls‘𝐽)‘(𝐹𝑢))))
8077, 79ralsn 4611 . . . . . . . . . . . . . . . . 17 (∀𝑘 ∈ {𝑛}∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ↔ ∃𝑢 ∈ ran ℤ𝑛 = ((cls‘𝐽)‘(𝐹𝑢)))
8176, 80sylib 219 . . . . . . . . . . . . . . . 16 (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → ∃𝑢 ∈ ran ℤ𝑛 = ((cls‘𝐽)‘(𝐹𝑢)))
82 uzin2 14692 . . . . . . . . . . . . . . . . . . . 20 ((𝑢 ∈ ran ℤ𝑘 ∈ ran ℤ) → (𝑢𝑘) ∈ ran ℤ)
838, 10sstrid 3975 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐹𝑢) ⊆ 𝑋)
8483, 12sseqtrd 4004 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐹𝑢) ⊆ 𝐽)
8515sscls 21592 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐽 ∈ Top ∧ (𝐹𝑢) ⊆ 𝐽) → (𝐹𝑢) ⊆ ((cls‘𝐽)‘(𝐹𝑢)))
867, 84, 85syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐹𝑢) ⊆ ((cls‘𝐽)‘(𝐹𝑢)))
87 sseq2 3990 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = ((cls‘𝐽)‘(𝐹𝑢)) → ((𝐹𝑢) ⊆ 𝑛 ↔ (𝐹𝑢) ⊆ ((cls‘𝐽)‘(𝐹𝑢))))
8886, 87syl5ibrcom 248 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑛 = ((cls‘𝐽)‘(𝐹𝑢)) → (𝐹𝑢) ⊆ 𝑛))
89 inss2 4203 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑢𝑘) ⊆ 𝑘
90 inss1 4202 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑢𝑘) ⊆ 𝑢
91 imass2 5958 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑢𝑘) ⊆ 𝑘 → (𝐹 “ (𝑢𝑘)) ⊆ (𝐹𝑘))
92 imass2 5958 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑢𝑘) ⊆ 𝑢 → (𝐹 “ (𝑢𝑘)) ⊆ (𝐹𝑢))
9391, 92anim12i 612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑢𝑘) ⊆ 𝑘 ∧ (𝑢𝑘) ⊆ 𝑢) → ((𝐹 “ (𝑢𝑘)) ⊆ (𝐹𝑘) ∧ (𝐹 “ (𝑢𝑘)) ⊆ (𝐹𝑢)))
94 ssin 4204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐹 “ (𝑢𝑘)) ⊆ (𝐹𝑘) ∧ (𝐹 “ (𝑢𝑘)) ⊆ (𝐹𝑢)) ↔ (𝐹 “ (𝑢𝑘)) ⊆ ((𝐹𝑘) ∩ (𝐹𝑢)))
9593, 94sylib 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑢𝑘) ⊆ 𝑘 ∧ (𝑢𝑘) ⊆ 𝑢) → (𝐹 “ (𝑢𝑘)) ⊆ ((𝐹𝑘) ∩ (𝐹𝑢)))
9689, 90, 95mp2an 688 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹 “ (𝑢𝑘)) ⊆ ((𝐹𝑘) ∩ (𝐹𝑢))
97 ss2in 4210 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐹𝑘) ⊆ 𝑦 ∧ (𝐹𝑢) ⊆ 𝑛) → ((𝐹𝑘) ∩ (𝐹𝑢)) ⊆ ( 𝑦𝑛))
9896, 97sstrid 3975 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐹𝑘) ⊆ 𝑦 ∧ (𝐹𝑢) ⊆ 𝑛) → (𝐹 “ (𝑢𝑘)) ⊆ ( 𝑦𝑛))
9977intunsn 4906 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∪ {𝑛}) = ( 𝑦𝑛)
10098, 99sseqtrrdi 4015 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹𝑘) ⊆ 𝑦 ∧ (𝐹𝑢) ⊆ 𝑛) → (𝐹 “ (𝑢𝑘)) ⊆ (𝑦 ∪ {𝑛}))
101100expcom 414 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹𝑢) ⊆ 𝑛 → ((𝐹𝑘) ⊆ 𝑦 → (𝐹 “ (𝑢𝑘)) ⊆ (𝑦 ∪ {𝑛})))
10288, 101syl6 35 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑛 = ((cls‘𝐽)‘(𝐹𝑢)) → ((𝐹𝑘) ⊆ 𝑦 → (𝐹 “ (𝑢𝑘)) ⊆ (𝑦 ∪ {𝑛}))))
103102impd 411 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝑛 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ (𝐹𝑘) ⊆ 𝑦) → (𝐹 “ (𝑢𝑘)) ⊆ (𝑦 ∪ {𝑛})))
104 imaeq2 5918 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚 = (𝑢𝑘) → (𝐹𝑚) = (𝐹 “ (𝑢𝑘)))
105104sseq1d 3995 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 = (𝑢𝑘) → ((𝐹𝑚) ⊆ (𝑦 ∪ {𝑛}) ↔ (𝐹 “ (𝑢𝑘)) ⊆ (𝑦 ∪ {𝑛})))
106105rspcev 3620 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑢𝑘) ∈ ran ℤ ∧ (𝐹 “ (𝑢𝑘)) ⊆ (𝑦 ∪ {𝑛})) → ∃𝑚 ∈ ran ℤ(𝐹𝑚) ⊆ (𝑦 ∪ {𝑛}))
107106expcom 414 . . . . . . . . . . . . . . . . . . . . . 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 3290 . . . . . . . . . . . . . . . . . 18 (𝜑 → (∃𝑢 ∈ ran ℤ𝑘 ∈ ran ℤ(𝑛 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ (𝐹𝑘) ⊆ 𝑦) → ∃𝑚 ∈ ran ℤ(𝐹𝑚) ⊆ (𝑦 ∪ {𝑛})))
112 reeanv 3365 . . . . . . . . . . . . . . . . . 18 (∃𝑢 ∈ ran ℤ𝑘 ∈ ran ℤ(𝑛 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ (𝐹𝑘) ⊆ 𝑦) ↔ (∃𝑢 ∈ ran ℤ𝑛 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑦))
113 imaeq2 5918 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑘 → (𝐹𝑚) = (𝐹𝑘))
114113sseq1d 3995 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑘 → ((𝐹𝑚) ⊆ (𝑦 ∪ {𝑛}) ↔ (𝐹𝑘) ⊆ (𝑦 ∪ {𝑛})))
115114cbvrexvw 3448 . . . . . . . . . . . . . . . . . 18 (∃𝑚 ∈ ran ℤ(𝐹𝑚) ⊆ (𝑦 ∪ {𝑛}) ↔ ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ (𝑦 ∪ {𝑛}))
116111, 112, 1153imtr3g 296 . . . . . . . . . . . . . . . . 17 (𝜑 → ((∃𝑢 ∈ ran ℤ𝑛 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑦) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ (𝑦 ∪ {𝑛})))
117116expd 416 . . . . . . . . . . . . . . . 16 (𝜑 → (∃𝑢 ∈ ran ℤ𝑛 = ((cls‘𝐽)‘(𝐹𝑢)) → (∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑦 → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ (𝑦 ∪ {𝑛}))))
11881, 117syl5 34 . . . . . . . . . . . . . . 15 (𝜑 → (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → (∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑦 → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ (𝑦 ∪ {𝑛}))))
119118imp 407 . . . . . . . . . . . . . 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 8746 . . . . . . . . . . 11 (𝑟 ∈ Fin → ((𝜑 ∧ ∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑟))
123122com12 32 . . . . . . . . . 10 ((𝜑 ∧ ∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))) → (𝑟 ∈ Fin → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑟))
124123impr 455 . . . . . . . . 9 ((𝜑 ∧ (∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ 𝑟 ∈ Fin)) → ∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑟)
1259ffnd 6508 . . . . . . . . . . 11 (𝜑𝐹 Fn ℕ)
126 inss1 4202 . . . . . . . . . . . . . . 15 (𝑘 ∩ ℕ) ⊆ 𝑘
127 imass2 5958 . . . . . . . . . . . . . . 15 ((𝑘 ∩ ℕ) ⊆ 𝑘 → (𝐹 “ (𝑘 ∩ ℕ)) ⊆ (𝐹𝑘))
128126, 127ax-mp 5 . . . . . . . . . . . . . 14 (𝐹 “ (𝑘 ∩ ℕ)) ⊆ (𝐹𝑘)
129 nnuz 12269 . . . . . . . . . . . . . . . . . . . 20 ℕ = (ℤ‘1)
130 1z 12000 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℤ
131 fnfvelrn 6840 . . . . . . . . . . . . . . . . . . . . 21 ((ℤ Fn ℤ ∧ 1 ∈ ℤ) → (ℤ‘1) ∈ ran ℤ)
13257, 130, 131mp2an 688 . . . . . . . . . . . . . . . . . . . 20 (ℤ‘1) ∈ ran ℤ
133129, 132eqeltri 2906 . . . . . . . . . . . . . . . . . . 19 ℕ ∈ ran ℤ
134 uzin2 14692 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ran ℤ ∧ ℕ ∈ ran ℤ) → (𝑘 ∩ ℕ) ∈ ran ℤ)
135133, 134mpan2 687 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ran ℤ → (𝑘 ∩ ℕ) ∈ ran ℤ)
136 uzn0 12248 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∩ ℕ) ∈ ran ℤ → (𝑘 ∩ ℕ) ≠ ∅)
137135, 136syl 17 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ran ℤ → (𝑘 ∩ ℕ) ≠ ∅)
138 n0 4307 . . . . . . . . . . . . . . . . 17 ((𝑘 ∩ ℕ) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝑘 ∩ ℕ))
139137, 138sylib 219 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ran ℤ → ∃𝑦 𝑦 ∈ (𝑘 ∩ ℕ))
140 fnfun 6446 . . . . . . . . . . . . . . . . . . 19 (𝐹 Fn ℕ → Fun 𝐹)
141 inss2 4203 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∩ ℕ) ⊆ ℕ
142 fndm 6448 . . . . . . . . . . . . . . . . . . . 20 (𝐹 Fn ℕ → dom 𝐹 = ℕ)
143141, 142sseqtrrid 4017 . . . . . . . . . . . . . . . . . . 19 (𝐹 Fn ℕ → (𝑘 ∩ ℕ) ⊆ dom 𝐹)
144 funfvima2 6984 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝐹 ∧ (𝑘 ∩ ℕ) ⊆ dom 𝐹) → (𝑦 ∈ (𝑘 ∩ ℕ) → (𝐹𝑦) ∈ (𝐹 “ (𝑘 ∩ ℕ))))
145140, 143, 144syl2anc 584 . . . . . . . . . . . . . . . . . 18 (𝐹 Fn ℕ → (𝑦 ∈ (𝑘 ∩ ℕ) → (𝐹𝑦) ∈ (𝐹 “ (𝑘 ∩ ℕ))))
146 ne0i 4297 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑦) ∈ (𝐹 “ (𝑘 ∩ ℕ)) → (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅)
147145, 146syl6 35 . . . . . . . . . . . . . . . . 17 (𝐹 Fn ℕ → (𝑦 ∈ (𝑘 ∩ ℕ) → (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅))
148147exlimdv 1925 . . . . . . . . . . . . . . . 16 (𝐹 Fn ℕ → (∃𝑦 𝑦 ∈ (𝑘 ∩ ℕ) → (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅))
149139, 148syl5 34 . . . . . . . . . . . . . . 15 (𝐹 Fn ℕ → (𝑘 ∈ ran ℤ → (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅))
150149imp 407 . . . . . . . . . . . . . 14 ((𝐹 Fn ℕ ∧ 𝑘 ∈ ran ℤ) → (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅)
151 ssn0 4351 . . . . . . . . . . . . . 14 (((𝐹 “ (𝑘 ∩ ℕ)) ⊆ (𝐹𝑘) ∧ (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅) → (𝐹𝑘) ≠ ∅)
152128, 150, 151sylancr 587 . . . . . . . . . . . . 13 ((𝐹 Fn ℕ ∧ 𝑘 ∈ ran ℤ) → (𝐹𝑘) ≠ ∅)
153 ssn0 4351 . . . . . . . . . . . . . 14 (((𝐹𝑘) ⊆ 𝑟 ∧ (𝐹𝑘) ≠ ∅) → 𝑟 ≠ ∅)
154153expcom 414 . . . . . . . . . . . . 13 ((𝐹𝑘) ≠ ∅ → ((𝐹𝑘) ⊆ 𝑟 𝑟 ≠ ∅))
155152, 154syl 17 . . . . . . . . . . . 12 ((𝐹 Fn ℕ ∧ 𝑘 ∈ ran ℤ) → ((𝐹𝑘) ⊆ 𝑟 𝑟 ≠ ∅))
156155rexlimdva 3281 . . . . . . . . . . 11 (𝐹 Fn ℕ → (∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑟 𝑟 ≠ ∅))
157125, 156syl 17 . . . . . . . . . 10 (𝜑 → (∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑟 𝑟 ≠ ∅))
158157adantr 481 . . . . . . . . 9 ((𝜑 ∧ (∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ 𝑟 ∈ Fin)) → (∃𝑘 ∈ ran ℤ(𝐹𝑘) ⊆ 𝑟 𝑟 ≠ ∅))
159124, 158mpd 15 . . . . . . . 8 ((𝜑 ∧ (∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ 𝑟 ∈ Fin)) → 𝑟 ≠ ∅)
160159necomd 3068 . . . . . . 7 ((𝜑 ∧ (∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ 𝑟 ∈ Fin)) → ∅ ≠ 𝑟)
161160neneqd 3018 . . . . . 6 ((𝜑 ∧ (∀𝑘𝑟𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ∧ 𝑟 ∈ Fin)) → ¬ ∅ = 𝑟)
16230, 161sylan2b 593 . . . . 5 ((𝜑𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∩ Fin)) → ¬ ∅ = 𝑟)
163162nrexdv 3267 . . . 4 (𝜑 → ¬ ∃𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∩ Fin)∅ = 𝑟)
164 0ex 5202 . . . . 5 ∅ ∈ V
165 zex 11978 . . . . . . . 8 ℤ ∈ V
166165pwex 5272 . . . . . . 7 𝒫 ℤ ∈ V
167 frn 6513 . . . . . . . 8 (ℤ:ℤ⟶𝒫 ℤ → ran ℤ ⊆ 𝒫 ℤ)
16855, 167ax-mp 5 . . . . . . 7 ran ℤ ⊆ 𝒫 ℤ
169166, 168ssexi 5217 . . . . . 6 ran ℤ ∈ V
170169abrexex 7652 . . . . 5 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∈ V
171 elfi 8865 . . . . 5 ((∅ ∈ V ∧ {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∈ V) → (∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}) ↔ ∃𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∩ Fin)∅ = 𝑟))
172164, 170, 171mp2an 688 . . . 4 (∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}) ↔ ∃𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ∩ Fin)∅ = 𝑟)
173163, 172sylnibr 330 . . 3 (𝜑 → ¬ ∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}))
174 cmptop 21931 . . . . . 6 (𝐽 ∈ Comp → 𝐽 ∈ Top)
175 cmpfi 21944 . . . . . 6 (𝐽 ∈ Top → (𝐽 ∈ Comp ↔ ∀𝑚 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑚) → 𝑚 ≠ ∅)))
176174, 175syl 17 . . . . 5 (𝐽 ∈ Comp → (𝐽 ∈ Comp ↔ ∀𝑚 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑚) → 𝑚 ≠ ∅)))
177176ibi 268 . . . 4 (𝐽 ∈ Comp → ∀𝑚 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑚) → 𝑚 ≠ ∅))
178 fveq2 6663 . . . . . . . 8 (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} → (fi‘𝑚) = (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}))
179178eleq2d 2895 . . . . . . 7 (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} → (∅ ∈ (fi‘𝑚) ↔ ∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))})))
180179notbid 319 . . . . . 6 (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} → (¬ ∅ ∈ (fi‘𝑚) ↔ ¬ ∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))})))
181 inteq 4870 . . . . . . . 8 (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} → 𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))})
182181neeq1d 3072 . . . . . . 7 (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} → ( 𝑚 ≠ ∅ ↔ {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ≠ ∅))
183 n0 4307 . . . . . . 7 ( {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ≠ ∅ ↔ ∃𝑦 𝑦 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))})
184182, 183syl6bb 288 . . . . . 6 (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} → ( 𝑚 ≠ ∅ ↔ ∃𝑦 𝑦 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}))
185180, 184imbi12d 346 . . . . 5 (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} → ((¬ ∅ ∈ (fi‘𝑚) → 𝑚 ≠ ∅) ↔ (¬ ∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}) → ∃𝑦 𝑦 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))})))
186185rspccv 3617 . . . 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 21766 . . 3 Rel (⇝𝑡𝐽)
190 r19.23v 3276 . . . . . 6 (∀𝑢 ∈ ran ℤ(𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑦𝑘) ↔ (∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑦𝑘))
191190albii 1811 . . . . 5 (∀𝑘𝑢 ∈ ran ℤ(𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑦𝑘) ↔ ∀𝑘(∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑦𝑘))
192 fvex 6676 . . . . . . . 8 ((cls‘𝐽)‘(𝐹𝑢)) ∈ V
193 eleq2 2898 . . . . . . . 8 (𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → (𝑦𝑘𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))))
194192, 193ceqsalv 3530 . . . . . . 7 (∀𝑘(𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑦𝑘) ↔ 𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢)))
195194ralbii 3162 . . . . . 6 (∀𝑢 ∈ ran ℤ𝑘(𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑦𝑘) ↔ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢)))
196 ralcom4 3232 . . . . . 6 (∀𝑢 ∈ ran ℤ𝑘(𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑦𝑘) ↔ ∀𝑘𝑢 ∈ ran ℤ(𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑦𝑘))
197195, 196bitr3i 278 . . . . 5 (∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢)) ↔ ∀𝑘𝑢 ∈ ran ℤ(𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑦𝑘))
198 vex 3495 . . . . . 6 𝑦 ∈ V
199198elintab 4878 . . . . 5 (𝑦 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ↔ ∀𝑘(∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) → 𝑦𝑘))
200191, 197, 1993bitr4i 304 . . . 4 (∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢)) ↔ 𝑦 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))})
201 eqid 2818 . . . . . . . . . . 11 ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ ℕ))
202 imaeq2 5918 . . . . . . . . . . . . 13 (𝑢 = ℕ → (𝐹𝑢) = (𝐹 “ ℕ))
203202fveq2d 6667 . . . . . . . . . . . 12 (𝑢 = ℕ → ((cls‘𝐽)‘(𝐹𝑢)) = ((cls‘𝐽)‘(𝐹 “ ℕ)))
204203rspceeqv 3635 . . . . . . . . . . 11 ((ℕ ∈ ran ℤ ∧ ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ ℕ))) → ∃𝑢 ∈ ran ℤ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹𝑢)))
205133, 201, 204mp2an 688 . . . . . . . . . 10 𝑢 ∈ ran ℤ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹𝑢))
206 fvex 6676 . . . . . . . . . . 11 ((cls‘𝐽)‘(𝐹 “ ℕ)) ∈ V
207 eqeq1 2822 . . . . . . . . . . . 12 (𝑘 = ((cls‘𝐽)‘(𝐹 “ ℕ)) → (𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ↔ ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹𝑢))))
208207rexbidv 3294 . . . . . . . . . . 11 (𝑘 = ((cls‘𝐽)‘(𝐹 “ ℕ)) → (∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢)) ↔ ∃𝑢 ∈ ran ℤ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹𝑢))))
209206, 208elab 3664 . . . . . . . . . 10 (((cls‘𝐽)‘(𝐹 “ ℕ)) ∈ {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ↔ ∃𝑢 ∈ ran ℤ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹𝑢)))
210205, 209mpbir 232 . . . . . . . . 9 ((cls‘𝐽)‘(𝐹 “ ℕ)) ∈ {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}
211 intss1 4882 . . . . . . . . 9 (((cls‘𝐽)‘(𝐹 “ ℕ)) ∈ {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} → {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ⊆ ((cls‘𝐽)‘(𝐹 “ ℕ)))
212210, 211ax-mp 5 . . . . . . . 8 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ⊆ ((cls‘𝐽)‘(𝐹 “ ℕ))
213 imassrn 5933 . . . . . . . . . . 11 (𝐹 “ ℕ) ⊆ ran 𝐹
214213, 13sstrid 3975 . . . . . . . . . 10 (𝜑 → (𝐹 “ ℕ) ⊆ 𝐽)
21515clsss3 21595 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ (𝐹 “ ℕ) ⊆ 𝐽) → ((cls‘𝐽)‘(𝐹 “ ℕ)) ⊆ 𝐽)
2167, 214, 215syl2anc 584 . . . . . . . . 9 (𝜑 → ((cls‘𝐽)‘(𝐹 “ ℕ)) ⊆ 𝐽)
217216, 12sseqtrrd 4005 . . . . . . . 8 (𝜑 → ((cls‘𝐽)‘(𝐹 “ ℕ)) ⊆ 𝑋)
218212, 217sstrid 3975 . . . . . . 7 (𝜑 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))} ⊆ 𝑋)
219218sselda 3964 . . . . . 6 ((𝜑𝑦 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}) → 𝑦𝑋)
220200, 219sylan2b 593 . . . . 5 ((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) → 𝑦𝑋)
221 heibor1.5 . . . . . . . . . . . 12 (𝜑𝐹 ∈ (Cau‘𝐷))
222 1zzd 12001 . . . . . . . . . . . . 13 (𝜑 → 1 ∈ ℤ)
223129, 4, 222iscau3 23808 . . . . . . . . . . . 12 (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋pm ℂ) ∧ ∀𝑦 ∈ ℝ+𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦))))
224221, 223mpbid 233 . . . . . . . . . . 11 (𝜑 → (𝐹 ∈ (𝑋pm ℂ) ∧ ∀𝑦 ∈ ℝ+𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦)))
225224simprd 496 . . . . . . . . . 10 (𝜑 → ∀𝑦 ∈ ℝ+𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦))
226 simp3 1130 . . . . . . . . . . . . 13 ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦) → ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦)
227226ralimi 3157 . . . . . . . . . . . 12 (∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦) → ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦)
228227reximi 3240 . . . . . . . . . . 11 (∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦) → ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦)
229228ralimi 3157 . . . . . . . . . 10 (∀𝑦 ∈ ℝ+𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦) → ∀𝑦 ∈ ℝ+𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦)
230225, 229syl 17 . . . . . . . . 9 (𝜑 → ∀𝑦 ∈ ℝ+𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦)
231230adantr 481 . . . . . . . 8 ((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) → ∀𝑦 ∈ ℝ+𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦)
232 rphalfcl 12404 . . . . . . . 8 (𝑟 ∈ ℝ+ → (𝑟 / 2) ∈ ℝ+)
233 breq2 5061 . . . . . . . . . . 11 (𝑦 = (𝑟 / 2) → (((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦 ↔ ((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2)))
2342332ralbidv 3196 . . . . . . . . . 10 (𝑦 = (𝑟 / 2) → (∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦 ↔ ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2)))
235234rexbidv 3294 . . . . . . . . 9 (𝑦 = (𝑟 / 2) → (∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦 ↔ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2)))
236235rspccva 3619 . . . . . . . 8 ((∀𝑦 ∈ ℝ+𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < 𝑦 ∧ (𝑟 / 2) ∈ ℝ+) → ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2))
237231, 232, 236syl2an 595 . . . . . . 7 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ 𝑟 ∈ ℝ+) → ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2))
2389ffund 6511 . . . . . . . . . . . 12 (𝜑 → Fun 𝐹)
239238ad2antrr 722 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → Fun 𝐹)
2407ad2antrr 722 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → 𝐽 ∈ Top)
241 imassrn 5933 . . . . . . . . . . . . . 14 (𝐹 “ (ℤ𝑚)) ⊆ ran 𝐹
242241, 13sstrid 3975 . . . . . . . . . . . . 13 (𝜑 → (𝐹 “ (ℤ𝑚)) ⊆ 𝐽)
243242ad2antrr 722 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → (𝐹 “ (ℤ𝑚)) ⊆ 𝐽)
244 nnz 11992 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ → 𝑚 ∈ ℤ)
245 fnfvelrn 6840 . . . . . . . . . . . . . . 15 ((ℤ Fn ℤ ∧ 𝑚 ∈ ℤ) → (ℤ𝑚) ∈ ran ℤ)
24657, 244, 245sylancr 587 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ → (ℤ𝑚) ∈ ran ℤ)
247246ad2antll 725 . . . . . . . . . . . . 13 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → (ℤ𝑚) ∈ ran ℤ)
248 simplr 765 . . . . . . . . . . . . 13 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢)))
249 imaeq2 5918 . . . . . . . . . . . . . . . 16 (𝑢 = (ℤ𝑚) → (𝐹𝑢) = (𝐹 “ (ℤ𝑚)))
250249fveq2d 6667 . . . . . . . . . . . . . . 15 (𝑢 = (ℤ𝑚) → ((cls‘𝐽)‘(𝐹𝑢)) = ((cls‘𝐽)‘(𝐹 “ (ℤ𝑚))))
251250eleq2d 2895 . . . . . . . . . . . . . 14 (𝑢 = (ℤ𝑚) → (𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢)) ↔ 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ (ℤ𝑚)))))
252251rspcv 3615 . . . . . . . . . . . . 13 ((ℤ𝑚) ∈ ran ℤ → (∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢)) → 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ (ℤ𝑚)))))
253247, 248, 252sylc 65 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ (ℤ𝑚))))
2544ad2antrr 722 . . . . . . . . . . . . 13 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → 𝐷 ∈ (∞Met‘𝑋))
255220adantr 481 . . . . . . . . . . . . 13 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → 𝑦𝑋)
256232ad2antrl 724 . . . . . . . . . . . . . 14 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → (𝑟 / 2) ∈ ℝ+)
257256rpxrd 12420 . . . . . . . . . . . . 13 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → (𝑟 / 2) ∈ ℝ*)
2585blopn 23037 . . . . . . . . . . . . 13 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦𝑋 ∧ (𝑟 / 2) ∈ ℝ*) → (𝑦(ball‘𝐷)(𝑟 / 2)) ∈ 𝐽)
259254, 255, 257, 258syl3anc 1363 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → (𝑦(ball‘𝐷)(𝑟 / 2)) ∈ 𝐽)
260 blcntr 22950 . . . . . . . . . . . . 13 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦𝑋 ∧ (𝑟 / 2) ∈ ℝ+) → 𝑦 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
261254, 255, 256, 260syl3anc 1363 . . . . . . . . . . . 12 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → 𝑦 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
26215clsndisj 21611 . . . . . . . . . . . 12 (((𝐽 ∈ Top ∧ (𝐹 “ (ℤ𝑚)) ⊆ 𝐽𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ (ℤ𝑚)))) ∧ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∈ 𝐽𝑦 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) → ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚))) ≠ ∅)
263240, 243, 253, 259, 261, 262syl32anc 1370 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚))) ≠ ∅)
264 n0 4307 . . . . . . . . . . . 12 (((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚))) ≠ ∅ ↔ ∃𝑛 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚))))
265 inss2 4203 . . . . . . . . . . . . . . . . 17 ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚))) ⊆ (𝐹 “ (ℤ𝑚))
266265sseli 3960 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚))) → 𝑛 ∈ (𝐹 “ (ℤ𝑚)))
267 fvelima 6724 . . . . . . . . . . . . . . . 16 ((Fun 𝐹𝑛 ∈ (𝐹 “ (ℤ𝑚))) → ∃𝑘 ∈ (ℤ𝑚)(𝐹𝑘) = 𝑛)
268266, 267sylan2 592 . . . . . . . . . . . . . . 15 ((Fun 𝐹𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚)))) → ∃𝑘 ∈ (ℤ𝑚)(𝐹𝑘) = 𝑛)
269 inss1 4202 . . . . . . . . . . . . . . . . . . 19 ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚))) ⊆ (𝑦(ball‘𝐷)(𝑟 / 2))
270269sseli 3960 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚))) → 𝑛 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
271270adantl 482 . . . . . . . . . . . . . . . . 17 ((Fun 𝐹𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚)))) → 𝑛 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
272 eleq1a 2905 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) → ((𝐹𝑘) = 𝑛 → (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
273271, 272syl 17 . . . . . . . . . . . . . . . 16 ((Fun 𝐹𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚)))) → ((𝐹𝑘) = 𝑛 → (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
274273reximdv 3270 . . . . . . . . . . . . . . 15 ((Fun 𝐹𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚)))) → (∃𝑘 ∈ (ℤ𝑚)(𝐹𝑘) = 𝑛 → ∃𝑘 ∈ (ℤ𝑚)(𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
275268, 274mpd 15 . . . . . . . . . . . . . 14 ((Fun 𝐹𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚)))) → ∃𝑘 ∈ (ℤ𝑚)(𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
276275ex 413 . . . . . . . . . . . . 13 (Fun 𝐹 → (𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚))) → ∃𝑘 ∈ (ℤ𝑚)(𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
277276exlimdv 1925 . . . . . . . . . . . 12 (Fun 𝐹 → (∃𝑛 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚))) → ∃𝑘 ∈ (ℤ𝑚)(𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
278264, 277syl5bi 243 . . . . . . . . . . 11 (Fun 𝐹 → (((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ𝑚))) ≠ ∅ → ∃𝑘 ∈ (ℤ𝑚)(𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
279239, 263, 278sylc 65 . . . . . . . . . 10 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → ∃𝑘 ∈ (ℤ𝑚)(𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
280 r19.29 3251 . . . . . . . . . . 11 ((∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) ∧ ∃𝑘 ∈ (ℤ𝑚)(𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ (ℤ𝑚)(∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
281 uznnssnn 12283 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ → (ℤ𝑚) ⊆ ℕ)
282281ad2antll 725 . . . . . . . . . . . . 13 (((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → (ℤ𝑚) ⊆ ℕ)
283 simprlr 776 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
2844ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → 𝐷 ∈ (∞Met‘𝑋))
285 simplrl 773 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → 𝑟 ∈ ℝ+)
286285, 232syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → (𝑟 / 2) ∈ ℝ+)
287286rpxrd 12420 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → (𝑟 / 2) ∈ ℝ*)
288 simpllr 772 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → 𝑦𝑋)
2899ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → 𝐹:ℕ⟶𝑋)
290 eluznn 12306 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑚 ∈ ℕ ∧ 𝑘 ∈ (ℤ𝑚)) → 𝑘 ∈ ℕ)
291290ad2ant2lr 744 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑟 ∈ ℝ+𝑚 ∈ ℕ) ∧ (𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) → 𝑘 ∈ ℕ)
292291ad2ant2lr 744 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → 𝑘 ∈ ℕ)
293289, 292ffvelrnd 6844 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → (𝐹𝑘) ∈ 𝑋)
294 elbl3 22929 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑟 / 2) ∈ ℝ*) ∧ (𝑦𝑋 ∧ (𝐹𝑘) ∈ 𝑋)) → ((𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) ↔ ((𝐹𝑘)𝐷𝑦) < (𝑟 / 2)))
295284, 287, 288, 293, 294syl22anc 834 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → ((𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) ↔ ((𝐹𝑘)𝐷𝑦) < (𝑟 / 2)))
296283, 295mpbid 233 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → ((𝐹𝑘)𝐷𝑦) < (𝑟 / 2))
2972ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → 𝐷 ∈ (Met‘𝑋))
298 simprr 769 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → 𝑛 ∈ (ℤ𝑘))
299 eluznn 12306 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑘 ∈ ℕ ∧ 𝑛 ∈ (ℤ𝑘)) → 𝑛 ∈ ℕ)
300292, 298, 299syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → 𝑛 ∈ ℕ)
301289, 300ffvelrnd 6844 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → (𝐹𝑛) ∈ 𝑋)
302 metcl 22869 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑛) ∈ 𝑋) → ((𝐹𝑘)𝐷(𝐹𝑛)) ∈ ℝ)
303297, 293, 301, 302syl3anc 1363 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → ((𝐹𝑘)𝐷(𝐹𝑛)) ∈ ℝ)
304 metcl 22869 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹𝑘) ∈ 𝑋𝑦𝑋) → ((𝐹𝑘)𝐷𝑦) ∈ ℝ)
305297, 293, 288, 304syl3anc 1363 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → ((𝐹𝑘)𝐷𝑦) ∈ ℝ)
306286rpred 12419 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → (𝑟 / 2) ∈ ℝ)
307 lt2add 11113 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐹𝑘)𝐷(𝐹𝑛)) ∈ ℝ ∧ ((𝐹𝑘)𝐷𝑦) ∈ ℝ) ∧ ((𝑟 / 2) ∈ ℝ ∧ (𝑟 / 2) ∈ ℝ)) → ((((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) ∧ ((𝐹𝑘)𝐷𝑦) < (𝑟 / 2)) → (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) < ((𝑟 / 2) + (𝑟 / 2))))
308303, 305, 306, 306, 307syl22anc 834 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → ((((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) ∧ ((𝐹𝑘)𝐷𝑦) < (𝑟 / 2)) → (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) < ((𝑟 / 2) + (𝑟 / 2))))
309296, 308mpan2d 690 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → (((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) → (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) < ((𝑟 / 2) + (𝑟 / 2))))
310285rpcnd 12421 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → 𝑟 ∈ ℂ)
3113102halvesd 11871 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → ((𝑟 / 2) + (𝑟 / 2)) = 𝑟)
312311breq2d 5069 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → ((((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) < ((𝑟 / 2) + (𝑟 / 2)) ↔ (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) < 𝑟))
313309, 312sylibd 240 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → (((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) → (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) < 𝑟))
314 mettri2 22878 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐷 ∈ (Met‘𝑋) ∧ ((𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑛) ∈ 𝑋𝑦𝑋)) → ((𝐹𝑛)𝐷𝑦) ≤ (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)))
315297, 293, 301, 288, 314syl13anc 1364 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → ((𝐹𝑛)𝐷𝑦) ≤ (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)))
316 metcl 22869 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹𝑛) ∈ 𝑋𝑦𝑋) → ((𝐹𝑛)𝐷𝑦) ∈ ℝ)
317297, 301, 288, 316syl3anc 1363 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → ((𝐹𝑛)𝐷𝑦) ∈ ℝ)
318303, 305readdcld 10658 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) ∈ ℝ)
319285rpred 12419 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → 𝑟 ∈ ℝ)
320 lelttr 10719 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑛)𝐷𝑦) ∈ ℝ ∧ (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) ∈ ℝ ∧ 𝑟 ∈ ℝ) → ((((𝐹𝑛)𝐷𝑦) ≤ (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) ∧ (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) < 𝑟) → ((𝐹𝑛)𝐷𝑦) < 𝑟))
321317, 318, 319, 320syl3anc 1363 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → ((((𝐹𝑛)𝐷𝑦) ≤ (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) ∧ (((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) < 𝑟) → ((𝐹𝑛)𝐷𝑦) < 𝑟))
322315, 321mpand 691 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → ((((𝐹𝑘)𝐷(𝐹𝑛)) + ((𝐹𝑘)𝐷𝑦)) < 𝑟 → ((𝐹𝑛)𝐷𝑦) < 𝑟))
323313, 322syld 47 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ𝑘))) → (((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) → ((𝐹𝑛)𝐷𝑦) < 𝑟))
324323anassrs 468 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ (𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) ∧ 𝑛 ∈ (ℤ𝑘)) → (((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) → ((𝐹𝑛)𝐷𝑦) < 𝑟))
325324ralimdva 3174 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ (𝑘 ∈ (ℤ𝑚) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) → (∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) → ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟))
326325expr 457 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ 𝑘 ∈ (ℤ𝑚)) → ((𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) → (∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) → ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟)))
327326com23 86 . . . . . . . . . . . . . . 15 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ 𝑘 ∈ (ℤ𝑚)) → (∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) → ((𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) → ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟)))
328327impd 411 . . . . . . . . . . . . . 14 ((((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) ∧ 𝑘 ∈ (ℤ𝑚)) → ((∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟))
329328reximdva 3271 . . . . . . . . . . . . 13 (((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → (∃𝑘 ∈ (ℤ𝑚)(∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟))
330 ssrexv 4031 . . . . . . . . . . . . 13 ((ℤ𝑚) ⊆ ℕ → (∃𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟 → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟))
331282, 329, 330sylsyld 61 . . . . . . . . . . . 12 (((𝜑𝑦𝑋) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → (∃𝑘 ∈ (ℤ𝑚)(∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟))
332220, 331syldanl 601 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → (∃𝑘 ∈ (ℤ𝑚)(∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) ∧ (𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟))
333280, 332syl5 34 . . . . . . . . . 10 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → ((∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) ∧ ∃𝑘 ∈ (ℤ𝑚)(𝐹𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟))
334279, 333mpan2d 690 . . . . . . . . 9 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ (𝑟 ∈ ℝ+𝑚 ∈ ℕ)) → (∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟))
335334anassrs 468 . . . . . . . 8 ((((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ 𝑟 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) → (∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟))
336335rexlimdva 3281 . . . . . . 7 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ 𝑟 ∈ ℝ+) → (∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ𝑚)∀𝑛 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑛)) < (𝑟 / 2) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟))
337237, 336mpd 15 . . . . . 6 (((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) ∧ 𝑟 ∈ ℝ+) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟)
338337ralrimiva 3179 . . . . 5 ((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) → ∀𝑟 ∈ ℝ+𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟)
339 eqidd 2819 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) = (𝐹𝑛))
3405, 4, 129, 222, 339, 9lmmbrf 23792 . . . . . 6 (𝜑 → (𝐹(⇝𝑡𝐽)𝑦 ↔ (𝑦𝑋 ∧ ∀𝑟 ∈ ℝ+𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟)))
341340adantr 481 . . . . 5 ((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) → (𝐹(⇝𝑡𝐽)𝑦 ↔ (𝑦𝑋 ∧ ∀𝑟 ∈ ℝ+𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ𝑘)((𝐹𝑛)𝐷𝑦) < 𝑟)))
342220, 338, 341mpbir2and 709 . . . 4 ((𝜑 ∧ ∀𝑢 ∈ ran ℤ𝑦 ∈ ((cls‘𝐽)‘(𝐹𝑢))) → 𝐹(⇝𝑡𝐽)𝑦)
343200, 342sylan2br 594 . . 3 ((𝜑𝑦 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}) → 𝐹(⇝𝑡𝐽)𝑦)
344 releldm 5807 . . 3 ((Rel (⇝𝑡𝐽) ∧ 𝐹(⇝𝑡𝐽)𝑦) → 𝐹 ∈ dom (⇝𝑡𝐽))
345189, 343, 344sylancr 587 . 2 ((𝜑𝑦 {𝑘 ∣ ∃𝑢 ∈ ran ℤ𝑘 = ((cls‘𝐽)‘(𝐹𝑢))}) → 𝐹 ∈ dom (⇝𝑡𝐽))
346188, 345exlimddv 1927 1 (𝜑𝐹 ∈ dom (⇝𝑡𝐽))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1079  wal 1526   = wceq 1528  wex 1771  wcel 2105  {cab 2796  wne 3013  wral 3135  wrex 3136  Vcvv 3492  cun 3931  cin 3932  wss 3933  c0 4288  𝒫 cpw 4535  {csn 4557   cuni 4830   cint 4867   class class class wbr 5057  dom cdm 5548  ran crn 5549  cima 5551  Rel wrel 5553  Fun wfun 6342   Fn wfn 6343  wf 6344  cfv 6348  (class class class)co 7145  pm cpm 8396  Fincfn 8497  ficfi 8862  cc 10523  cr 10524  0cc0 10525  1c1 10526   + caddc 10528  *cxr 10662   < clt 10663  cle 10664   / cdiv 11285  cn 11626  2c2 11680  cz 11969  cuz 12231  +crp 12377  ∞Metcxmet 20458  Metcmet 20459  ballcbl 20460  MetOpencmopn 20463  Topctop 21429  Clsdccld 21552  clsccl 21554  𝑡clm 21762  Compccmp 21922  Cauccau 23783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602  ax-pre-sup 10603
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-iin 4913  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-1st 7678  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-2o 8092  df-oadd 8095  df-er 8278  df-map 8397  df-pm 8398  df-en 8498  df-dom 8499  df-sdom 8500  df-fin 8501  df-fi 8863  df-sup 8894  df-inf 8895  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-div 11286  df-nn 11627  df-2 11688  df-n0 11886  df-z 11970  df-uz 12232  df-q 12337  df-rp 12378  df-xneg 12495  df-xadd 12496  df-xmul 12497  df-topgen 16705  df-psmet 20465  df-xmet 20466  df-met 20467  df-bl 20468  df-mopn 20469  df-top 21430  df-topon 21447  df-bases 21482  df-cld 21555  df-ntr 21556  df-cls 21557  df-lm 21765  df-cmp 21923  df-cau 23786
This theorem is referenced by:  heibor1  34969
  Copyright terms: Public domain W3C validator