Theorem heibor1lem 36268

Description: Lemma for heibor1 36269. 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 23687	. . . . . . . . . 10 ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
4	2, 3	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))
5		heibor.1	. . . . . . . . . 10 ⊢ 𝐽 = (MetOpen‘𝐷)
6	5	mopntop 23793	. . . . . . . . 9 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
7	4, 6	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ Top)
8		imassrn 6024	. . . . . . . . 9 ⊢ (𝐹 “ 𝑢) ⊆ ran 𝐹
9		heibor1.6	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:ℕ⟶𝑋)
10	9	frnd 6676	. . . . . . . . . 10 ⊢ (𝜑 → ran 𝐹 ⊆ 𝑋)
11	5	mopnuni 23794	. . . . . . . . . . 11 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽)
12	4, 11	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 = ∪ 𝐽)
13	10, 12	sseqtrd 3984	. . . . . . . . 9 ⊢ (𝜑 → ran 𝐹 ⊆ ∪ 𝐽)
14	8, 13	sstrid 3955	. . . . . . . 8 ⊢ (𝜑 → (𝐹 “ 𝑢) ⊆ ∪ 𝐽)
15		eqid 2736	. . . . . . . . 9 ⊢ ∪ 𝐽 = ∪ 𝐽
16	15	clscld 22398	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ (𝐹 “ 𝑢) ⊆ ∪ 𝐽) → ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∈ (Clsd‘𝐽))
17	7, 14, 16	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∈ (Clsd‘𝐽))
18		eleq1a 2833	. . . . . . 7 ⊢ (((cls‘𝐽)‘(𝐹 “ 𝑢)) ∈ (Clsd‘𝐽) → (𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑘 ∈ (Clsd‘𝐽)))
19	17, 18	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑘 ∈ (Clsd‘𝐽)))
20	19	rexlimdvw 3157	. . . . 5 ⊢ (𝜑 → (∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑘 ∈ (Clsd‘𝐽)))
21	20	abssdv 4025	. . . 4 ⊢ (𝜑 → {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ⊆ (Clsd‘𝐽))
22		fvex 6855	. . . . 5 ⊢ (Clsd‘𝐽) ∈ V
23	22	elpw2 5302	. . . 4 ⊢ ({𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∈ 𝒫 (Clsd‘𝐽) ↔ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ⊆ (Clsd‘𝐽))
24	21, 23	sylibr 233	. . 3 ⊢ (𝜑 → {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∈ 𝒫 (Clsd‘𝐽))
25		elin 3926	. . . . . . 7 ⊢ (𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∩ Fin) ↔ (𝑟 ∈ 𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∧ 𝑟 ∈ Fin))
26		velpw 4565	. . . . . . . . 9 ⊢ (𝑟 ∈ 𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ↔ 𝑟 ⊆ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))})
27		ssabral 4019	. . . . . . . . 9 ⊢ (𝑟 ⊆ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ↔ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))
28	26, 27	bitri 274	. . . . . . . 8 ⊢ (𝑟 ∈ 𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ↔ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))
29	28	anbi1i 624	. . . . . . 7 ⊢ ((𝑟 ∈ 𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∧ 𝑟 ∈ Fin) ↔ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin))
30	25, 29	bitri 274	. . . . . 6 ⊢ (𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∩ Fin) ↔ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin))
31		raleq 3309	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ∅ → (∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∀𝑘 ∈ ∅ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))))
32	31	anbi2d 629	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → ((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) ↔ (𝜑 ∧ ∀𝑘 ∈ ∅ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))))
33		inteq 4910	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = ∅ → ∩ 𝑚 = ∩ ∅)
34	33	sseq2d 3976	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ∅ → ((𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ (𝐹 “ 𝑘) ⊆ ∩ ∅))
35	34	rexbidv 3175	. . . . . . . . . . . . 13 ⊢ (𝑚 = ∅ → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ ∅))
36	32, 35	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑚 = ∅ → (((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚) ↔ ((𝜑 ∧ ∀𝑘 ∈ ∅ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ ∅)))
37		raleq 3309	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑦 → (∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∀𝑘 ∈ 𝑦 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))))
38	37	anbi2d 629	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑦 → ((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) ↔ (𝜑 ∧ ∀𝑘 ∈ 𝑦 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))))
39		inteq 4910	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑦 → ∩ 𝑚 = ∩ 𝑦)
40	39	sseq2d 3976	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑦 → ((𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ (𝐹 “ 𝑘) ⊆ ∩ 𝑦))
41	40	rexbidv 3175	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑦 → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦))
42	38, 41	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑦 → (((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚) ↔ ((𝜑 ∧ ∀𝑘 ∈ 𝑦 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦)))
43		raleq 3309	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝑦 ∪ {𝑛}) → (∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))))
44	43	anbi2d 629	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝑦 ∪ {𝑛}) → ((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) ↔ (𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))))
45		inteq 4910	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝑦 ∪ {𝑛}) → ∩ 𝑚 = ∩ (𝑦 ∪ {𝑛}))
46	45	sseq2d 3976	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝑦 ∪ {𝑛}) → ((𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ (𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛})))
47	46	rexbidv 3175	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝑦 ∪ {𝑛}) → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛})))
48	44, 47	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝑦 ∪ {𝑛}) → (((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚) ↔ ((𝜑 ∧ ∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛}))))
49		raleq 3309	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑟 → (∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))))
50	49	anbi2d 629	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑟 → ((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) ↔ (𝜑 ∧ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))))
51		inteq 4910	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑟 → ∩ 𝑚 = ∩ 𝑟)
52	51	sseq2d 3976	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑟 → ((𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ (𝐹 “ 𝑘) ⊆ ∩ 𝑟))
53	52	rexbidv 3175	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑟 → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚 ↔ ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑟))
54	50, 53	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑟 → (((𝜑 ∧ ∀𝑘 ∈ 𝑚 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑚) ↔ ((𝜑 ∧ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑟)))
55		uzf 12766	. . . . . . . . . . . . . . . 16 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
56		ffn 6668	. . . . . . . . . . . . . . . 16 ⊢ (ℤ≥:ℤ⟶𝒫 ℤ → ℤ≥ Fn ℤ)
57	55, 56	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ℤ≥ Fn ℤ
58		0z 12510	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℤ
59		fnfvelrn 7031	. . . . . . . . . . . . . . 15 ⊢ ((ℤ≥ Fn ℤ ∧ 0 ∈ ℤ) → (ℤ≥‘0) ∈ ran ℤ≥)
60	57, 58, 59	mp2an 690	. . . . . . . . . . . . . 14 ⊢ (ℤ≥‘0) ∈ ran ℤ≥
61		ssv 3968	. . . . . . . . . . . . . . 15 ⊢ (𝐹 “ (ℤ≥‘0)) ⊆ V
62		int0 4923	. . . . . . . . . . . . . . 15 ⊢ ∩ ∅ = V
63	61, 62	sseqtrri 3981	. . . . . . . . . . . . . 14 ⊢ (𝐹 “ (ℤ≥‘0)) ⊆ ∩ ∅
64		imaeq2 6009	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (ℤ≥‘0) → (𝐹 “ 𝑘) = (𝐹 “ (ℤ≥‘0)))
65	64	sseq1d 3975	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (ℤ≥‘0) → ((𝐹 “ 𝑘) ⊆ ∩ ∅ ↔ (𝐹 “ (ℤ≥‘0)) ⊆ ∩ ∅))
66	65	rspcev 3581	. . . . . . . . . . . . . 14 ⊢ (((ℤ≥‘0) ∈ ran ℤ≥ ∧ (𝐹 “ (ℤ≥‘0)) ⊆ ∩ ∅) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ ∅)
67	60, 63, 66	mp2an 690	. . . . . . . . . . . . 13 ⊢ ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ ∅
68	67	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ∀𝑘 ∈ ∅ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ ∅)
69		ssun1 4132	. . . . . . . . . . . . . . . . 17 ⊢ 𝑦 ⊆ (𝑦 ∪ {𝑛})
70		ssralv 4010	. . . . . . . . . . . . . . . . 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 4133	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑛} ⊆ (𝑦 ∪ {𝑛})
75		ssralv 4010	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑛} ⊆ (𝑦 ∪ {𝑛}) → (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → ∀𝑘 ∈ {𝑛}∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))))
76	74, 75	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → ∀𝑘 ∈ {𝑛}∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))
77		vex 3449	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑛 ∈ V
78		eqeq1 2740	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑛 → (𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ 𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢))))
79	78	rexbidv 3175	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑛 → (∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∃𝑢 ∈ ran ℤ≥𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢))))
80	77, 79	ralsn 4642	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑘 ∈ {𝑛}∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∃𝑢 ∈ ran ℤ≥𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))
81	76, 80	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → ∃𝑢 ∈ ran ℤ≥𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)))
82		uzin2 15229	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑢 ∈ ran ℤ≥ ∧ 𝑘 ∈ ran ℤ≥) → (𝑢 ∩ 𝑘) ∈ ran ℤ≥)
83	8, 10	sstrid 3955	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐹 “ 𝑢) ⊆ 𝑋)
84	83, 12	sseqtrd 3984	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐹 “ 𝑢) ⊆ ∪ 𝐽)
85	15	sscls 22407	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐽 ∈ Top ∧ (𝐹 “ 𝑢) ⊆ ∪ 𝐽) → (𝐹 “ 𝑢) ⊆ ((cls‘𝐽)‘(𝐹 “ 𝑢)))
86	7, 84, 85	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐹 “ 𝑢) ⊆ ((cls‘𝐽)‘(𝐹 “ 𝑢)))
87		sseq2 3970	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → ((𝐹 “ 𝑢) ⊆ 𝑛 ↔ (𝐹 “ 𝑢) ⊆ ((cls‘𝐽)‘(𝐹 “ 𝑢))))
88	86, 87	syl5ibrcom 246	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → (𝐹 “ 𝑢) ⊆ 𝑛))
89		inss2 4189	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑢 ∩ 𝑘) ⊆ 𝑘
90		inss1 4188	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑢 ∩ 𝑘) ⊆ 𝑢
91		imass2 6054	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑢 ∩ 𝑘) ⊆ 𝑘 → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (𝐹 “ 𝑘))
92		imass2 6054	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑢 ∩ 𝑘) ⊆ 𝑢 → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (𝐹 “ 𝑢))
93	91, 92	anim12i 613	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑢 ∩ 𝑘) ⊆ 𝑘 ∧ (𝑢 ∩ 𝑘) ⊆ 𝑢) → ((𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (𝐹 “ 𝑘) ∧ (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (𝐹 “ 𝑢)))
94		ssin 4190	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (𝐹 “ 𝑘) ∧ (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (𝐹 “ 𝑢)) ↔ (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ((𝐹 “ 𝑘) ∩ (𝐹 “ 𝑢)))
95	93, 94	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑢 ∩ 𝑘) ⊆ 𝑘 ∧ (𝑢 ∩ 𝑘) ⊆ 𝑢) → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ((𝐹 “ 𝑘) ∩ (𝐹 “ 𝑢)))
96	89, 90, 95	mp2an 690	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ((𝐹 “ 𝑘) ∩ (𝐹 “ 𝑢))
97		ss2in 4196	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐹 “ 𝑘) ⊆ ∩ 𝑦 ∧ (𝐹 “ 𝑢) ⊆ 𝑛) → ((𝐹 “ 𝑘) ∩ (𝐹 “ 𝑢)) ⊆ (∩ 𝑦 ∩ 𝑛))
98	96, 97	sstrid 3955	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐹 “ 𝑘) ⊆ ∩ 𝑦 ∧ (𝐹 “ 𝑢) ⊆ 𝑛) → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ (∩ 𝑦 ∩ 𝑛))
99	77	intunsn 4950	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ∩ (𝑦 ∪ {𝑛}) = (∩ 𝑦 ∩ 𝑛)
100	98, 99	sseqtrrdi 3995	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 “ 𝑘) ⊆ ∩ 𝑦 ∧ (𝐹 “ 𝑢) ⊆ 𝑛) → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ∩ (𝑦 ∪ {𝑛}))
101	100	expcom 414	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹 “ 𝑢) ⊆ 𝑛 → ((𝐹 “ 𝑘) ⊆ ∩ 𝑦 → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ∩ (𝑦 ∪ {𝑛})))
102	88, 101	syl6 35	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → ((𝐹 “ 𝑘) ⊆ ∩ 𝑦 → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ∩ (𝑦 ∪ {𝑛}))))
103	102	impd 411	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ (𝐹 “ 𝑘) ⊆ ∩ 𝑦) → (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ∩ (𝑦 ∪ {𝑛})))
104		imaeq2 6009	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑚 = (𝑢 ∩ 𝑘) → (𝐹 “ 𝑚) = (𝐹 “ (𝑢 ∩ 𝑘)))
105	104	sseq1d 3975	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 = (𝑢 ∩ 𝑘) → ((𝐹 “ 𝑚) ⊆ ∩ (𝑦 ∪ {𝑛}) ↔ (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ∩ (𝑦 ∪ {𝑛})))
106	105	rspcev 3581	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑢 ∩ 𝑘) ∈ ran ℤ≥ ∧ (𝐹 “ (𝑢 ∩ 𝑘)) ⊆ ∩ (𝑦 ∪ {𝑛})) → ∃𝑚 ∈ ran ℤ≥(𝐹 “ 𝑚) ⊆ ∩ (𝑦 ∪ {𝑛}))
107	106	expcom 414	. . . . . . . . . . . . . . . . . . . . . 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 3204	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (∃𝑢 ∈ ran ℤ≥∃𝑘 ∈ ran ℤ≥(𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ (𝐹 “ 𝑘) ⊆ ∩ 𝑦) → ∃𝑚 ∈ ran ℤ≥(𝐹 “ 𝑚) ⊆ ∩ (𝑦 ∪ {𝑛})))
112		reeanv 3217	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑢 ∈ ran ℤ≥∃𝑘 ∈ ran ℤ≥(𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ (𝐹 “ 𝑘) ⊆ ∩ 𝑦) ↔ (∃𝑢 ∈ ran ℤ≥𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦))
113		imaeq2 6009	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑘 → (𝐹 “ 𝑚) = (𝐹 “ 𝑘))
114	113	sseq1d 3975	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑘 → ((𝐹 “ 𝑚) ⊆ ∩ (𝑦 ∪ {𝑛}) ↔ (𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛})))
115	114	cbvrexvw 3226	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑚 ∈ ran ℤ≥(𝐹 “ 𝑚) ⊆ ∩ (𝑦 ∪ {𝑛}) ↔ ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛}))
116	111, 112, 115	3imtr3g 294	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((∃𝑢 ∈ ran ℤ≥𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛})))
117	116	expd 416	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∃𝑢 ∈ ran ℤ≥𝑛 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦 → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛}))))
118	81, 117	syl5 34	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (∀𝑘 ∈ (𝑦 ∪ {𝑛})∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑦 → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ (𝑦 ∪ {𝑛}))))
119	118	imp 407	. . . . . . . . . . . . . 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 9108	. . . . . . . . . . 11 ⊢ (𝑟 ∈ Fin → ((𝜑 ∧ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑟))
123	122	com12 32	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))) → (𝑟 ∈ Fin → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑟))
124	123	impr 455	. . . . . . . . 9 ⊢ ((𝜑 ∧ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin)) → ∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑟)
125	9	ffnd 6669	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 Fn ℕ)
126		inss1 4188	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∩ ℕ) ⊆ 𝑘
127		imass2 6054	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∩ ℕ) ⊆ 𝑘 → (𝐹 “ (𝑘 ∩ ℕ)) ⊆ (𝐹 “ 𝑘))
128	126, 127	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (𝐹 “ (𝑘 ∩ ℕ)) ⊆ (𝐹 “ 𝑘)
129		nnuz 12806	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℕ = (ℤ≥‘1)
130		1z 12533	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ ℤ
131		fnfvelrn 7031	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℤ≥ Fn ℤ ∧ 1 ∈ ℤ) → (ℤ≥‘1) ∈ ran ℤ≥)
132	57, 130, 131	mp2an 690	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℤ≥‘1) ∈ ran ℤ≥
133	129, 132	eqeltri 2834	. . . . . . . . . . . . . . . . . . 19 ⊢ ℕ ∈ ran ℤ≥
134		uzin2 15229	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ran ℤ≥ ∧ ℕ ∈ ran ℤ≥) → (𝑘 ∩ ℕ) ∈ ran ℤ≥)
135	133, 134	mpan2 689	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ran ℤ≥ → (𝑘 ∩ ℕ) ∈ ran ℤ≥)
136		uzn0 12780	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∩ ℕ) ∈ ran ℤ≥ → (𝑘 ∩ ℕ) ≠ ∅)
137	135, 136	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ran ℤ≥ → (𝑘 ∩ ℕ) ≠ ∅)
138		n0 4306	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∩ ℕ) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝑘 ∩ ℕ))
139	137, 138	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ran ℤ≥ → ∃𝑦 𝑦 ∈ (𝑘 ∩ ℕ))
140		fnfun 6602	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 Fn ℕ → Fun 𝐹)
141		inss2 4189	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∩ ℕ) ⊆ ℕ
142		fndm 6605	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹 Fn ℕ → dom 𝐹 = ℕ)
143	141, 142	sseqtrrid 3997	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 Fn ℕ → (𝑘 ∩ ℕ) ⊆ dom 𝐹)
144		funfvima2 7181	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝐹 ∧ (𝑘 ∩ ℕ) ⊆ dom 𝐹) → (𝑦 ∈ (𝑘 ∩ ℕ) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑘 ∩ ℕ))))
145	140, 143, 144	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 Fn ℕ → (𝑦 ∈ (𝑘 ∩ ℕ) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑘 ∩ ℕ))))
146		ne0i 4294	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑦) ∈ (𝐹 “ (𝑘 ∩ ℕ)) → (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅)
147	145, 146	syl6 35	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 Fn ℕ → (𝑦 ∈ (𝑘 ∩ ℕ) → (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅))
148	147	exlimdv 1936	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 Fn ℕ → (∃𝑦 𝑦 ∈ (𝑘 ∩ ℕ) → (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅))
149	139, 148	syl5 34	. . . . . . . . . . . . . . 15 ⊢ (𝐹 Fn ℕ → (𝑘 ∈ ran ℤ≥ → (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅))
150	149	imp 407	. . . . . . . . . . . . . 14 ⊢ ((𝐹 Fn ℕ ∧ 𝑘 ∈ ran ℤ≥) → (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅)
151		ssn0 4360	. . . . . . . . . . . . . 14 ⊢ (((𝐹 “ (𝑘 ∩ ℕ)) ⊆ (𝐹 “ 𝑘) ∧ (𝐹 “ (𝑘 ∩ ℕ)) ≠ ∅) → (𝐹 “ 𝑘) ≠ ∅)
152	128, 150, 151	sylancr 587	. . . . . . . . . . . . 13 ⊢ ((𝐹 Fn ℕ ∧ 𝑘 ∈ ran ℤ≥) → (𝐹 “ 𝑘) ≠ ∅)
153		ssn0 4360	. . . . . . . . . . . . . 14 ⊢ (((𝐹 “ 𝑘) ⊆ ∩ 𝑟 ∧ (𝐹 “ 𝑘) ≠ ∅) → ∩ 𝑟 ≠ ∅)
154	153	expcom 414	. . . . . . . . . . . . 13 ⊢ ((𝐹 “ 𝑘) ≠ ∅ → ((𝐹 “ 𝑘) ⊆ ∩ 𝑟 → ∩ 𝑟 ≠ ∅))
155	152, 154	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐹 Fn ℕ ∧ 𝑘 ∈ ran ℤ≥) → ((𝐹 “ 𝑘) ⊆ ∩ 𝑟 → ∩ 𝑟 ≠ ∅))
156	155	rexlimdva 3152	. . . . . . . . . . 11 ⊢ (𝐹 Fn ℕ → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑟 → ∩ 𝑟 ≠ ∅))
157	125, 156	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑟 → ∩ 𝑟 ≠ ∅))
158	157	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin)) → (∃𝑘 ∈ ran ℤ≥(𝐹 “ 𝑘) ⊆ ∩ 𝑟 → ∩ 𝑟 ≠ ∅))
159	124, 158	mpd 15	. . . . . . . 8 ⊢ ((𝜑 ∧ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin)) → ∩ 𝑟 ≠ ∅)
160	159	necomd 2999	. . . . . . 7 ⊢ ((𝜑 ∧ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin)) → ∅ ≠ ∩ 𝑟)
161	160	neneqd 2948	. . . . . 6 ⊢ ((𝜑 ∧ (∀𝑘 ∈ 𝑟 ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∧ 𝑟 ∈ Fin)) → ¬ ∅ = ∩ 𝑟)
162	30, 161	sylan2b 594	. . . . 5 ⊢ ((𝜑 ∧ 𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∩ Fin)) → ¬ ∅ = ∩ 𝑟)
163	162	nrexdv 3146	. . . 4 ⊢ (𝜑 → ¬ ∃𝑟 ∈ (𝒫 {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∩ Fin)∅ = ∩ 𝑟)
164		0ex 5264	. . . . 5 ⊢ ∅ ∈ V
165		zex 12508	. . . . . . . 8 ⊢ ℤ ∈ V
166	165	pwex 5335	. . . . . . 7 ⊢ 𝒫 ℤ ∈ V
167		frn 6675	. . . . . . . 8 ⊢ (ℤ≥:ℤ⟶𝒫 ℤ → ran ℤ≥ ⊆ 𝒫 ℤ)
168	55, 167	ax-mp 5	. . . . . . 7 ⊢ ran ℤ≥ ⊆ 𝒫 ℤ
169	166, 168	ssexi 5279	. . . . . 6 ⊢ ran ℤ≥ ∈ V
170	169	abrexex 7895	. . . . 5 ⊢ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ∈ V
171		elfi 9349	. . . . 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 22746	. . . . . 6 ⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top)
175		cmpfi 22759	. . . . . 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 6842	. . . . . . . 8 ⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → (fi‘𝑚) = (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))}))
179	178	eleq2d 2823	. . . . . . 7 ⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → (∅ ∈ (fi‘𝑚) ↔ ∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))})))
180	179	notbid 317	. . . . . 6 ⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → (¬ ∅ ∈ (fi‘𝑚) ↔ ¬ ∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))})))
181		inteq 4910	. . . . . . . 8 ⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → ∩ 𝑚 = ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))})
182	181	neeq1d 3003	. . . . . . 7 ⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → (∩ 𝑚 ≠ ∅ ↔ ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ≠ ∅))
183		n0 4306	. . . . . . 7 ⊢ (∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ≠ ∅ ↔ ∃𝑦 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))})
184	182, 183	bitrdi 286	. . . . . 6 ⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → (∩ 𝑚 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))}))
185	180, 184	imbi12d 344	. . . . 5 ⊢ (𝑚 = {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → ((¬ ∅ ∈ (fi‘𝑚) → ∩ 𝑚 ≠ ∅) ↔ (¬ ∅ ∈ (fi‘{𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))}) → ∃𝑦 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))})))
186	185	rspccv 3578	. . . 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 22581	. . 3 ⊢ Rel (⇝𝑡‘𝐽)
190		r19.23v 3179	. . . . . 6 ⊢ (∀𝑢 ∈ ran ℤ≥(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘) ↔ (∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘))
191	190	albii 1821	. . . . 5 ⊢ (∀𝑘∀𝑢 ∈ ran ℤ≥(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘) ↔ ∀𝑘(∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘))
192		fvex 6855	. . . . . . . 8 ⊢ ((cls‘𝐽)‘(𝐹 “ 𝑢)) ∈ V
193		eleq2 2826	. . . . . . . 8 ⊢ (𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → (𝑦 ∈ 𝑘 ↔ 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))))
194	192, 193	ceqsalv 3481	. . . . . . 7 ⊢ (∀𝑘(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘) ↔ 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢)))
195	194	ralbii 3096	. . . . . 6 ⊢ (∀𝑢 ∈ ran ℤ≥∀𝑘(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘) ↔ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢)))
196		ralcom4 3269	. . . . . 6 ⊢ (∀𝑢 ∈ ran ℤ≥∀𝑘(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘) ↔ ∀𝑘∀𝑢 ∈ ran ℤ≥(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘))
197	195, 196	bitr3i 276	. . . . 5 ⊢ (∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∀𝑘∀𝑢 ∈ ran ℤ≥(𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘))
198		vex 3449	. . . . . 6 ⊢ 𝑦 ∈ V
199	198	elintab 4919	. . . . 5 ⊢ (𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ↔ ∀𝑘(∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) → 𝑦 ∈ 𝑘))
200	191, 197, 199	3bitr4i 302	. . . 4 ⊢ (∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))})
201		eqid 2736	. . . . . . . . . . 11 ⊢ ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ ℕ))
202		imaeq2 6009	. . . . . . . . . . . . 13 ⊢ (𝑢 = ℕ → (𝐹 “ 𝑢) = (𝐹 “ ℕ))
203	202	fveq2d 6846	. . . . . . . . . . . 12 ⊢ (𝑢 = ℕ → ((cls‘𝐽)‘(𝐹 “ 𝑢)) = ((cls‘𝐽)‘(𝐹 “ ℕ)))
204	203	rspceeqv 3595	. . . . . . . . . . 11 ⊢ ((ℕ ∈ ran ℤ≥ ∧ ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ ℕ))) → ∃𝑢 ∈ ran ℤ≥((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ 𝑢)))
205	133, 201, 204	mp2an 690	. . . . . . . . . 10 ⊢ ∃𝑢 ∈ ran ℤ≥((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ 𝑢))
206		fvex 6855	. . . . . . . . . . 11 ⊢ ((cls‘𝐽)‘(𝐹 “ ℕ)) ∈ V
207		eqeq1 2740	. . . . . . . . . . . 12 ⊢ (𝑘 = ((cls‘𝐽)‘(𝐹 “ ℕ)) → (𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ 𝑢))))
208	207	rexbidv 3175	. . . . . . . . . . 11 ⊢ (𝑘 = ((cls‘𝐽)‘(𝐹 “ ℕ)) → (∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ ∃𝑢 ∈ ran ℤ≥((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ 𝑢))))
209	206, 208	elab 3630	. . . . . . . . . 10 ⊢ (((cls‘𝐽)‘(𝐹 “ ℕ)) ∈ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ↔ ∃𝑢 ∈ ran ℤ≥((cls‘𝐽)‘(𝐹 “ ℕ)) = ((cls‘𝐽)‘(𝐹 “ 𝑢)))
210	205, 209	mpbir 230	. . . . . . . . 9 ⊢ ((cls‘𝐽)‘(𝐹 “ ℕ)) ∈ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))}
211		intss1 4924	. . . . . . . . 9 ⊢ (((cls‘𝐽)‘(𝐹 “ ℕ)) ∈ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} → ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ⊆ ((cls‘𝐽)‘(𝐹 “ ℕ)))
212	210, 211	ax-mp 5	. . . . . . . 8 ⊢ ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ⊆ ((cls‘𝐽)‘(𝐹 “ ℕ))
213		imassrn 6024	. . . . . . . . . . 11 ⊢ (𝐹 “ ℕ) ⊆ ran 𝐹
214	213, 13	sstrid 3955	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹 “ ℕ) ⊆ ∪ 𝐽)
215	15	clsss3 22410	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ (𝐹 “ ℕ) ⊆ ∪ 𝐽) → ((cls‘𝐽)‘(𝐹 “ ℕ)) ⊆ ∪ 𝐽)
216	7, 214, 215	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → ((cls‘𝐽)‘(𝐹 “ ℕ)) ⊆ ∪ 𝐽)
217	216, 12	sseqtrrd 3985	. . . . . . . 8 ⊢ (𝜑 → ((cls‘𝐽)‘(𝐹 “ ℕ)) ⊆ 𝑋)
218	212, 217	sstrid 3955	. . . . . . 7 ⊢ (𝜑 → ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))} ⊆ 𝑋)
219	218	sselda 3944	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))}) → 𝑦 ∈ 𝑋)
220	200, 219	sylan2b 594	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) → 𝑦 ∈ 𝑋)
221		heibor1.5	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ∈ (Cau‘𝐷))
222		1zzd 12534	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 ∈ ℤ)
223	129, 4, 222	iscau3 24642	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦))))
224	221, 223	mpbid 231	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ ∀𝑦 ∈ ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦)))
225	224	simprd 496	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑦 ∈ ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦))
226		simp3 1138	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦) → ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦)
227	226	ralimi 3086	. . . . . . . . . . . 12 ⊢ (∀𝑘 ∈ (ℤ≥‘𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦) → ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦)
228	227	reximi 3087	. . . . . . . . . . 11 ⊢ (∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦) → ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦)
229	228	ralimi 3086	. . . . . . . . . 10 ⊢ (∀𝑦 ∈ ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦) → ∀𝑦 ∈ ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦)
230	225, 229	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑦 ∈ ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦)
231	230	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∀𝑦 ∈ ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦)
232		rphalfcl 12942	. . . . . . . 8 ⊢ (𝑟 ∈ ℝ+ → (𝑟 / 2) ∈ ℝ+)
233		breq2 5109	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑟 / 2) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦 ↔ ((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2)))
234	233	2ralbidv 3212	. . . . . . . . . 10 ⊢ (𝑦 = (𝑟 / 2) → (∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦 ↔ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2)))
235	234	rexbidv 3175	. . . . . . . . 9 ⊢ (𝑦 = (𝑟 / 2) → (∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦 ↔ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2)))
236	235	rspccva 3580	. . . . . . . 8 ⊢ ((∀𝑦 ∈ ℝ+ ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < 𝑦 ∧ (𝑟 / 2) ∈ ℝ+) → ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2))
237	231, 232, 236	syl2an 596	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ 𝑟 ∈ ℝ+) → ∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2))
238	9	ffund 6672	. . . . . . . . . . . 12 ⊢ (𝜑 → Fun 𝐹)
239	238	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → Fun 𝐹)
240	7	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → 𝐽 ∈ Top)
241		imassrn 6024	. . . . . . . . . . . . . 14 ⊢ (𝐹 “ (ℤ≥‘𝑚)) ⊆ ran 𝐹
242	241, 13	sstrid 3955	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹 “ (ℤ≥‘𝑚)) ⊆ ∪ 𝐽)
243	242	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (𝐹 “ (ℤ≥‘𝑚)) ⊆ ∪ 𝐽)
244		nnz 12520	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℤ)
245		fnfvelrn 7031	. . . . . . . . . . . . . . 15 ⊢ ((ℤ≥ Fn ℤ ∧ 𝑚 ∈ ℤ) → (ℤ≥‘𝑚) ∈ ran ℤ≥)
246	57, 244, 245	sylancr 587	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ → (ℤ≥‘𝑚) ∈ ran ℤ≥)
247	246	ad2antll 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (ℤ≥‘𝑚) ∈ ran ℤ≥)
248		simplr 767	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢)))
249		imaeq2 6009	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = (ℤ≥‘𝑚) → (𝐹 “ 𝑢) = (𝐹 “ (ℤ≥‘𝑚)))
250	249	fveq2d 6846	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = (ℤ≥‘𝑚) → ((cls‘𝐽)‘(𝐹 “ 𝑢)) = ((cls‘𝐽)‘(𝐹 “ (ℤ≥‘𝑚))))
251	250	eleq2d 2823	. . . . . . . . . . . . . 14 ⊢ (𝑢 = (ℤ≥‘𝑚) → (𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢)) ↔ 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ (ℤ≥‘𝑚)))))
252	251	rspcv 3577	. . . . . . . . . . . . 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 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → 𝑦 ∈ 𝑋)
256	232	ad2antrl 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (𝑟 / 2) ∈ ℝ+)
257	256	rpxrd 12958	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (𝑟 / 2) ∈ ℝ*)
258	5	blopn 23856	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ (𝑟 / 2) ∈ ℝ*) → (𝑦(ball‘𝐷)(𝑟 / 2)) ∈ 𝐽)
259	254, 255, 257, 258	syl3anc 1371	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (𝑦(ball‘𝐷)(𝑟 / 2)) ∈ 𝐽)
260		blcntr 23766	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ (𝑟 / 2) ∈ ℝ+) → 𝑦 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
261	254, 255, 256, 260	syl3anc 1371	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → 𝑦 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
262	15	clsndisj 22426	. . . . . . . . . . . 12 ⊢ (((𝐽 ∈ Top ∧ (𝐹 “ (ℤ≥‘𝑚)) ⊆ ∪ 𝐽 ∧ 𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ (ℤ≥‘𝑚)))) ∧ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∈ 𝐽 ∧ 𝑦 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) → ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) ≠ ∅)
263	240, 243, 253, 259, 261, 262	syl32anc 1378	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) ≠ ∅)
264		n0 4306	. . . . . . . . . . . 12 ⊢ (((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) ≠ ∅ ↔ ∃𝑛 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))))
265		inss2 4189	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) ⊆ (𝐹 “ (ℤ≥‘𝑚))
266	265	sseli 3940	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) → 𝑛 ∈ (𝐹 “ (ℤ≥‘𝑚)))
267		fvelima 6908	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝐹 ∧ 𝑛 ∈ (𝐹 “ (ℤ≥‘𝑚))) → ∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) = 𝑛)
268	266, 267	sylan2 593	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝐹 ∧ 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚)))) → ∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) = 𝑛)
269		inss1 4188	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) ⊆ (𝑦(ball‘𝐷)(𝑟 / 2))
270	269	sseli 3940	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) → 𝑛 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
271	270	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun 𝐹 ∧ 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚)))) → 𝑛 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
272		eleq1a 2833	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) → ((𝐹‘𝑘) = 𝑛 → (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
273	271, 272	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝐹 ∧ 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚)))) → ((𝐹‘𝑘) = 𝑛 → (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
274	273	reximdv 3167	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝐹 ∧ 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚)))) → (∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) = 𝑛 → ∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
275	268, 274	mpd 15	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝐹 ∧ 𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚)))) → ∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))
276	275	ex 413	. . . . . . . . . . . . 13 ⊢ (Fun 𝐹 → (𝑛 ∈ ((𝑦(ball‘𝐷)(𝑟 / 2)) ∩ (𝐹 “ (ℤ≥‘𝑚))) → ∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
277	276	exlimdv 1936	. . . . . . . . . . . 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 3117	. . . . . . . . . . 11 ⊢ ((∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ ∃𝑘 ∈ (ℤ≥‘𝑚)(𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ (ℤ≥‘𝑚)(∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))))
281		uznnssnn 12820	. . . . . . . . . . . . . 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 12958	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (𝑟 / 2) ∈ ℝ*)
288		simpllr 774	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝑦 ∈ 𝑋)
289	9	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝐹:ℕ⟶𝑋)
290		eluznn 12843	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑚 ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘𝑚)) → 𝑘 ∈ ℕ)
291	290	ad2ant2lr 746	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ) ∧ (𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) → 𝑘 ∈ ℕ)
292	291	ad2ant2lr 746	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝑘 ∈ ℕ)
293	289, 292	ffvelcdmd 7036	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (𝐹‘𝑘) ∈ 𝑋)
294		elbl3 23745	. . . . . . . . . . . . . . . . . . . . . . . 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 12843	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 ∈ (ℤ≥‘𝑘)) → 𝑛 ∈ ℕ)
300	292, 298, 299	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝑛 ∈ ℕ)
301	289, 300	ffvelcdmd 7036	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (𝐹‘𝑛) ∈ 𝑋)
302		metcl 23685	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑛) ∈ 𝑋) → ((𝐹‘𝑘)𝐷(𝐹‘𝑛)) ∈ ℝ)
303	297, 293, 301, 302	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((𝐹‘𝑘)𝐷(𝐹‘𝑛)) ∈ ℝ)
304		metcl 23685	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝐹‘𝑘)𝐷𝑦) ∈ ℝ)
305	297, 293, 288, 304	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((𝐹‘𝑘)𝐷𝑦) ∈ ℝ)
306	286	rpred 12957	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (𝑟 / 2) ∈ ℝ)
307		lt2add 11640	. . . . . . . . . . . . . . . . . . . . . . 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 12959	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝑟 ∈ ℂ)
311	310	2halvesd 12399	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((𝑟 / 2) + (𝑟 / 2)) = 𝑟)
312	311	breq2d 5117	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < ((𝑟 / 2) + (𝑟 / 2)) ↔ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < 𝑟))
313	309, 312	sylibd 238	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < 𝑟))
314		mettri2 23694	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ ((𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑛) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹‘𝑛)𝐷𝑦) ≤ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)))
315	297, 293, 301, 288, 314	syl13anc 1372	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((𝐹‘𝑛)𝐷𝑦) ≤ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)))
316		metcl 23685	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘𝑛) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝐹‘𝑛)𝐷𝑦) ∈ ℝ)
317	297, 301, 288, 316	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((𝐹‘𝑛)𝐷𝑦) ∈ ℝ)
318	303, 305	readdcld 11184	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) ∈ ℝ)
319	285	rpred 12957	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → 𝑟 ∈ ℝ)
320		lelttr 11245	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑛)𝐷𝑦) ∈ ℝ ∧ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) ∈ ℝ ∧ 𝑟 ∈ ℝ) → ((((𝐹‘𝑛)𝐷𝑦) ≤ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) ∧ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < 𝑟) → ((𝐹‘𝑛)𝐷𝑦) < 𝑟))
321	317, 318, 319, 320	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((((𝐹‘𝑛)𝐷𝑦) ≤ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) ∧ (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < 𝑟) → ((𝐹‘𝑛)𝐷𝑦) < 𝑟))
322	315, 321	mpand 693	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → ((((𝐹‘𝑘)𝐷(𝐹‘𝑛)) + ((𝐹‘𝑘)𝐷𝑦)) < 𝑟 → ((𝐹‘𝑛)𝐷𝑦) < 𝑟))
323	313, 322	syld 47	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ ((𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) ∧ 𝑛 ∈ (ℤ≥‘𝑘))) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ((𝐹‘𝑛)𝐷𝑦) < 𝑟))
324	323	anassrs 468	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ (𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) ∧ 𝑛 ∈ (ℤ≥‘𝑘)) → (((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ((𝐹‘𝑛)𝐷𝑦) < 𝑟))
325	324	ralimdva 3164	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ (𝑘 ∈ (ℤ≥‘𝑚) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)))) → (∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))
326	325	expr 457	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ 𝑘 ∈ (ℤ≥‘𝑚)) → ((𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) → (∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)))
327	326	com23 86	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ 𝑘 ∈ (ℤ≥‘𝑚)) → (∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ((𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2)) → ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)))
328	327	impd 411	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) ∧ 𝑘 ∈ (ℤ≥‘𝑚)) → ((∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))
329	328	reximdva 3165	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (∃𝑘 ∈ (ℤ≥‘𝑚)(∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑦(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))
330		ssrexv 4011	. . . . . . . . . . . . 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 692	. . . . . . . . 9 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ (𝑟 ∈ ℝ+ ∧ 𝑚 ∈ ℕ)) → (∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))
335	334	anassrs 468	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ 𝑟 ∈ ℝ+) ∧ 𝑚 ∈ ℕ) → (∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))
336	335	rexlimdva 3152	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ 𝑟 ∈ ℝ+) → (∃𝑚 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑚)∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑛)) < (𝑟 / 2) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟))
337	237, 336	mpd 15	. . . . . 6 ⊢ (((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) ∧ 𝑟 ∈ ℝ+) → ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)
338	337	ralrimiva 3143	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) → ∀𝑟 ∈ ℝ+ ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)
339		eqidd 2737	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) = (𝐹‘𝑛))
340	5, 4, 129, 222, 339, 9	lmmbrf 24626	. . . . . 6 ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑦 ↔ (𝑦 ∈ 𝑋 ∧ ∀𝑟 ∈ ℝ+ ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)))
341	340	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) → (𝐹(⇝𝑡‘𝐽)𝑦 ↔ (𝑦 ∈ 𝑋 ∧ ∀𝑟 ∈ ℝ+ ∃𝑘 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘𝑘)((𝐹‘𝑛)𝐷𝑦) < 𝑟)))
342	220, 338, 341	mpbir2and 711	. . . 4 ⊢ ((𝜑 ∧ ∀𝑢 ∈ ran ℤ≥𝑦 ∈ ((cls‘𝐽)‘(𝐹 “ 𝑢))) → 𝐹(⇝𝑡‘𝐽)𝑦)
343	200, 342	sylan2br 595	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))}) → 𝐹(⇝𝑡‘𝐽)𝑦)
344		releldm 5899	. . 3 ⊢ ((Rel (⇝𝑡‘𝐽) ∧ 𝐹(⇝𝑡‘𝐽)𝑦) → 𝐹 ∈ dom (⇝𝑡‘𝐽))
345	189, 343, 344	sylancr 587	. 2 ⊢ ((𝜑 ∧ 𝑦 ∈ ∩ {𝑘 ∣ ∃𝑢 ∈ ran ℤ≥𝑘 = ((cls‘𝐽)‘(𝐹 “ 𝑢))}) → 𝐹 ∈ dom (⇝𝑡‘𝐽))
346	188, 345	exlimddv 1938	1 ⊢ (𝜑 → 𝐹 ∈ dom (⇝𝑡‘𝐽))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087  ∀wal 1539   = wceq 1541  ∃wex 1781   ∈ wcel 2106  {cab 2713   ≠ wne 2943  ∀wral 3064  ∃wrex 3073  Vcvv 3445   ∪ cun 3908   ∩ cin 3909   ⊆ wss 3910  ∅c0 4282  𝒫 cpw 4560  {csn 4586  ∪ cuni 4865  ∩ cint 4907   class class class wbr 5105  dom cdm 5633  ran crn 5634   “ cima 5636  Rel wrel 5638  Fun wfun 6490   Fn wfn 6491  ⟶wf 6492  ‘cfv 6496  (class class class)co 7357   ↑_pm cpm 8766  Fincfn 8883  ficfi 9346  ℂcc 11049  ℝcr 11050  0cc0 11051  1c1 11052   + caddc 11054  ℝ^*cxr 11188   < clt 11189   ≤ cle 11190   / cdiv 11812  ℕcn 12153  2c2 12208  ℤcz 12499  ℤ_≥cuz 12763  ℝ⁺crp 12915  ∞Metcxmet 20781  Metcmet 20782  ballcbl 20783  MetOpencmopn 20786  Topctop 22242  Clsdccld 22367  clsccl 22369  ⇝_𝑡clm 22577  Compccmp 22737  Cauccau 24617

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-map 8767  df-pm 8768  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fi 9347  df-sup 9378  df-inf 9379  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-n0 12414  df-z 12500  df-uz 12764  df-q 12874  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-topgen 17325  df-psmet 20788  df-xmet 20789  df-met 20790  df-bl 20791  df-mopn 20792  df-top 22243  df-topon 22260  df-bases 22296  df-cld 22370  df-ntr 22371  df-cls 22372  df-lm 22580  df-cmp 22738  df-cau 24620

This theorem is referenced by:  heibor1  36269