Theorem heibor1lem 37810

Description: Lemma for heibor1 37811. 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 24229	. . . . . . . . . 10 ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
4	2, 3	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))
5		heibor.1	. . . . . . . . . 10 ⊢ 𝐽 = (MetOpen‘𝐷)
6	5	mopntop 24335	. . . . . . . . 9 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
7	4, 6	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ Top)
8		imassrn 6045	. . . . . . . . 9 ⊢ (𝐹 “ 𝑢) ⊆ ran 𝐹
9		heibor1.6	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:ℕ⟶𝑋)
10	9	frnd 6699	. . . . . . . . . 10 ⊢ (𝜑 → ran 𝐹 ⊆ 𝑋)
11	5	mopnuni 24336	. . . . . . . . . . 11 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽)
12	4, 11	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 = ∪ 𝐽)
13	10, 12	sseqtrd 3986	. . . . . . . . 9 ⊢ (𝜑 → ran 𝐹 ⊆ ∪ 𝐽)
14	8, 13	sstrid 3961	. . . . . . . 8 ⊢ (𝜑 → (𝐹 “ 𝑢) ⊆ ∪ 𝐽)
15		eqid 2730	. . . . . . . . 9 ⊢ ∪ 𝐽 = ∪ 𝐽
16	15	clscld 22941	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ (𝐹 “ 𝑢) ⊆ ∪ 𝐽) → ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∈ (Clsd‘𝐽))
17	7, 14, 16	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∈ (Clsd‘𝐽))
18		eleq1a 2824	. . . . . . 7 ⊢ (((cls‘𝐽)‘(𝐹 “ 𝑢)) ∈ (Clsd‘𝐽) → (𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑘 ∈ (Clsd‘𝐽)))
19	17, 18	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑘 ∈ (Clsd‘𝐽)))
20	19	rexlimdvw 3140	. . . . 5 ⊢ (𝜑 → (∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑘 ∈ (Clsd‘𝐽)))
21	20	abssdv 4034	. . . 4 ⊢ (𝜑 → {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ⊆ (Clsd‘𝐽))
22		fvex 6874	. . . . 5 ⊢ (Clsd‘𝐽) ∈ V
23	22	elpw2 5292	. . . 4 ⊢ ({𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∈ 𝒫 (Clsd‘𝐽) ↔ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ⊆ (Clsd‘𝐽))
24	21, 23	sylibr 234	. . 3 ⊢ (𝜑 → {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∈ 𝒫 (Clsd‘𝐽))
25		elin 3933	. . . . . . 7 ⊢ (𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∩ Fin) ↔ (𝑟 ∈ 𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∧ 𝑟 ∈ Fin))
26		velpw 4571	. . . . . . . . 9 ⊢ (𝑟 ∈ 𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ↔ 𝑟 ⊆ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))})
27		ssabral 4031	. . . . . . . . 9 ⊢ (𝑟 ⊆ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ↔ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))
28	26, 27	bitri 275	. . . . . . . 8 ⊢ (𝑟 ∈ 𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ↔ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))
29	28	anbi1i 624	. . . . . . 7 ⊢ ((𝑟 ∈ 𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∧ 𝑟 ∈ Fin) ↔ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin))
30	25, 29	bitri 275	. . . . . 6 ⊢ (𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∩ Fin) ↔ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin))
31		raleq 3298	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ∅ → (∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∀𝑘 ∈ ∅ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))))
32	31	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → ((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) ↔ (𝜑 ∧ ∀𝑘 ∈ ∅ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))))
33		inteq 4916	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = ∅ → ∩ 𝑚 = ∩ ∅)
34	33	sseq2d 3982	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ∅ → ((𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ (𝐹 “ 𝑘) ⊆ ∩ ∅))
35	34	rexbidv 3158	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ ∅))
36	32, 35	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑚 = ∅ → (((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚) ↔ ((𝜑 ∧ ∀𝑘 ∈ ∅ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ ∅)))
37		raleq 3298	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑦 → (∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∀𝑘 ∈ 𝑦 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))))
38	37	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑦 → ((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) ↔ (𝜑 ∧ ∀𝑘 ∈ 𝑦 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))))
39		inteq 4916	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑦 → ∩ 𝑚 = ∩ 𝑦)
40	39	sseq2d 3982	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑦 → ((𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ (𝐹 “ 𝑘) ⊆ ∩ 𝑦))
41	40	rexbidv 3158	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑦 → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦))
42	38, 41	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑦 → (((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚) ↔ ((𝜑 ∧ ∀𝑘 ∈ 𝑦 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦)))
43		raleq 3298	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝑦 ∪ {𝑛}) → (∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))))
44	43	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝑦 ∪ {𝑛}) → ((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) ↔ (𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))))
45		inteq 4916	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝑦 ∪ {𝑛}) → ∩ 𝑚 = ∩ (𝑦 ∪ {𝑛}))
46	45	sseq2d 3982	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝑦 ∪ {𝑛}) → ((𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ (𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛})))
47	46	rexbidv 3158	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝑦 ∪ {𝑛}) → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛})))
48	44, 47	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝑦 ∪ {𝑛}) → (((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚) ↔ ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛}))))
49		raleq 3298	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑟 → (∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))))
50	49	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑟 → ((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) ↔ (𝜑 ∧ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))))
51		inteq 4916	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑟 → ∩ 𝑚 = ∩ 𝑟)
52	51	sseq2d 3982	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑟 → ((𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ (𝐹 “ 𝑘) ⊆ ∩ 𝑟))
53	52	rexbidv 3158	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑟 → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑟))
54	50, 53	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑟 → (((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚) ↔ ((𝜑 ∧ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑟)))
55		uzf 12803	. . . . . . . . . . . . . . . 16 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
56		ffn 6691	. . . . . . . . . . . . . . . 16 ⊢ (ℤ≥:ℤ⟶𝒫 ℤ → ℤ≥ Fn ℤ)
57	55, 56	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ℤ≥ Fn ℤ
58		0z 12547	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℤ
59		fnfvelrn 7055	. . . . . . . . . . . . . . 15 ⊢ ((ℤ≥ Fn ℤ ∧ 0 ∈ ℤ) → (ℤ≥‘0) ∈ ran ℤ≥)
60	57, 58, 59	mp2an 692	. . . . . . . . . . . . . 14 ⊢ (ℤ≥‘0) ∈ ran ℤ≥
61		ssv 3974	. . . . . . . . . . . . . . 15 ⊢ (𝐹 “ (ℤ≥‘0)) ⊆ V
62		int0 4929	. . . . . . . . . . . . . . 15 ⊢ ∩ ∅ = V
63	61, 62	sseqtrri 3999	. . . . . . . . . . . . . 14 ⊢ (𝐹 “ (ℤ≥‘0)) ⊆ ∩ ∅
64		imaeq2 6030	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (ℤ≥‘0) → (𝐹 “ 𝑘) = (𝐹 “ (ℤ≥‘0)))
65	64	sseq1d 3981	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (ℤ≥‘0) → ((𝐹 “ 𝑘) ⊆ ∩ ∅ ↔ (𝐹 “ (ℤ≥‘0)) ⊆ ∩ ∅))
66	65	rspcev 3591	. . . . . . . . . . . . . 14 ⊢ (((ℤ≥‘0) ∈ ran ℤ≥ ∧ (𝐹 “ (ℤ≥‘0)) ⊆ ∩ ∅) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ ∅)
67	60, 63, 66	mp2an 692	. . . . . . . . . . . . 13 ⊢ ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ ∅
68	67	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ∀𝑘 ∈ ∅ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ ∅)
69		ssun1 4144	. . . . . . . . . . . . . . . . 17 ⊢ 𝑦 ⊆ (𝑦 ∪ {𝑛})
70		ssralv 4018	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ (𝑦 ∪ {𝑛}) → (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → ∀𝑘 ∈ 𝑦 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))))
71	69, 70	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → ∀𝑘 ∈ 𝑦 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))
72	71	anim2i 617	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → (𝜑 ∧ ∀𝑘 ∈ 𝑦 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))))
73	72	imim1i 63	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝑦 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦) → ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦))
74		ssun2 4145	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑛} ⊆ (𝑦 ∪ {𝑛})
75		ssralv 4018	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑛} ⊆ (𝑦 ∪ {𝑛}) → (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → ∀𝑘 ∈ {𝑛}∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))))
76	74, 75	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → ∀𝑘 ∈ {𝑛}∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))
77		vex 3454	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑛 ∈ V
78		eqeq1 2734	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑛 → (𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ 𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢))))
79	78	rexbidv 3158	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑛 → (∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∃𝑢 ∈ ran ℤ≥𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢))))
80	77, 79	ralsn 4648	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑘 ∈ {𝑛}∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∃𝑢 ∈ ran ℤ≥𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))
81	76, 80	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → ∃𝑢 ∈ ran ℤ≥𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))
82		uzin2 15318	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑢 ∈ ran ℤ≥ ∧ 𝑘 ∈ ran ℤ≥) → (𝑢 ∩ 𝑘) ∈ ran ℤ≥)
83	8, 10	sstrid 3961	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐹 “ 𝑢) ⊆ 𝑋)
84	83, 12	sseqtrd 3986	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐹 “ 𝑢) ⊆ ∪ 𝐽)
85	15	sscls 22950	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐽 ∈ Top ∧ (𝐹 “ 𝑢) ⊆ ∪ 𝐽) → (𝐹 “ 𝑢) ⊆ ((cls‘𝐽)‘(𝐹 “ 𝑢)))
86	7, 84, 85	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐹 “ 𝑢) ⊆ ((cls‘𝐽)‘(𝐹 “ 𝑢)))
87		sseq2 3976	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → ((𝐹 “ 𝑢) ⊆ 𝑛 ↔ (𝐹 “ 𝑢) ⊆ ((cls‘𝐽)‘(𝐹 “ 𝑢))))
88	86, 87	syl5ibrcom 247	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → (𝐹 “ 𝑢) ⊆ 𝑛))
89		inss2 4204	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑢 ∩ 𝑘) ⊆ 𝑘
90		inss1 4203	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑢 ∩ 𝑘) ⊆ 𝑢
91		imass2 6076	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑢 ∩ 𝑘) ⊆ 𝑘 → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (𝐹 “ 𝑘))
92		imass2 6076	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑢 ∩ 𝑘) ⊆ 𝑢 → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (𝐹 “ 𝑢))
93	91, 92	anim12i 613	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑢 ∩ 𝑘) ⊆ 𝑘 ∧ (𝑢 ∩ 𝑘) ⊆ 𝑢) → ((𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (𝐹 “ 𝑘) ∧ (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (𝐹 “ 𝑢)))
94		ssin 4205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (𝐹 “ 𝑘) ∧ (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (𝐹 “ 𝑢)) ↔ (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ((𝐹 “ 𝑘) ∩ (𝐹 “ 𝑢)))
95	93, 94	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑢 ∩ 𝑘) ⊆ 𝑘 ∧ (𝑢 ∩ 𝑘) ⊆ 𝑢) → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ((𝐹 “ 𝑘) ∩ (𝐹 “ 𝑢)))
96	89, 90, 95	mp2an 692	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ((𝐹 “ 𝑘) ∩ (𝐹 “ 𝑢))
97		ss2in 4211	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐹 “ 𝑘) ⊆ ∩ 𝑦 ∧ (𝐹 “ 𝑢) ⊆ 𝑛) → ((𝐹 “ 𝑘) ∩ (𝐹 “ 𝑢)) ⊆ (∩ 𝑦 ∩ 𝑛))
98	96, 97	sstrid 3961	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐹 “ 𝑘) ⊆ ∩ 𝑦 ∧ (𝐹 “ 𝑢) ⊆ 𝑛) → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (∩ 𝑦 ∩ 𝑛))
99	77	intunsn 4954	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ∩ (𝑦 ∪ {𝑛}) = (∩ 𝑦 ∩ 𝑛)
100	98, 99	sseqtrrdi 3991	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 “ 𝑘) ⊆ ∩ 𝑦 ∧ (𝐹 “ 𝑢) ⊆ 𝑛) → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ∩ (𝑦 ∪ {𝑛}))
101	100	expcom 413	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹 “ 𝑢) ⊆ 𝑛 → ((𝐹 “ 𝑘) ⊆ ∩ 𝑦 → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ∩ (𝑦 ∪ {𝑛})))
102	88, 101	syl6 35	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → ((𝐹 “ 𝑘) ⊆ ∩ 𝑦 → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ∩ (𝑦 ∪ {𝑛}))))
103	102	impd 410	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ (𝐹 “ 𝑘) ⊆ ∩ 𝑦) → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ∩ (𝑦 ∪ {𝑛})))
104		imaeq2 6030	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑚 = (𝑢 ∩ 𝑘) → (𝐹 “ 𝑚) = (𝐹 “ (𝑢 ∩ 𝑘)))
105	104	sseq1d 3981	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 = (𝑢 ∩ 𝑘) → ((𝐹 “ 𝑚) ⊆ ∩ (𝑦 ∪ {𝑛}) ↔ (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ∩ (𝑦 ∪ {𝑛})))
106	105	rspcev 3591	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑢 ∩ 𝑘) ∈ ran ℤ≥ ∧ (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ∩ (𝑦 ∪ {𝑛})) → ∃𝑚 ∈ ran ℤ≥(𝐹 “ 𝑚) ⊆ ∩ (𝑦 ∪ {𝑛}))
107	106	expcom 413	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ∩ (𝑦 ∪ {𝑛}) → ((𝑢 ∩ 𝑘) ∈ ran ℤ≥ → ∃𝑚 ∈ ran ℤ≥(𝐹 “ 𝑚) ⊆ ∩ (𝑦 ∪ {𝑛})))
108	103, 107	syl6 35	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ (𝐹 “ 𝑘) ⊆ ∩ 𝑦) → ((𝑢 ∩ 𝑘) ∈ ran ℤ≥ → ∃𝑚 ∈ ran ℤ≥(𝐹 “ 𝑚) ⊆ ∩ (𝑦 ∪ {𝑛}))))
109	108	com23 86	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑢 ∩ 𝑘) ∈ ran ℤ≥ → ((𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ (𝐹 “ 𝑘) ⊆ ∩ 𝑦) → ∃𝑚 ∈ ran ℤ≥(𝐹 “ 𝑚) ⊆ ∩ (𝑦 ∪ {𝑛}))))
110	82, 109	syl5 34	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑢 ∈ ran ℤ≥ ∧ 𝑘 ∈ ran ℤ≥) → ((𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ (𝐹 “ 𝑘) ⊆ ∩ 𝑦) → ∃𝑚 ∈ ran ℤ≥(𝐹 “ 𝑚) ⊆ ∩ (𝑦 ∪ {𝑛}))))
111	110	rexlimdvv 3194	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (∃𝑢 ∈ ran ℤ≥∃𝑘 ∈ ran ℤ≥(𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ (𝐹 “ 𝑘) ⊆ ∩ 𝑦) → ∃𝑚 ∈ ran ℤ≥(𝐹 “ 𝑚) ⊆ ∩ (𝑦 ∪ {𝑛})))
112		reeanv 3210	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑢 ∈ ran ℤ≥∃𝑘 ∈ ran ℤ≥(𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ (𝐹 “ 𝑘) ⊆ ∩ 𝑦) ↔ (∃𝑢 ∈ ran ℤ≥𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦))
113		imaeq2 6030	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑘 → (𝐹 “ 𝑚) = (𝐹 “ 𝑘))
114	113	sseq1d 3981	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑘 → ((𝐹 “ 𝑚) ⊆ ∩ (𝑦 ∪ {𝑛}) ↔ (𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛})))
115	114	cbvrexvw 3217	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑚 ∈ ran ℤ≥(𝐹 “ 𝑚) ⊆ ∩ (𝑦 ∪ {𝑛}) ↔ ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛}))
116	111, 112, 115	3imtr3g 295	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((∃𝑢 ∈ ran ℤ≥𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛})))
117	116	expd 415	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∃𝑢 ∈ ran ℤ≥𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦 → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛}))))
118	81, 117	syl5 34	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦 → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛}))))
119	118	imp 406	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦 → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛})))
120	73, 119	sylcom 30	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝑦 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦) → ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛})))
121	120	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ Fin → (((𝜑 ∧ ∀𝑘 ∈ 𝑦 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦) → ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛}))))
122	36, 42, 48, 54, 68, 121	findcard2 9134	. . . . . . . . . . 11 ⊢ (𝑟 ∈ Fin → ((𝜑 ∧ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑟))
123	122	com12 32	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → (𝑟 ∈ Fin → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑟))
124	123	impr 454	. . . . . . . . 9 ⊢ ((𝜑 ∧ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin)) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑟)
125	9	ffnd 6692	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 Fn ℕ)
126		inss1 4203	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∩ ℕ) ⊆ 𝑘
127		imass2 6076	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∩ ℕ) ⊆ 𝑘 → (𝐹 “ (𝑘 ∩ ℕ)) ⊆ (𝐹 “ 𝑘))
128	126, 127	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (𝐹 “ (𝑘 ∩ ℕ)) ⊆ (𝐹 “ 𝑘)
129		nnuz 12843	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℕ = (ℤ≥‘1)
130		1z 12570	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ ℤ
131		fnfvelrn 7055	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℤ≥ Fn ℤ ∧ 1 ∈ ℤ) → (ℤ≥‘1) ∈ ran ℤ≥)
132	57, 130, 131	mp2an 692	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℤ≥‘1) ∈ ran ℤ≥
133	129, 132	eqeltri 2825	. . . . . . . . . . . . . . . . . . 19 ⊢ ℕ ∈ ran ℤ≥
134		uzin2 15318	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ran ℤ≥ ∧ ℕ ∈ ran ℤ≥) → (𝑘 ∩ ℕ) ∈ ran ℤ≥)
135	133, 134	mpan2 691	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ran ℤ≥ → (𝑘 ∩ ℕ) ∈ ran ℤ≥)
136		uzn0 12817	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∩ ℕ) ∈ ran ℤ≥ → (𝑘 ∩ ℕ) ≠ ∅)
137	135, 136	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ran ℤ≥ → (𝑘 ∩ ℕ) ≠ ∅)
138		n0 4319	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∩ ℕ) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝑘 ∩ ℕ))
139	137, 138	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ran ℤ≥ → ∃𝑦 𝑦 ∈ (𝑘 ∩ ℕ))
140		fnfun 6621	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 Fn ℕ → Fun 𝐹)
141		inss2 4204	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∩ ℕ) ⊆ ℕ
142		fndm 6624	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹 Fn ℕ → dom 𝐹 = ℕ)
143	141, 142	sseqtrrid 3993	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 Fn ℕ → (𝑘 ∩ ℕ) ⊆ dom 𝐹)
144		funfvima2 7208	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝐹 ∧ (𝑘 ∩ ℕ) ⊆ dom 𝐹) → (𝑦 ∈ (𝑘 ∩ ℕ) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑘 ∩ ℕ))))
145	140, 143, 144	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 Fn ℕ → (𝑦 ∈ (𝑘 ∩ ℕ) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑘 ∩ ℕ))))
146		ne0i 4307	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑦) ∈ (𝐹 “ (𝑘 ∩ ℕ)) → (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅)
147	145, 146	syl6 35	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 Fn ℕ → (𝑦 ∈ (𝑘 ∩ ℕ) → (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅))
148	147	exlimdv 1933	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 Fn ℕ → (∃𝑦 𝑦 ∈ (𝑘 ∩ ℕ) → (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅))
149	139, 148	syl5 34	. . . . . . . . . . . . . . 15 ⊢ (𝐹 Fn ℕ → (𝑘 ∈ ran ℤ≥ → (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅))
150	149	imp 406	. . . . . . . . . . . . . 14 ⊢ ((𝐹 Fn ℕ ∧ 𝑘 ∈ ran ℤ≥) → (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅)
151		ssn0 4370	. . . . . . . . . . . . . 14 ⊢ (((𝐹 “ (𝑘 ∩ ℕ)) ⊆ (𝐹 “ 𝑘) ∧ (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅) → (𝐹 “ 𝑘) ≠ ∅)
152	128, 150, 151	sylancr 587	. . . . . . . . . . . . 13 ⊢ ((𝐹 Fn ℕ ∧ 𝑘 ∈ ran ℤ≥) → (𝐹 “ 𝑘) ≠ ∅)
153		ssn0 4370	. . . . . . . . . . . . . 14 ⊢ (((𝐹 “ 𝑘) ⊆ ∩ 𝑟 ∧ (𝐹 “ 𝑘) ≠ ∅) → ∩ 𝑟 ≠ ∅)
154	153	expcom 413	. . . . . . . . . . . . 13 ⊢ ((𝐹 “ 𝑘) ≠ ∅ → ((𝐹 “ 𝑘) ⊆ ∩ 𝑟 → ∩ 𝑟 ≠ ∅))
155	152, 154	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐹 Fn ℕ ∧ 𝑘 ∈ ran ℤ≥) → ((𝐹 “ 𝑘) ⊆ ∩ 𝑟 → ∩ 𝑟 ≠ ∅))
156	155	rexlimdva 3135	. . . . . . . . . . 11 ⊢ (𝐹 Fn ℕ → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑟 → ∩ 𝑟 ≠ ∅))
157	125, 156	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑟 → ∩ 𝑟 ≠ ∅))
158	157	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin)) → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑟 → ∩ 𝑟 ≠ ∅))
159	124, 158	mpd 15	. . . . . . . 8 ⊢ ((𝜑 ∧ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin)) → ∩ 𝑟 ≠ ∅)
160	159	necomd 2981	. . . . . . 7 ⊢ ((𝜑 ∧ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin)) → ∅ ≠ ∩ 𝑟)
161	160	neneqd 2931	. . . . . 6 ⊢ ((𝜑 ∧ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin)) → ¬ ∅ = ∩ 𝑟)
162	30, 161	sylan2b 594	. . . . 5 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∩ Fin)) → ¬ ∅ = ∩ 𝑟)
163	162	nrexdv 3129	. . . 4 ⊢ (𝜑 → ¬ ∃𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∩ Fin)∅ = ∩ 𝑟)
164		0ex 5265	. . . . 5 ⊢ ∅ ∈ V
165		zex 12545	. . . . . . . 8 ⊢ ℤ ∈ V
166	165	pwex 5338	. . . . . . 7 ⊢ 𝒫 ℤ ∈ V
167		frn 6698	. . . . . . . 8 ⊢ (ℤ≥:ℤ⟶𝒫 ℤ → ran ℤ≥ ⊆ 𝒫 ℤ)
168	55, 167	ax-mp 5	. . . . . . 7 ⊢ ran ℤ≥ ⊆ 𝒫 ℤ
169	166, 168	ssexi 5280	. . . . . 6 ⊢ ran ℤ≥ ∈ V
170	169	abrexex 7944	. . . . 5 ⊢ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∈ V
171		elfi 9371	. . . . 5 ⊢ ((∅ ∈ V ∧ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∈ V) → (∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))}) ↔ ∃𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∩ Fin)∅ = ∩ 𝑟))
172	164, 170, 171	mp2an 692	. . . 4 ⊢ (∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))}) ↔ ∃𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∩ Fin)∅ = ∩ 𝑟)
173	163, 172	sylnibr 329	. . 3 ⊢ (𝜑 → ¬ ∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))}))
174		cmptop 23289	. . . . . 6 ⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top)
175		cmpfi 23302	. . . . . 6 ⊢ (𝐽 ∈ Top → (𝐽 ∈ Comp ↔ ∀𝑚 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑚) → ∩ 𝑚 ≠ ∅)))
176	174, 175	syl 17	. . . . 5 ⊢ (𝐽 ∈ Comp → (𝐽 ∈ Comp ↔ ∀𝑚 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑚) → ∩ 𝑚 ≠ ∅)))
177	176	ibi 267	. . . 4 ⊢ (𝐽 ∈ Comp → ∀𝑚 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑚) → ∩ 𝑚 ≠ ∅))
178		fveq2 6861	. . . . . . . 8 ⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → (fi‘𝑚) = (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))}))
179	178	eleq2d 2815	. . . . . . 7 ⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → (∅ ∈ (fi‘𝑚) ↔ ∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))})))
180	179	notbid 318	. . . . . 6 ⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → (¬ ∅ ∈ (fi‘𝑚) ↔ ¬ ∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))})))
181		inteq 4916	. . . . . . . 8 ⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → ∩ 𝑚 = ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))})
182	181	neeq1d 2985	. . . . . . 7 ⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → (∩ 𝑚 ≠ ∅ ↔ ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ≠ ∅))
183		n0 4319	. . . . . . 7 ⊢ (∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ≠ ∅ ↔ ∃𝑦 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))})
184	182, 183	bitrdi 287	. . . . . 6 ⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → (∩ 𝑚 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))}))
185	180, 184	imbi12d 344	. . . . 5 ⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → ((¬ ∅ ∈ (fi‘𝑚) → ∩ 𝑚 ≠ ∅) ↔ (¬ ∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))}) → ∃𝑦 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))})))
186	185	rspccv 3588	. . . 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 23124	. . 3 ⊢ Rel (⇝𝑡‘𝐽)
190		r19.23v 3162	. . . . . 6 ⊢ (∀𝑢 ∈ ran ℤ≥(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘) ↔ (∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘))
191	190	albii 1819	. . . . 5 ⊢ (∀𝑘∀𝑢 ∈ ran ℤ≥(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘) ↔ ∀𝑘(∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘))
192		fvex 6874	. . . . . . . 8 ⊢ ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∈ V
193		eleq2 2818	. . . . . . . 8 ⊢ (𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → (𝑦 ∈ 𝑘 ↔ 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))))
194	192, 193	ceqsalv 3490	. . . . . . 7 ⊢ (∀𝑘(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘) ↔ 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢)))
195	194	ralbii 3076	. . . . . 6 ⊢ (∀𝑢 ∈ ran ℤ≥∀𝑘(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘) ↔ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢)))
196		ralcom4 3264	. . . . . 6 ⊢ (∀𝑢 ∈ ran ℤ≥∀𝑘(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘) ↔ ∀𝑘∀𝑢 ∈ ran ℤ≥(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘))
197	195, 196	bitr3i 277	. . . . 5 ⊢ (∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∀𝑘∀𝑢 ∈ ran ℤ≥(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘))
198		vex 3454	. . . . . 6 ⊢ 𝑦 ∈ V
199	198	elintab 4925	. . . . 5 ⊢ (𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ↔ ∀𝑘(∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘))
200	191, 197, 199	3bitr4i 303	. . . 4 ⊢ (∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))})
201		eqid 2730	. . . . . . . . . . 11 ⊢ ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ ℕ))
202		imaeq2 6030	. . . . . . . . . . . . 13 ⊢ (𝑢 = ℕ → (𝐹 “ 𝑢) = (𝐹 “ ℕ))
203	202	fveq2d 6865	. . . . . . . . . . . 12 ⊢ (𝑢 = ℕ → ((cls‘𝐽)‘(𝐹 “ 𝑢)) = ((cls‘𝐽)‘(𝐹 “ ℕ)))
204	203	rspceeqv 3614	. . . . . . . . . . 11 ⊢ ((ℕ ∈ ran ℤ≥ ∧ ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ ℕ))) → ∃𝑢 ∈ ran ℤ≥((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ 𝑢)))
205	133, 201, 204	mp2an 692	. . . . . . . . . 10 ⊢ ∃𝑢 ∈ ran ℤ≥((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ 𝑢))
206		fvex 6874	. . . . . . . . . . 11 ⊢ ((cls‘𝐽)‘(𝐹 “ ℕ)) ∈ V
207		eqeq1 2734	. . . . . . . . . . . 12 ⊢ (𝑘 = ((cls‘𝐽)‘(𝐹 “ ℕ)) → (𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ 𝑢))))
208	207	rexbidv 3158	. . . . . . . . . . 11 ⊢ (𝑘 = ((cls‘𝐽)‘(𝐹 “ ℕ)) → (∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∃𝑢 ∈ ran ℤ≥((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ 𝑢))))
209	206, 208	elab 3649	. . . . . . . . . 10 ⊢ (((cls‘𝐽)‘(𝐹 “ ℕ)) ∈ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ↔ ∃𝑢 ∈ ran ℤ≥((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ 𝑢)))
210	205, 209	mpbir 231	. . . . . . . . 9 ⊢ ((cls‘𝐽)‘(𝐹 “ ℕ)) ∈ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))}
211		intss1 4930	. . . . . . . . 9 ⊢ (((cls‘𝐽)‘(𝐹 “ ℕ)) ∈ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ⊆ ((cls‘𝐽)‘(𝐹 “ ℕ)))
212	210, 211	ax-mp 5	. . . . . . . 8 ⊢ ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ⊆ ((cls‘𝐽)‘(𝐹 “ ℕ))
213		imassrn 6045	. . . . . . . . . . 11 ⊢ (𝐹 “ ℕ) ⊆ ran 𝐹
214	213, 13	sstrid 3961	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹 “ ℕ) ⊆ ∪ 𝐽)
215	15	clsss3 22953	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ (𝐹 “ ℕ) ⊆ ∪ 𝐽) → ((cls‘𝐽)‘(𝐹 “ ℕ)) ⊆ ∪ 𝐽)
216	7, 214, 215	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → ((cls‘𝐽)‘(𝐹 “ ℕ)) ⊆ ∪ 𝐽)
217	216, 12	sseqtrrd 3987	. . . . . . . 8 ⊢ (𝜑 → ((cls‘𝐽)‘(𝐹 “ ℕ)) ⊆ 𝑋)
218	212, 217	sstrid 3961	. . . . . . 7 ⊢ (𝜑 → ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ⊆ 𝑋)
219	218	sselda 3949	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))}) → 𝑦 ∈ 𝑋)
220	200, 219	sylan2b 594	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) → 𝑦 ∈ 𝑋)
221		heibor1.5	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ∈ (Cau‘𝐷))
222		1zzd 12571	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ∈ ℤ)
223	129, 4, 222	iscau3 25185	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦))))
224	221, 223	mpbid 232	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦)))
225	224	simprd 495	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑦 ∈ ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦))
226		simp3 1138	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦) → ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦)
227	226	ralimi 3067	. . . . . . . . . . . 12 ⊢ (∀𝑘 ∈ (ℤ≥‘𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦) → ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦)
228	227	reximi 3068	. . . . . . . . . . 11 ⊢ (∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦) → ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦)
229	228	ralimi 3067	. . . . . . . . . 10 ⊢ (∀𝑦 ∈ ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦) → ∀𝑦 ∈ ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦)
230	225, 229	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑦 ∈ ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦)
231	230	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∀𝑦 ∈ ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦)
232		rphalfcl 12987	. . . . . . . 8 ⊢ (𝑟 ∈ ℝ+ → (𝑟 / 2) ∈ ℝ+)
233		breq2 5114	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑟 / 2) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦 ↔ ((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2)))
234	233	2ralbidv 3202	. . . . . . . . . 10 ⊢ (𝑦 = (𝑟 / 2) → (∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦 ↔ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2)))
235	234	rexbidv 3158	. . . . . . . . 9 ⊢ (𝑦 = (𝑟 / 2) → (∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦 ↔ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2)))
236	235	rspccva 3590	. . . . . . . 8 ⊢ ((∀𝑦 ∈ ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦 ∧ (𝑟 / 2) ∈ ℝ+) → ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2))
237	231, 232, 236	syl2an 596	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ 𝑟 ∈ ℝ+) → ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2))
238	9	ffund 6695	. . . . . . . . . . . 12 ⊢ (𝜑 → Fun 𝐹)
239	238	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → Fun 𝐹)
240	7	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → 𝐽 ∈ Top)
241		imassrn 6045	. . . . . . . . . . . . . 14 ⊢ (𝐹 “ (ℤ≥‘𝑚)) ⊆ ran 𝐹
242	241, 13	sstrid 3961	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹 “ (ℤ≥‘𝑚)) ⊆ ∪ 𝐽)
243	242	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (𝐹 “ (ℤ≥‘𝑚)) ⊆ ∪ 𝐽)
244		nnz 12557	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℤ)
245		fnfvelrn 7055	. . . . . . . . . . . . . . 15 ⊢ ((ℤ≥ Fn ℤ ∧ 𝑚 ∈ ℤ) → (ℤ≥‘𝑚) ∈ ran ℤ≥)
246	57, 244, 245	sylancr 587	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ → (ℤ≥‘𝑚) ∈ ran ℤ≥)
247	246	ad2antll 729	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (ℤ≥‘𝑚) ∈ ran ℤ≥)
248		simplr 768	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢)))
249		imaeq2 6030	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = (ℤ≥‘𝑚) → (𝐹 “ 𝑢) = (𝐹 “ (ℤ≥‘𝑚)))
250	249	fveq2d 6865	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = (ℤ≥‘𝑚) → ((cls‘𝐽)‘(𝐹 “ 𝑢)) = ((cls‘𝐽)‘(𝐹 “ (ℤ≥‘𝑚))))
251	250	eleq2d 2815	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (ℤ≥‘𝑚) → (𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ (ℤ≥‘𝑚)))))
252	251	rspcv 3587	. . . . . . . . . . . . 13 ⊢ ((ℤ≥‘𝑚) ∈ ran ℤ≥ → (∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ (ℤ≥‘𝑚)))))
253	247, 248, 252	sylc 65	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ (ℤ≥‘𝑚))))
254	4	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → 𝐷 ∈ (∞Met‘𝑋))
255	220	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → 𝑦 ∈ 𝑋)
256	232	ad2antrl 728	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (𝑟 / 2) ∈ ℝ+)
257	256	rpxrd 13003	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (𝑟 / 2) ∈ ℝ*)
258	5	blopn 24395	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ (𝑟 / 2) ∈ ℝ*) → (𝑦(ball‘𝐷)(𝑟 / 2)) ∈ 𝐽)
259	254, 255, 257, 258	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (𝑦(ball‘𝐷)(𝑟 / 2)) ∈ 𝐽)
260		blcntr 24308	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ (𝑟 / 2) ∈ ℝ+) → 𝑦 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
261	254, 255, 256, 260	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → 𝑦 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
262	15	clsndisj 22969	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ (𝐹 “ (ℤ≥‘𝑚)) ⊆ ∪ 𝐽 ∧ 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ (ℤ≥‘𝑚)))) ∧ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∈ 𝐽 ∧ 𝑦 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) → ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) ≠ ∅)
263	240, 243, 253, 259, 261, 262	syl32anc 1380	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) ≠ ∅)
264		n0 4319	. . . . . . . . . . . 12 ⊢ (((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) ≠ ∅ ↔ ∃𝑛 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))))
265		inss2 4204	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) ⊆ (𝐹 “ (ℤ≥‘𝑚))
266	265	sseli 3945	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) → 𝑛 ∈ (𝐹 “ (ℤ≥‘𝑚)))
267		fvelima 6929	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝐹 ∧ 𝑛 ∈ (𝐹 “ (ℤ≥‘𝑚))) → ∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) = 𝑛)
268	266, 267	sylan2 593	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝐹 ∧ 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚)))) → ∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) = 𝑛)
269		inss1 4203	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) ⊆ (𝑦(ball‘𝐷)(𝑟 / 2))
270	269	sseli 3945	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) → 𝑛 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
271	270	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun 𝐹 ∧ 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚)))) → 𝑛 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
272		eleq1a 2824	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) → ((𝐹‘𝑘) = 𝑛 → (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
273	271, 272	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝐹 ∧ 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚)))) → ((𝐹‘𝑘) = 𝑛 → (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
274	273	reximdv 3149	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝐹 ∧ 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚)))) → (∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) = 𝑛 → ∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
275	268, 274	mpd 15	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝐹 ∧ 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚)))) → ∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
276	275	ex 412	. . . . . . . . . . . . 13 ⊢ (Fun 𝐹 → (𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) → ∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
277	276	exlimdv 1933	. . . . . . . . . . . 12 ⊢ (Fun 𝐹 → (∃𝑛 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) → ∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
278	264, 277	biimtrid 242	. . . . . . . . . . 11 ⊢ (Fun 𝐹 → (((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) ≠ ∅ → ∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
279	239, 263, 278	sylc 65	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → ∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
280		r19.29 3095	. . . . . . . . . . 11 ⊢ ((∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ ∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ (ℤ≥‘𝑚)(∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
281		uznnssnn 12861	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ → (ℤ≥‘𝑚) ⊆ ℕ)
282	281	ad2antll 729	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (ℤ≥‘𝑚) ⊆ ℕ)
283		simprlr 779	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
284	4	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝐷 ∈ (∞Met‘𝑋))
285		simplrl 776	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝑟 ∈ ℝ+)
286	285, 232	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (𝑟 / 2) ∈ ℝ+)
287	286	rpxrd 13003	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (𝑟 / 2) ∈ ℝ*)
288		simpllr 775	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝑦 ∈ 𝑋)
289	9	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝐹:ℕ⟶𝑋)
290		eluznn 12884	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑚 ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘𝑚)) → 𝑘 ∈ ℕ)
291	290	ad2ant2lr 748	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ) ∧ (𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) → 𝑘 ∈ ℕ)
292	291	ad2ant2lr 748	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝑘 ∈ ℕ)
293	289, 292	ffvelcdmd 7060	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (𝐹‘𝑘) ∈ 𝑋)
294		elbl3 24287	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑟 / 2) ∈ ℝ*) ∧ (𝑦 ∈ 𝑋 ∧ (𝐹‘𝑘) ∈ 𝑋)) → ((𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) ↔ ((𝐹‘𝑘)𝐷𝑦) < (𝑟 / 2)))
295	284, 287, 288, 293, 294	syl22anc 838	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) ↔ ((𝐹‘𝑘)𝐷𝑦) < (𝑟 / 2)))
296	283, 295	mpbid 232	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((𝐹‘𝑘)𝐷𝑦) < (𝑟 / 2))
297	2	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝐷 ∈ (Met‘𝑋))
298		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝑛 ∈ (ℤ≥‘𝑘))
299		eluznn 12884	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑘)) → 𝑛 ∈ ℕ)
300	292, 298, 299	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝑛 ∈ ℕ)
301	289, 300	ffvelcdmd 7060	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (𝐹‘𝑛) ∈ 𝑋)
302		metcl 24227	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑛) ∈ 𝑋) → ((𝐹‘𝑘)𝐷(𝐹‘𝑛)) ∈ ℝ)
303	297, 293, 301, 302	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((𝐹‘𝑘)𝐷(𝐹‘𝑛)) ∈ ℝ)
304		metcl 24227	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝐹‘𝑘)𝐷𝑦) ∈ ℝ)
305	297, 293, 288, 304	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((𝐹‘𝑘)𝐷𝑦) ∈ ℝ)
306	286	rpred 13002	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (𝑟 / 2) ∈ ℝ)
307		lt2add 11670	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐹‘𝑘)𝐷(𝐹‘𝑛)) ∈ ℝ ∧ ((𝐹‘𝑘)𝐷𝑦) ∈ ℝ) ∧ ((𝑟 / 2) ∈ ℝ ∧ (𝑟 / 2) ∈ ℝ)) → ((((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ ((𝐹‘𝑘)𝐷𝑦) < (𝑟 / 2)) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < ((𝑟 / 2) + (𝑟 / 2))))
308	303, 305, 306, 306, 307	syl22anc 838	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ ((𝐹‘𝑘)𝐷𝑦) < (𝑟 / 2)) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < ((𝑟 / 2) + (𝑟 / 2))))
309	296, 308	mpan2d 694	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < ((𝑟 / 2) + (𝑟 / 2))))
310	285	rpcnd 13004	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝑟 ∈ ℂ)
311	310	2halvesd 12435	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((𝑟 / 2) + (𝑟 / 2)) = 𝑟)
312	311	breq2d 5122	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < ((𝑟 / 2) + (𝑟 / 2)) ↔ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < 𝑟))
313	309, 312	sylibd 239	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < 𝑟))
314		mettri2 24236	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ ((𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑛) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹‘𝑛)𝐷𝑦) ≤ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)))
315	297, 293, 301, 288, 314	syl13anc 1374	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((𝐹‘𝑛)𝐷𝑦) ≤ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)))
316		metcl 24227	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘𝑛) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝐹‘𝑛)𝐷𝑦) ∈ ℝ)
317	297, 301, 288, 316	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((𝐹‘𝑛)𝐷𝑦) ∈ ℝ)
318	303, 305	readdcld 11210	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) ∈ ℝ)
319	285	rpred 13002	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝑟 ∈ ℝ)
320		lelttr 11271	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑛)𝐷𝑦) ∈ ℝ ∧ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) ∈ ℝ ∧ 𝑟 ∈ ℝ) → ((((𝐹‘𝑛)𝐷𝑦) ≤ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) ∧ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < 𝑟) → ((𝐹‘𝑛)𝐷𝑦) < 𝑟))
321	317, 318, 319, 320	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((((𝐹‘𝑛)𝐷𝑦) ≤ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) ∧ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < 𝑟) → ((𝐹‘𝑛)𝐷𝑦) < 𝑟))
322	315, 321	mpand 695	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < 𝑟 → ((𝐹‘𝑛)𝐷𝑦) < 𝑟))
323	313, 322	syld 47	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ((𝐹‘𝑛)𝐷𝑦) < 𝑟))
324	323	anassrs 467	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ (𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) ∧ 𝑛 ∈ (ℤ≥‘𝑘)) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ((𝐹‘𝑛)𝐷𝑦) < 𝑟))
325	324	ralimdva 3146	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ (𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) → (∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))
326	325	expr 456	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ 𝑘 ∈ (ℤ≥‘𝑚)) → ((𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) → (∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)))
327	326	com23 86	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ 𝑘 ∈ (ℤ≥‘𝑚)) → (∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ((𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) → ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)))
328	327	impd 410	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ 𝑘 ∈ (ℤ≥‘𝑚)) → ((∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))
329	328	reximdva 3147	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (∃𝑘 ∈ (ℤ≥‘𝑚)(∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))
330		ssrexv 4019	. . . . . . . . . . . . 13 ⊢ ((ℤ≥‘𝑚) ⊆ ℕ → (∃𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟 → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))
331	282, 329, 330	sylsyld 61	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (∃𝑘 ∈ (ℤ≥‘𝑚)(∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))
332	220, 331	syldanl 602	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (∃𝑘 ∈ (ℤ≥‘𝑚)(∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))
333	280, 332	syl5 34	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → ((∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ ∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))
334	279, 333	mpan2d 694	. . . . . . . . 9 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))
335	334	anassrs 467	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ 𝑟 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) → (∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))
336	335	rexlimdva 3135	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ 𝑟 ∈ ℝ+) → (∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))
337	237, 336	mpd 15	. . . . . 6 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ 𝑟 ∈ ℝ+) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)
338	337	ralrimiva 3126	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∀𝑟 ∈ ℝ+ ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)
339		eqidd 2731	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) = (𝐹‘𝑛))
340	5, 4, 129, 222, 339, 9	lmmbrf 25169	. . . . . 6 ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑦 ↔ (𝑦 ∈ 𝑋 ∧ ∀𝑟 ∈ ℝ+ ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)))
341	340	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) → (𝐹(⇝𝑡‘𝐽)𝑦 ↔ (𝑦 ∈ 𝑋 ∧ ∀𝑟 ∈ ℝ+ ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)))
342	220, 338, 341	mpbir2and 713	. . . 4 ⊢ ((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) → 𝐹(⇝𝑡‘𝐽)𝑦)
343	200, 342	sylan2br 595	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))}) → 𝐹(⇝𝑡‘𝐽)𝑦)
344		releldm 5911	. . 3 ⊢ ((Rel (⇝𝑡‘𝐽) ∧ 𝐹(⇝𝑡‘𝐽)𝑦) → 𝐹 ∈ dom (⇝𝑡‘𝐽))
345	189, 343, 344	sylancr 587	. 2 ⊢ ((𝜑 ∧ 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))}) → 𝐹 ∈ dom (⇝𝑡‘𝐽))
346	188, 345	exlimddv 1935	1 ⊢ (𝜑 → 𝐹 ∈ dom (⇝𝑡‘𝐽))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2109  {cab 2708   ≠ wne 2926  ∀wral 3045  ∃wrex 3054  Vcvv 3450   ∪ cun 3915   ∩ cin 3916   ⊆ wss 3917  ∅c0 4299  𝒫 cpw 4566  {csn 4592  ∪ cuni 4874  ∩ cint 4913   class class class wbr 5110  dom cdm 5641  ran crn 5642   “ cima 5644  Rel wrel 5646  Fun wfun 6508   Fn wfn 6509  ⟶wf 6510  ‘cfv 6514  (class class class)co 7390   ↑_pm cpm 8803  Fincfn 8921  ficfi 9368  ℂcc 11073  ℝcr 11074  0cc0 11075  1c1 11076   + caddc 11078  ℝ^*cxr 11214   < clt 11215   ≤ cle 11216   / cdiv 11842  ℕcn 12193  2c2 12248  ℤcz 12536  ℤ_≥cuz 12800  ℝ⁺crp 12958  ∞Metcxmet 21256  Metcmet 21257  ballcbl 21258  MetOpencmopn 21261  Topctop 22787  Clsdccld 22910  clsccl 22912  ⇝_𝑡clm 23120  Compccmp 23280  Cauccau 25160

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152  ax-pre-sup 11153

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-int 4914  df-iun 4960  df-iin 4961  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-om 7846  df-1st 7971  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-1o 8437  df-er 8674  df-map 8804  df-pm 8805  df-en 8922  df-dom 8923  df-sdom 8924  df-fin 8925  df-fi 9369  df-sup 9400  df-inf 9401  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221  df-sub 11414  df-neg 11415  df-div 11843  df-nn 12194  df-2 12256  df-n0 12450  df-z 12537  df-uz 12801  df-q 12915  df-rp 12959  df-xneg 13079  df-xadd 13080  df-xmul 13081  df-topgen 17413  df-psmet 21263  df-xmet 21264  df-met 21265  df-bl 21266  df-mopn 21267  df-top 22788  df-topon 22805  df-bases 22840  df-cld 22913  df-ntr 22914  df-cls 22915  df-lm 23123  df-cmp 23281  df-cau 25163

This theorem is referenced by:  heibor1  37811