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.

Step	Hyp	Ref	Expression
1		heibor1.4	. . 3 ⊢ (𝜑 → 𝐽 ∈ Comp)
2		heibor1.3	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))
3		metxmet 24284	. . . . . . . . . 10 ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
4	2, 3	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))
5		heibor.1	. . . . . . . . . 10 ⊢ 𝐽 = (MetOpen‘𝐷)
6	5	mopntop 24390	. . . . . . . . 9 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
7	4, 6	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ Top)
8		imassrn 6075	. . . . . . . . 9 ⊢ (𝐹 “ 𝑢) ⊆ ran 𝐹
9		heibor1.6	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:ℕ⟶𝑋)
10	9	frnd 6731	. . . . . . . . . 10 ⊢ (𝜑 → ran 𝐹 ⊆ 𝑋)
11	5	mopnuni 24391	. . . . . . . . . . 11 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽)
12	4, 11	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 = ∪ 𝐽)
13	10, 12	sseqtrd 4017	. . . . . . . . 9 ⊢ (𝜑 → ran 𝐹 ⊆ ∪ 𝐽)
14	8, 13	sstrid 3988	. . . . . . . 8 ⊢ (𝜑 → (𝐹 “ 𝑢) ⊆ ∪ 𝐽)
15		eqid 2725	. . . . . . . . 9 ⊢ ∪ 𝐽 = ∪ 𝐽
16	15	clscld 22995	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ (𝐹 “ 𝑢) ⊆ ∪ 𝐽) → ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∈ (Clsd‘𝐽))
17	7, 14, 16	syl2anc 582	. . . . . . 7 ⊢ (𝜑 → ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∈ (Clsd‘𝐽))
18		eleq1a 2820	. . . . . . 7 ⊢ (((cls‘𝐽)‘(𝐹 “ 𝑢)) ∈ (Clsd‘𝐽) → (𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑘 ∈ (Clsd‘𝐽)))
19	17, 18	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑘 ∈ (Clsd‘𝐽)))
20	19	rexlimdvw 3149	. . . . 5 ⊢ (𝜑 → (∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑘 ∈ (Clsd‘𝐽)))
21	20	abssdv 4061	. . . 4 ⊢ (𝜑 → {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ⊆ (Clsd‘𝐽))
22		fvex 6909	. . . . 5 ⊢ (Clsd‘𝐽) ∈ V
23	22	elpw2 5348	. . . 4 ⊢ ({𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∈ 𝒫 (Clsd‘𝐽) ↔ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ⊆ (Clsd‘𝐽))
24	21, 23	sylibr 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‘𝐽)‘(𝐹 “ 𝑢)))
28	26, 27	bitri 274	. . . . . . . 8 ⊢ (𝑟 ∈ 𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ↔ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))
29	28	anbi1i 622	. . . . . . 7 ⊢ ((𝑟 ∈ 𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∧ 𝑟 ∈ Fin) ↔ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin))
30	25, 29	bitri 274	. . . . . 6 ⊢ (𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∩ Fin) ↔ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin))
31		raleq 3311	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ∅ → (∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∀𝑘 ∈ ∅ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))))
32	31	anbi2d 628	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → ((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) ↔ (𝜑 ∧ ∀𝑘 ∈ ∅ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))))
33		inteq 4953	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = ∅ → ∩ 𝑚 = ∩ ∅)
34	33	sseq2d 4009	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ∅ → ((𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ (𝐹 “ 𝑘) ⊆ ∩ ∅))
35	34	rexbidv 3168	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ ∅))
36	32, 35	imbi12d 343	. . . . . . . . . . . 12 ⊢ (𝑚 = ∅ → (((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚) ↔ ((𝜑 ∧ ∀𝑘 ∈ ∅ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ ∅)))
37		raleq 3311	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑦 → (∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∀𝑘 ∈ 𝑦 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))))
38	37	anbi2d 628	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑦 → ((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) ↔ (𝜑 ∧ ∀𝑘 ∈ 𝑦 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))))
39		inteq 4953	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑦 → ∩ 𝑚 = ∩ 𝑦)
40	39	sseq2d 4009	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑦 → ((𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ (𝐹 “ 𝑘) ⊆ ∩ 𝑦))
41	40	rexbidv 3168	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑦 → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦))
42	38, 41	imbi12d 343	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑦 → (((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚) ↔ ((𝜑 ∧ ∀𝑘 ∈ 𝑦 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦)))
43		raleq 3311	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝑦 ∪ {𝑛}) → (∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))))
44	43	anbi2d 628	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝑦 ∪ {𝑛}) → ((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) ↔ (𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))))
45		inteq 4953	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝑦 ∪ {𝑛}) → ∩ 𝑚 = ∩ (𝑦 ∪ {𝑛}))
46	45	sseq2d 4009	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝑦 ∪ {𝑛}) → ((𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ (𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛})))
47	46	rexbidv 3168	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝑦 ∪ {𝑛}) → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛})))
48	44, 47	imbi12d 343	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝑦 ∪ {𝑛}) → (((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚) ↔ ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛}))))
49		raleq 3311	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑟 → (∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))))
50	49	anbi2d 628	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑟 → ((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) ↔ (𝜑 ∧ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))))
51		inteq 4953	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑟 → ∩ 𝑚 = ∩ 𝑟)
52	51	sseq2d 4009	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑟 → ((𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ (𝐹 “ 𝑘) ⊆ ∩ 𝑟))
53	52	rexbidv 3168	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑟 → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑟))
54	50, 53	imbi12d 343	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑟 → (((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚) ↔ ((𝜑 ∧ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑟)))
55		uzf 12858	. . . . . . . . . . . . . . . 16 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
56		ffn 6723	. . . . . . . . . . . . . . . 16 ⊢ (ℤ≥:ℤ⟶𝒫 ℤ → ℤ≥ Fn ℤ)
57	55, 56	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ℤ≥ Fn ℤ
58		0z 12602	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℤ
59		fnfvelrn 7089	. . . . . . . . . . . . . . 15 ⊢ ((ℤ≥ Fn ℤ ∧ 0 ∈ ℤ) → (ℤ≥‘0) ∈ ran ℤ≥)
60	57, 58, 59	mp2an 690	. . . . . . . . . . . . . 14 ⊢ (ℤ≥‘0) ∈ ran ℤ≥
61		ssv 4001	. . . . . . . . . . . . . . 15 ⊢ (𝐹 “ (ℤ≥‘0)) ⊆ V
62		int0 4966	. . . . . . . . . . . . . . 15 ⊢ ∩ ∅ = V
63	61, 62	sseqtrri 4014	. . . . . . . . . . . . . 14 ⊢ (𝐹 “ (ℤ≥‘0)) ⊆ ∩ ∅
64		imaeq2 6060	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (ℤ≥‘0) → (𝐹 “ 𝑘) = (𝐹 “ (ℤ≥‘0)))
65	64	sseq1d 4008	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (ℤ≥‘0) → ((𝐹 “ 𝑘) ⊆ ∩ ∅ ↔ (𝐹 “ (ℤ≥‘0)) ⊆ ∩ ∅))
66	65	rspcev 3606	. . . . . . . . . . . . . 14 ⊢ (((ℤ≥‘0) ∈ ran ℤ≥ ∧ (𝐹 “ (ℤ≥‘0)) ⊆ ∩ ∅) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ ∅)
67	60, 63, 66	mp2an 690	. . . . . . . . . . . . 13 ⊢ ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ ∅
68	67	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ∀𝑘 ∈ ∅ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ ∅)
69		ssun1 4170	. . . . . . . . . . . . . . . . 17 ⊢ 𝑦 ⊆ (𝑦 ∪ {𝑛})
70		ssralv 4045	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ (𝑦 ∪ {𝑛}) → (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → ∀𝑘 ∈ 𝑦 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))))
71	69, 70	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → ∀𝑘 ∈ 𝑦 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))
72	71	anim2i 615	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → (𝜑 ∧ ∀𝑘 ∈ 𝑦 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))))
73	72	imim1i 63	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝑦 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦) → ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦))
74		ssun2 4171	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑛} ⊆ (𝑦 ∪ {𝑛})
75		ssralv 4045	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑛} ⊆ (𝑦 ∪ {𝑛}) → (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → ∀𝑘 ∈ {𝑛}∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))))
76	74, 75	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → ∀𝑘 ∈ {𝑛}∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))
77		vex 3465	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑛 ∈ V
78		eqeq1 2729	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑛 → (𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ 𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢))))
79	78	rexbidv 3168	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑛 → (∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∃𝑢 ∈ ran ℤ≥𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢))))
80	77, 79	ralsn 4687	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑘 ∈ {𝑛}∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∃𝑢 ∈ ran ℤ≥𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))
81	76, 80	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → ∃𝑢 ∈ ran ℤ≥𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))
82		uzin2 15327	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑢 ∈ ran ℤ≥ ∧ 𝑘 ∈ ran ℤ≥) → (𝑢 ∩ 𝑘) ∈ ran ℤ≥)
83	8, 10	sstrid 3988	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐹 “ 𝑢) ⊆ 𝑋)
84	83, 12	sseqtrd 4017	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐹 “ 𝑢) ⊆ ∪ 𝐽)
85	15	sscls 23004	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐽 ∈ Top ∧ (𝐹 “ 𝑢) ⊆ ∪ 𝐽) → (𝐹 “ 𝑢) ⊆ ((cls‘𝐽)‘(𝐹 “ 𝑢)))
86	7, 84, 85	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐹 “ 𝑢) ⊆ ((cls‘𝐽)‘(𝐹 “ 𝑢)))
87		sseq2 4003	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → ((𝐹 “ 𝑢) ⊆ 𝑛 ↔ (𝐹 “ 𝑢) ⊆ ((cls‘𝐽)‘(𝐹 “ 𝑢))))
88	86, 87	syl5ibrcom 246	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → (𝐹 “ 𝑢) ⊆ 𝑛))
89		inss2 4228	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑢 ∩ 𝑘) ⊆ 𝑘
90		inss1 4227	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑢 ∩ 𝑘) ⊆ 𝑢
91		imass2 6107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑢 ∩ 𝑘) ⊆ 𝑘 → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (𝐹 “ 𝑘))
92		imass2 6107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑢 ∩ 𝑘) ⊆ 𝑢 → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (𝐹 “ 𝑢))
93	91, 92	anim12i 611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑢 ∩ 𝑘) ⊆ 𝑘 ∧ (𝑢 ∩ 𝑘) ⊆ 𝑢) → ((𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (𝐹 “ 𝑘) ∧ (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (𝐹 “ 𝑢)))
94		ssin 4229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (𝐹 “ 𝑘) ∧ (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (𝐹 “ 𝑢)) ↔ (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ((𝐹 “ 𝑘) ∩ (𝐹 “ 𝑢)))
95	93, 94	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑢 ∩ 𝑘) ⊆ 𝑘 ∧ (𝑢 ∩ 𝑘) ⊆ 𝑢) → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ((𝐹 “ 𝑘) ∩ (𝐹 “ 𝑢)))
96	89, 90, 95	mp2an 690	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ((𝐹 “ 𝑘) ∩ (𝐹 “ 𝑢))
97		ss2in 4235	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐹 “ 𝑘) ⊆ ∩ 𝑦 ∧ (𝐹 “ 𝑢) ⊆ 𝑛) → ((𝐹 “ 𝑘) ∩ (𝐹 “ 𝑢)) ⊆ (∩ 𝑦 ∩ 𝑛))
98	96, 97	sstrid 3988	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐹 “ 𝑘) ⊆ ∩ 𝑦 ∧ (𝐹 “ 𝑢) ⊆ 𝑛) → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (∩ 𝑦 ∩ 𝑛))
99	77	intunsn 4993	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ∩ (𝑦 ∪ {𝑛}) = (∩ 𝑦 ∩ 𝑛)
100	98, 99	sseqtrrdi 4028	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 “ 𝑘) ⊆ ∩ 𝑦 ∧ (𝐹 “ 𝑢) ⊆ 𝑛) → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ∩ (𝑦 ∪ {𝑛}))
101	100	expcom 412	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹 “ 𝑢) ⊆ 𝑛 → ((𝐹 “ 𝑘) ⊆ ∩ 𝑦 → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ∩ (𝑦 ∪ {𝑛})))
102	88, 101	syl6 35	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → ((𝐹 “ 𝑘) ⊆ ∩ 𝑦 → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ∩ (𝑦 ∪ {𝑛}))))
103	102	impd 409	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ (𝐹 “ 𝑘) ⊆ ∩ 𝑦) → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ∩ (𝑦 ∪ {𝑛})))
104		imaeq2 6060	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑚 = (𝑢 ∩ 𝑘) → (𝐹 “ 𝑚) = (𝐹 “ (𝑢 ∩ 𝑘)))
105	104	sseq1d 4008	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 = (𝑢 ∩ 𝑘) → ((𝐹 “ 𝑚) ⊆ ∩ (𝑦 ∪ {𝑛}) ↔ (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ∩ (𝑦 ∪ {𝑛})))
106	105	rspcev 3606	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑢 ∩ 𝑘) ∈ ran ℤ≥ ∧ (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ∩ (𝑦 ∪ {𝑛})) → ∃𝑚 ∈ ran ℤ≥(𝐹 “ 𝑚) ⊆ ∩ (𝑦 ∪ {𝑛}))
107	106	expcom 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ∩ (𝑦 ∪ {𝑛}) → ((𝑢 ∩ 𝑘) ∈ ran ℤ≥ → ∃𝑚 ∈ ran ℤ≥(𝐹 “ 𝑚) ⊆ ∩ (𝑦 ∪ {𝑛})))
108	103, 107	syl6 35	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ (𝐹 “ 𝑘) ⊆ ∩ 𝑦) → ((𝑢 ∩ 𝑘) ∈ ran ℤ≥ → ∃𝑚 ∈ ran ℤ≥(𝐹 “ 𝑚) ⊆ ∩ (𝑦 ∪ {𝑛}))))
109	108	com23 86	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑢 ∩ 𝑘) ∈ ran ℤ≥ → ((𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ (𝐹 “ 𝑘) ⊆ ∩ 𝑦) → ∃𝑚 ∈ ran ℤ≥(𝐹 “ 𝑚) ⊆ ∩ (𝑦 ∪ {𝑛}))))
110	82, 109	syl5 34	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑢 ∈ ran ℤ≥ ∧ 𝑘 ∈ ran ℤ≥) → ((𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ (𝐹 “ 𝑘) ⊆ ∩ 𝑦) → ∃𝑚 ∈ ran ℤ≥(𝐹 “ 𝑚) ⊆ ∩ (𝑦 ∪ {𝑛}))))
111	110	rexlimdvv 3200	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (∃𝑢 ∈ ran ℤ≥∃𝑘 ∈ ran ℤ≥(𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ (𝐹 “ 𝑘) ⊆ ∩ 𝑦) → ∃𝑚 ∈ ran ℤ≥(𝐹 “ 𝑚) ⊆ ∩ (𝑦 ∪ {𝑛})))
112		reeanv 3216	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑢 ∈ ran ℤ≥∃𝑘 ∈ ran ℤ≥(𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ (𝐹 “ 𝑘) ⊆ ∩ 𝑦) ↔ (∃𝑢 ∈ ran ℤ≥𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦))
113		imaeq2 6060	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑘 → (𝐹 “ 𝑚) = (𝐹 “ 𝑘))
114	113	sseq1d 4008	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑘 → ((𝐹 “ 𝑚) ⊆ ∩ (𝑦 ∪ {𝑛}) ↔ (𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛})))
115	114	cbvrexvw 3225	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑚 ∈ ran ℤ≥(𝐹 “ 𝑚) ⊆ ∩ (𝑦 ∪ {𝑛}) ↔ ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛}))
116	111, 112, 115	3imtr3g 294	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((∃𝑢 ∈ ran ℤ≥𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛})))
117	116	expd 414	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∃𝑢 ∈ ran ℤ≥𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦 → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛}))))
118	81, 117	syl5 34	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦 → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛}))))
119	118	imp 405	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦 → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛})))
120	73, 119	sylcom 30	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝑦 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦) → ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛})))
121	120	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ Fin → (((𝜑 ∧ ∀𝑘 ∈ 𝑦 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦) → ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛}))))
122	36, 42, 48, 54, 68, 121	findcard2 9189	. . . . . . . . . . 11 ⊢ (𝑟 ∈ Fin → ((𝜑 ∧ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑟))
123	122	com12 32	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → (𝑟 ∈ Fin → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑟))
124	123	impr 453	. . . . . . . . 9 ⊢ ((𝜑 ∧ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin)) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑟)
125	9	ffnd 6724	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 Fn ℕ)
126		inss1 4227	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∩ ℕ) ⊆ 𝑘
127		imass2 6107	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∩ ℕ) ⊆ 𝑘 → (𝐹 “ (𝑘 ∩ ℕ)) ⊆ (𝐹 “ 𝑘))
128	126, 127	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (𝐹 “ (𝑘 ∩ ℕ)) ⊆ (𝐹 “ 𝑘)
129		nnuz 12898	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℕ = (ℤ≥‘1)
130		1z 12625	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ ℤ
131		fnfvelrn 7089	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℤ≥ Fn ℤ ∧ 1 ∈ ℤ) → (ℤ≥‘1) ∈ ran ℤ≥)
132	57, 130, 131	mp2an 690	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℤ≥‘1) ∈ ran ℤ≥
133	129, 132	eqeltri 2821	. . . . . . . . . . . . . . . . . . 19 ⊢ ℕ ∈ ran ℤ≥
134		uzin2 15327	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ran ℤ≥ ∧ ℕ ∈ ran ℤ≥) → (𝑘 ∩ ℕ) ∈ ran ℤ≥)
135	133, 134	mpan2 689	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ran ℤ≥ → (𝑘 ∩ ℕ) ∈ ran ℤ≥)
136		uzn0 12872	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∩ ℕ) ∈ ran ℤ≥ → (𝑘 ∩ ℕ) ≠ ∅)
137	135, 136	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ran ℤ≥ → (𝑘 ∩ ℕ) ≠ ∅)
138		n0 4346	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∩ ℕ) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝑘 ∩ ℕ))
139	137, 138	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ran ℤ≥ → ∃𝑦 𝑦 ∈ (𝑘 ∩ ℕ))
140		fnfun 6655	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 Fn ℕ → Fun 𝐹)
141		inss2 4228	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∩ ℕ) ⊆ ℕ
142		fndm 6658	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹 Fn ℕ → dom 𝐹 = ℕ)
143	141, 142	sseqtrrid 4030	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 Fn ℕ → (𝑘 ∩ ℕ) ⊆ dom 𝐹)
144		funfvima2 7243	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝐹 ∧ (𝑘 ∩ ℕ) ⊆ dom 𝐹) → (𝑦 ∈ (𝑘 ∩ ℕ) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑘 ∩ ℕ))))
145	140, 143, 144	syl2anc 582	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 Fn ℕ → (𝑦 ∈ (𝑘 ∩ ℕ) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑘 ∩ ℕ))))
146		ne0i 4334	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑦) ∈ (𝐹 “ (𝑘 ∩ ℕ)) → (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅)
147	145, 146	syl6 35	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 Fn ℕ → (𝑦 ∈ (𝑘 ∩ ℕ) → (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅))
148	147	exlimdv 1928	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 Fn ℕ → (∃𝑦 𝑦 ∈ (𝑘 ∩ ℕ) → (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅))
149	139, 148	syl5 34	. . . . . . . . . . . . . . 15 ⊢ (𝐹 Fn ℕ → (𝑘 ∈ ran ℤ≥ → (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅))
150	149	imp 405	. . . . . . . . . . . . . 14 ⊢ ((𝐹 Fn ℕ ∧ 𝑘 ∈ ran ℤ≥) → (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅)
151		ssn0 4402	. . . . . . . . . . . . . 14 ⊢ (((𝐹 “ (𝑘 ∩ ℕ)) ⊆ (𝐹 “ 𝑘) ∧ (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅) → (𝐹 “ 𝑘) ≠ ∅)
152	128, 150, 151	sylancr 585	. . . . . . . . . . . . 13 ⊢ ((𝐹 Fn ℕ ∧ 𝑘 ∈ ran ℤ≥) → (𝐹 “ 𝑘) ≠ ∅)
153		ssn0 4402	. . . . . . . . . . . . . 14 ⊢ (((𝐹 “ 𝑘) ⊆ ∩ 𝑟 ∧ (𝐹 “ 𝑘) ≠ ∅) → ∩ 𝑟 ≠ ∅)
154	153	expcom 412	. . . . . . . . . . . . 13 ⊢ ((𝐹 “ 𝑘) ≠ ∅ → ((𝐹 “ 𝑘) ⊆ ∩ 𝑟 → ∩ 𝑟 ≠ ∅))
155	152, 154	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐹 Fn ℕ ∧ 𝑘 ∈ ran ℤ≥) → ((𝐹 “ 𝑘) ⊆ ∩ 𝑟 → ∩ 𝑟 ≠ ∅))
156	155	rexlimdva 3144	. . . . . . . . . . 11 ⊢ (𝐹 Fn ℕ → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑟 → ∩ 𝑟 ≠ ∅))
157	125, 156	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑟 → ∩ 𝑟 ≠ ∅))
158	157	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin)) → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑟 → ∩ 𝑟 ≠ ∅))
159	124, 158	mpd 15	. . . . . . . 8 ⊢ ((𝜑 ∧ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin)) → ∩ 𝑟 ≠ ∅)
160	159	necomd 2985	. . . . . . 7 ⊢ ((𝜑 ∧ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin)) → ∅ ≠ ∩ 𝑟)
161	160	neneqd 2934	. . . . . 6 ⊢ ((𝜑 ∧ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin)) → ¬ ∅ = ∩ 𝑟)
162	30, 161	sylan2b 592	. . . . 5 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∩ Fin)) → ¬ ∅ = ∩ 𝑟)
163	162	nrexdv 3138	. . . 4 ⊢ (𝜑 → ¬ ∃𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∩ Fin)∅ = ∩ 𝑟)
164		0ex 5308	. . . . 5 ⊢ ∅ ∈ V
165		zex 12600	. . . . . . . 8 ⊢ ℤ ∈ V
166	165	pwex 5380	. . . . . . 7 ⊢ 𝒫 ℤ ∈ V
167		frn 6730	. . . . . . . 8 ⊢ (ℤ≥:ℤ⟶𝒫 ℤ → ran ℤ≥ ⊆ 𝒫 ℤ)
168	55, 167	ax-mp 5	. . . . . . 7 ⊢ ran ℤ≥ ⊆ 𝒫 ℤ
169	166, 168	ssexi 5323	. . . . . 6 ⊢ ran ℤ≥ ∈ V
170	169	abrexex 7967	. . . . 5 ⊢ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∈ V
171		elfi 9438	. . . . 5 ⊢ ((∅ ∈ V ∧ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∈ V) → (∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))}) ↔ ∃𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∩ Fin)∅ = ∩ 𝑟))
172	164, 170, 171	mp2an 690	. . . 4 ⊢ (∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))}) ↔ ∃𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∩ Fin)∅ = ∩ 𝑟)
173	163, 172	sylnibr 328	. . 3 ⊢ (𝜑 → ¬ ∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))}))
174		cmptop 23343	. . . . . 6 ⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top)
175		cmpfi 23356	. . . . . 6 ⊢ (𝐽 ∈ Top → (𝐽 ∈ Comp ↔ ∀𝑚 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑚) → ∩ 𝑚 ≠ ∅)))
176	174, 175	syl 17	. . . . 5 ⊢ (𝐽 ∈ Comp → (𝐽 ∈ Comp ↔ ∀𝑚 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑚) → ∩ 𝑚 ≠ ∅)))
177	176	ibi 266	. . . 4 ⊢ (𝐽 ∈ Comp → ∀𝑚 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑚) → ∩ 𝑚 ≠ ∅))
178		fveq2 6896	. . . . . . . 8 ⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → (fi‘𝑚) = (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))}))
179	178	eleq2d 2811	. . . . . . 7 ⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → (∅ ∈ (fi‘𝑚) ↔ ∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))})))
180	179	notbid 317	. . . . . 6 ⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → (¬ ∅ ∈ (fi‘𝑚) ↔ ¬ ∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))})))
181		inteq 4953	. . . . . . . 8 ⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → ∩ 𝑚 = ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))})
182	181	neeq1d 2989	. . . . . . 7 ⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → (∩ 𝑚 ≠ ∅ ↔ ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ≠ ∅))
183		n0 4346	. . . . . . 7 ⊢ (∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ≠ ∅ ↔ ∃𝑦 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))})
184	182, 183	bitrdi 286	. . . . . 6 ⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → (∩ 𝑚 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))}))
185	180, 184	imbi12d 343	. . . . 5 ⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → ((¬ ∅ ∈ (fi‘𝑚) → ∩ 𝑚 ≠ ∅) ↔ (¬ ∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))}) → ∃𝑦 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))})))
186	185	rspccv 3603	. . . 4 ⊢ (∀𝑚 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑚) → ∩ 𝑚 ≠ ∅) → ({𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∈ 𝒫 (Clsd‘𝐽) → (¬ ∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))}) → ∃𝑦 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))})))
187	177, 186	syl 17	. . 3 ⊢ (𝐽 ∈ Comp → ({𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∈ 𝒫 (Clsd‘𝐽) → (¬ ∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))}) → ∃𝑦 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))})))
188	1, 24, 173, 187	syl3c 66	. 2 ⊢ (𝜑 → ∃𝑦 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))})
189		lmrel 23178	. . 3 ⊢ Rel (⇝𝑡‘𝐽)
190		r19.23v 3172	. . . . . 6 ⊢ (∀𝑢 ∈ ran ℤ≥(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘) ↔ (∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘))
191	190	albii 1813	. . . . 5 ⊢ (∀𝑘∀𝑢 ∈ ran ℤ≥(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘) ↔ ∀𝑘(∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘))
192		fvex 6909	. . . . . . . 8 ⊢ ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∈ V
193		eleq2 2814	. . . . . . . 8 ⊢ (𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → (𝑦 ∈ 𝑘 ↔ 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))))
194	192, 193	ceqsalv 3500	. . . . . . 7 ⊢ (∀𝑘(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘) ↔ 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢)))
195	194	ralbii 3082	. . . . . 6 ⊢ (∀𝑢 ∈ ran ℤ≥∀𝑘(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘) ↔ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢)))
196		ralcom4 3273	. . . . . 6 ⊢ (∀𝑢 ∈ ran ℤ≥∀𝑘(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘) ↔ ∀𝑘∀𝑢 ∈ ran ℤ≥(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘))
197	195, 196	bitr3i 276	. . . . 5 ⊢ (∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∀𝑘∀𝑢 ∈ ran ℤ≥(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘))
198		vex 3465	. . . . . 6 ⊢ 𝑦 ∈ V
199	198	elintab 4962	. . . . 5 ⊢ (𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ↔ ∀𝑘(∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘))
200	191, 197, 199	3bitr4i 302	. . . 4 ⊢ (∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))})
201		eqid 2725	. . . . . . . . . . 11 ⊢ ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ ℕ))
202		imaeq2 6060	. . . . . . . . . . . . 13 ⊢ (𝑢 = ℕ → (𝐹 “ 𝑢) = (𝐹 “ ℕ))
203	202	fveq2d 6900	. . . . . . . . . . . 12 ⊢ (𝑢 = ℕ → ((cls‘𝐽)‘(𝐹 “ 𝑢)) = ((cls‘𝐽)‘(𝐹 “ ℕ)))
204	203	rspceeqv 3628	. . . . . . . . . . 11 ⊢ ((ℕ ∈ ran ℤ≥ ∧ ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ ℕ))) → ∃𝑢 ∈ ran ℤ≥((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ 𝑢)))
205	133, 201, 204	mp2an 690	. . . . . . . . . 10 ⊢ ∃𝑢 ∈ ran ℤ≥((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ 𝑢))
206		fvex 6909	. . . . . . . . . . 11 ⊢ ((cls‘𝐽)‘(𝐹 “ ℕ)) ∈ V
207		eqeq1 2729	. . . . . . . . . . . 12 ⊢ (𝑘 = ((cls‘𝐽)‘(𝐹 “ ℕ)) → (𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ 𝑢))))
208	207	rexbidv 3168	. . . . . . . . . . 11 ⊢ (𝑘 = ((cls‘𝐽)‘(𝐹 “ ℕ)) → (∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∃𝑢 ∈ ran ℤ≥((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ 𝑢))))
209	206, 208	elab 3664	. . . . . . . . . 10 ⊢ (((cls‘𝐽)‘(𝐹 “ ℕ)) ∈ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ↔ ∃𝑢 ∈ ran ℤ≥((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ 𝑢)))
210	205, 209	mpbir 230	. . . . . . . . 9 ⊢ ((cls‘𝐽)‘(𝐹 “ ℕ)) ∈ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))}
211		intss1 4967	. . . . . . . . 9 ⊢ (((cls‘𝐽)‘(𝐹 “ ℕ)) ∈ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ⊆ ((cls‘𝐽)‘(𝐹 “ ℕ)))
212	210, 211	ax-mp 5	. . . . . . . 8 ⊢ ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ⊆ ((cls‘𝐽)‘(𝐹 “ ℕ))
213		imassrn 6075	. . . . . . . . . . 11 ⊢ (𝐹 “ ℕ) ⊆ ran 𝐹
214	213, 13	sstrid 3988	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹 “ ℕ) ⊆ ∪ 𝐽)
215	15	clsss3 23007	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ (𝐹 “ ℕ) ⊆ ∪ 𝐽) → ((cls‘𝐽)‘(𝐹 “ ℕ)) ⊆ ∪ 𝐽)
216	7, 214, 215	syl2anc 582	. . . . . . . . 9 ⊢ (𝜑 → ((cls‘𝐽)‘(𝐹 “ ℕ)) ⊆ ∪ 𝐽)
217	216, 12	sseqtrrd 4018	. . . . . . . 8 ⊢ (𝜑 → ((cls‘𝐽)‘(𝐹 “ ℕ)) ⊆ 𝑋)
218	212, 217	sstrid 3988	. . . . . . 7 ⊢ (𝜑 → ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ⊆ 𝑋)
219	218	sselda 3976	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))}) → 𝑦 ∈ 𝑋)
220	200, 219	sylan2b 592	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) → 𝑦 ∈ 𝑋)
221		heibor1.5	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ∈ (Cau‘𝐷))
222		1zzd 12626	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ∈ ℤ)
223	129, 4, 222	iscau3 25250	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦))))
224	221, 223	mpbid 231	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦)))
225	224	simprd 494	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑦 ∈ ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦))
226		simp3 1135	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦) → ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦)
227	226	ralimi 3072	. . . . . . . . . . . 12 ⊢ (∀𝑘 ∈ (ℤ≥‘𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦) → ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦)
228	227	reximi 3073	. . . . . . . . . . 11 ⊢ (∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦) → ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦)
229	228	ralimi 3072	. . . . . . . . . 10 ⊢ (∀𝑦 ∈ ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦) → ∀𝑦 ∈ ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦)
230	225, 229	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑦 ∈ ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦)
231	230	adantr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∀𝑦 ∈ ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦)
232		rphalfcl 13036	. . . . . . . 8 ⊢ (𝑟 ∈ ℝ+ → (𝑟 / 2) ∈ ℝ+)
233		breq2 5153	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑟 / 2) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦 ↔ ((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2)))
234	233	2ralbidv 3208	. . . . . . . . . 10 ⊢ (𝑦 = (𝑟 / 2) → (∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦 ↔ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2)))
235	234	rexbidv 3168	. . . . . . . . 9 ⊢ (𝑦 = (𝑟 / 2) → (∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦 ↔ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2)))
236	235	rspccva 3605	. . . . . . . 8 ⊢ ((∀𝑦 ∈ ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦 ∧ (𝑟 / 2) ∈ ℝ+) → ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2))
237	231, 232, 236	syl2an 594	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ 𝑟 ∈ ℝ+) → ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2))
238	9	ffund 6727	. . . . . . . . . . . 12 ⊢ (𝜑 → Fun 𝐹)
239	238	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → Fun 𝐹)
240	7	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → 𝐽 ∈ Top)
241		imassrn 6075	. . . . . . . . . . . . . 14 ⊢ (𝐹 “ (ℤ≥‘𝑚)) ⊆ ran 𝐹
242	241, 13	sstrid 3988	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹 “ (ℤ≥‘𝑚)) ⊆ ∪ 𝐽)
243	242	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (𝐹 “ (ℤ≥‘𝑚)) ⊆ ∪ 𝐽)
244		nnz 12612	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℤ)
245		fnfvelrn 7089	. . . . . . . . . . . . . . 15 ⊢ ((ℤ≥ Fn ℤ ∧ 𝑚 ∈ ℤ) → (ℤ≥‘𝑚) ∈ ran ℤ≥)
246	57, 244, 245	sylancr 585	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ → (ℤ≥‘𝑚) ∈ ran ℤ≥)
247	246	ad2antll 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (ℤ≥‘𝑚) ∈ ran ℤ≥)
248		simplr 767	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢)))
249		imaeq2 6060	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = (ℤ≥‘𝑚) → (𝐹 “ 𝑢) = (𝐹 “ (ℤ≥‘𝑚)))
250	249	fveq2d 6900	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = (ℤ≥‘𝑚) → ((cls‘𝐽)‘(𝐹 “ 𝑢)) = ((cls‘𝐽)‘(𝐹 “ (ℤ≥‘𝑚))))
251	250	eleq2d 2811	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (ℤ≥‘𝑚) → (𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ (ℤ≥‘𝑚)))))
252	251	rspcv 3602	. . . . . . . . . . . . 13 ⊢ ((ℤ≥‘𝑚) ∈ ran ℤ≥ → (∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ (ℤ≥‘𝑚)))))
253	247, 248, 252	sylc 65	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ (ℤ≥‘𝑚))))
254	4	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → 𝐷 ∈ (∞Met‘𝑋))
255	220	adantr 479	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → 𝑦 ∈ 𝑋)
256	232	ad2antrl 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (𝑟 / 2) ∈ ℝ+)
257	256	rpxrd 13052	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (𝑟 / 2) ∈ ℝ*)
258	5	blopn 24453	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ (𝑟 / 2) ∈ ℝ*) → (𝑦(ball‘𝐷)(𝑟 / 2)) ∈ 𝐽)
259	254, 255, 257, 258	syl3anc 1368	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (𝑦(ball‘𝐷)(𝑟 / 2)) ∈ 𝐽)
260		blcntr 24363	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ (𝑟 / 2) ∈ ℝ+) → 𝑦 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
261	254, 255, 256, 260	syl3anc 1368	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → 𝑦 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
262	15	clsndisj 23023	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ (𝐹 “ (ℤ≥‘𝑚)) ⊆ ∪ 𝐽 ∧ 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ (ℤ≥‘𝑚)))) ∧ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∈ 𝐽 ∧ 𝑦 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) → ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) ≠ ∅)
263	240, 243, 253, 259, 261, 262	syl32anc 1375	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) ≠ ∅)
264		n0 4346	. . . . . . . . . . . 12 ⊢ (((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) ≠ ∅ ↔ ∃𝑛 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))))
265		inss2 4228	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) ⊆ (𝐹 “ (ℤ≥‘𝑚))
266	265	sseli 3972	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) → 𝑛 ∈ (𝐹 “ (ℤ≥‘𝑚)))
267		fvelima 6963	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝐹 ∧ 𝑛 ∈ (𝐹 “ (ℤ≥‘𝑚))) → ∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) = 𝑛)
268	266, 267	sylan2 591	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝐹 ∧ 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚)))) → ∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) = 𝑛)
269		inss1 4227	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) ⊆ (𝑦(ball‘𝐷)(𝑟 / 2))
270	269	sseli 3972	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) → 𝑛 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
271	270	adantl 480	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun 𝐹 ∧ 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚)))) → 𝑛 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
272		eleq1a 2820	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) → ((𝐹‘𝑘) = 𝑛 → (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
273	271, 272	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝐹 ∧ 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚)))) → ((𝐹‘𝑘) = 𝑛 → (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
274	273	reximdv 3159	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝐹 ∧ 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚)))) → (∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) = 𝑛 → ∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
275	268, 274	mpd 15	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝐹 ∧ 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚)))) → ∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
276	275	ex 411	. . . . . . . . . . . . 13 ⊢ (Fun 𝐹 → (𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) → ∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
277	276	exlimdv 1928	. . . . . . . . . . . 12 ⊢ (Fun 𝐹 → (∃𝑛 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) → ∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
278	264, 277	biimtrid 241	. . . . . . . . . . 11 ⊢ (Fun 𝐹 → (((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) ≠ ∅ → ∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
279	239, 263, 278	sylc 65	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → ∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
280		r19.29 3103	. . . . . . . . . . 11 ⊢ ((∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ ∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ (ℤ≥‘𝑚)(∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
281		uznnssnn 12912	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ → (ℤ≥‘𝑚) ⊆ ℕ)
282	281	ad2antll 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (ℤ≥‘𝑚) ⊆ ℕ)
283		simprlr 778	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
284	4	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝐷 ∈ (∞Met‘𝑋))
285		simplrl 775	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝑟 ∈ ℝ+)
286	285, 232	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (𝑟 / 2) ∈ ℝ+)
287	286	rpxrd 13052	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (𝑟 / 2) ∈ ℝ*)
288		simpllr 774	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝑦 ∈ 𝑋)
289	9	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝐹:ℕ⟶𝑋)
290		eluznn 12935	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑚 ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘𝑚)) → 𝑘 ∈ ℕ)
291	290	ad2ant2lr 746	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ) ∧ (𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) → 𝑘 ∈ ℕ)
292	291	ad2ant2lr 746	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝑘 ∈ ℕ)
293	289, 292	ffvelcdmd 7094	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (𝐹‘𝑘) ∈ 𝑋)
294		elbl3 24342	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑟 / 2) ∈ ℝ*) ∧ (𝑦 ∈ 𝑋 ∧ (𝐹‘𝑘) ∈ 𝑋)) → ((𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) ↔ ((𝐹‘𝑘)𝐷𝑦) < (𝑟 / 2)))
295	284, 287, 288, 293, 294	syl22anc 837	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) ↔ ((𝐹‘𝑘)𝐷𝑦) < (𝑟 / 2)))
296	283, 295	mpbid 231	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((𝐹‘𝑘)𝐷𝑦) < (𝑟 / 2))
297	2	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝐷 ∈ (Met‘𝑋))
298		simprr 771	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝑛 ∈ (ℤ≥‘𝑘))
299		eluznn 12935	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑘)) → 𝑛 ∈ ℕ)
300	292, 298, 299	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝑛 ∈ ℕ)
301	289, 300	ffvelcdmd 7094	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (𝐹‘𝑛) ∈ 𝑋)
302		metcl 24282	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑛) ∈ 𝑋) → ((𝐹‘𝑘)𝐷(𝐹‘𝑛)) ∈ ℝ)
303	297, 293, 301, 302	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((𝐹‘𝑘)𝐷(𝐹‘𝑛)) ∈ ℝ)
304		metcl 24282	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝐹‘𝑘)𝐷𝑦) ∈ ℝ)
305	297, 293, 288, 304	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((𝐹‘𝑘)𝐷𝑦) ∈ ℝ)
306	286	rpred 13051	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (𝑟 / 2) ∈ ℝ)
307		lt2add 11731	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐹‘𝑘)𝐷(𝐹‘𝑛)) ∈ ℝ ∧ ((𝐹‘𝑘)𝐷𝑦) ∈ ℝ) ∧ ((𝑟 / 2) ∈ ℝ ∧ (𝑟 / 2) ∈ ℝ)) → ((((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ ((𝐹‘𝑘)𝐷𝑦) < (𝑟 / 2)) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < ((𝑟 / 2) + (𝑟 / 2))))
308	303, 305, 306, 306, 307	syl22anc 837	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ ((𝐹‘𝑘)𝐷𝑦) < (𝑟 / 2)) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < ((𝑟 / 2) + (𝑟 / 2))))
309	296, 308	mpan2d 692	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < ((𝑟 / 2) + (𝑟 / 2))))
310	285	rpcnd 13053	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝑟 ∈ ℂ)
311	310	2halvesd 12491	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((𝑟 / 2) + (𝑟 / 2)) = 𝑟)
312	311	breq2d 5161	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < ((𝑟 / 2) + (𝑟 / 2)) ↔ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < 𝑟))
313	309, 312	sylibd 238	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < 𝑟))
314		mettri2 24291	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ ((𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑛) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹‘𝑛)𝐷𝑦) ≤ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)))
315	297, 293, 301, 288, 314	syl13anc 1369	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((𝐹‘𝑛)𝐷𝑦) ≤ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)))
316		metcl 24282	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘𝑛) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝐹‘𝑛)𝐷𝑦) ∈ ℝ)
317	297, 301, 288, 316	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((𝐹‘𝑛)𝐷𝑦) ∈ ℝ)
318	303, 305	readdcld 11275	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) ∈ ℝ)
319	285	rpred 13051	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝑟 ∈ ℝ)
320		lelttr 11336	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑛)𝐷𝑦) ∈ ℝ ∧ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) ∈ ℝ ∧ 𝑟 ∈ ℝ) → ((((𝐹‘𝑛)𝐷𝑦) ≤ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) ∧ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < 𝑟) → ((𝐹‘𝑛)𝐷𝑦) < 𝑟))
321	317, 318, 319, 320	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((((𝐹‘𝑛)𝐷𝑦) ≤ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) ∧ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < 𝑟) → ((𝐹‘𝑛)𝐷𝑦) < 𝑟))
322	315, 321	mpand 693	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < 𝑟 → ((𝐹‘𝑛)𝐷𝑦) < 𝑟))
323	313, 322	syld 47	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ((𝐹‘𝑛)𝐷𝑦) < 𝑟))
324	323	anassrs 466	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ (𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) ∧ 𝑛 ∈ (ℤ≥‘𝑘)) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ((𝐹‘𝑛)𝐷𝑦) < 𝑟))
325	324	ralimdva 3156	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ (𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) → (∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))
326	325	expr 455	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ 𝑘 ∈ (ℤ≥‘𝑚)) → ((𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) → (∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)))
327	326	com23 86	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ 𝑘 ∈ (ℤ≥‘𝑚)) → (∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ((𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) → ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)))
328	327	impd 409	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ 𝑘 ∈ (ℤ≥‘𝑚)) → ((∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))
329	328	reximdva 3157	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (∃𝑘 ∈ (ℤ≥‘𝑚)(∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))
330		ssrexv 4046	. . . . . . . . . . . . 13 ⊢ ((ℤ≥‘𝑚) ⊆ ℕ → (∃𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟 → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))
331	282, 329, 330	sylsyld 61	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (∃𝑘 ∈ (ℤ≥‘𝑚)(∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))
332	220, 331	syldanl 600	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (∃𝑘 ∈ (ℤ≥‘𝑚)(∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))
333	280, 332	syl5 34	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → ((∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ ∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))
334	279, 333	mpan2d 692	. . . . . . . . 9 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))
335	334	anassrs 466	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ 𝑟 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) → (∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))
336	335	rexlimdva 3144	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ 𝑟 ∈ ℝ+) → (∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))
337	237, 336	mpd 15	. . . . . 6 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ 𝑟 ∈ ℝ+) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)
338	337	ralrimiva 3135	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∀𝑟 ∈ ℝ+ ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)
339		eqidd 2726	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) = (𝐹‘𝑛))
340	5, 4, 129, 222, 339, 9	lmmbrf 25234	. . . . . 6 ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑦 ↔ (𝑦 ∈ 𝑋 ∧ ∀𝑟 ∈ ℝ+ ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)))
341	340	adantr 479	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) → (𝐹(⇝𝑡‘𝐽)𝑦 ↔ (𝑦 ∈ 𝑋 ∧ ∀𝑟 ∈ ℝ+ ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)))
342	220, 338, 341	mpbir2and 711	. . . 4 ⊢ ((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) → 𝐹(⇝𝑡‘𝐽)𝑦)
343	200, 342	sylan2br 593	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))}) → 𝐹(⇝𝑡‘𝐽)𝑦)
344		releldm 5946	. . 3 ⊢ ((Rel (⇝𝑡‘𝐽) ∧ 𝐹(⇝𝑡‘𝐽)𝑦) → 𝐹 ∈ dom (⇝𝑡‘𝐽))
345	189, 343, 344	sylancr 585	. 2 ⊢ ((𝜑 ∧ 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))}) → 𝐹 ∈ dom (⇝𝑡‘𝐽))
346	188, 345	exlimddv 1930	1 ⊢ (𝜑 → 𝐹 ∈ dom (⇝𝑡‘𝐽))

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