Theorem caubl 25180

Description: Sufficient condition to ensure a sequence of nested balls is Cauchy. (Contributed by Mario Carneiro, 18-Jan-2014.) (Revised by Mario Carneiro, 1-May-2014.)

Hypotheses

Ref	Expression
caubl.2	⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))
caubl.3	⊢ (𝜑 → 𝐹:ℕ⟶(𝑋 × ℝ+))
caubl.4	⊢ (𝜑 → ∀𝑛 ∈ ℕ ((ball‘𝐷)‘(𝐹‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)))
caubl.5	⊢ (𝜑 → ∀𝑟 ∈ ℝ+ ∃𝑛 ∈ ℕ (2nd ‘(𝐹‘𝑛)) < 𝑟)

Assertion

Ref	Expression
caubl	⊢ (𝜑 → (1st ∘ 𝐹) ∈ (Cau‘𝐷))

Distinct variable groups:   𝑛,𝑟,𝐷   𝑛,𝐹,𝑟   𝜑,𝑟   𝑛,𝑋,𝑟   𝜑,𝑛

Proof of Theorem caubl

Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		caubl.5	. . 3 ⊢ (𝜑 → ∀𝑟 ∈ ℝ+ ∃𝑛 ∈ ℕ (2nd ‘(𝐹‘𝑛)) < 𝑟)
2		2fveq3 6887	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝑛 → ((ball‘𝐷)‘(𝐹‘𝑟)) = ((ball‘𝐷)‘(𝐹‘𝑛)))
3	2	sseq1d 4006	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝑛 → (((ball‘𝐷)‘(𝐹‘𝑟)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) ↔ ((ball‘𝐷)‘(𝐹‘𝑛)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))))
4	3	imbi2d 340	. . . . . . . . . . 11 ⊢ (𝑟 = 𝑛 → (((𝜑 ∧ 𝑛 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘𝑟)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))) ↔ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘𝑛)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)))))
5		2fveq3 6887	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝑘 → ((ball‘𝐷)‘(𝐹‘𝑟)) = ((ball‘𝐷)‘(𝐹‘𝑘)))
6	5	sseq1d 4006	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝑘 → (((ball‘𝐷)‘(𝐹‘𝑟)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) ↔ ((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))))
7	6	imbi2d 340	. . . . . . . . . . 11 ⊢ (𝑟 = 𝑘 → (((𝜑 ∧ 𝑛 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘𝑟)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))) ↔ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)))))
8		2fveq3 6887	. . . . . . . . . . . . 13 ⊢ (𝑟 = (𝑘 + 1) → ((ball‘𝐷)‘(𝐹‘𝑟)) = ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))))
9	8	sseq1d 4006	. . . . . . . . . . . 12 ⊢ (𝑟 = (𝑘 + 1) → (((ball‘𝐷)‘(𝐹‘𝑟)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) ↔ ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))))
10	9	imbi2d 340	. . . . . . . . . . 11 ⊢ (𝑟 = (𝑘 + 1) → (((𝜑 ∧ 𝑛 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘𝑟)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))) ↔ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)))))
11		ssid 3997	. . . . . . . . . . . 12 ⊢ ((ball‘𝐷)‘(𝐹‘𝑛)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))
12	11	2a1i 12	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℤ → ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘𝑛)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))))
13		caubl.4	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑛 ∈ ℕ ((ball‘𝐷)‘(𝐹‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)))
14		eluznn 12901	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝑘 ∈ ℕ)
15		fvoveq1 7425	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → (𝐹‘(𝑛 + 1)) = (𝐹‘(𝑘 + 1)))
16	15	fveq2d 6886	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → ((ball‘𝐷)‘(𝐹‘(𝑛 + 1))) = ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))))
17		2fveq3 6887	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → ((ball‘𝐷)‘(𝐹‘𝑛)) = ((ball‘𝐷)‘(𝐹‘𝑘)))
18	16, 17	sseq12d 4008	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑘 → (((ball‘𝐷)‘(𝐹‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) ↔ ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑘))))
19	18	rspccva 3603	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑛 ∈ ℕ ((ball‘𝐷)‘(𝐹‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) ∧ 𝑘 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑘)))
20	13, 14, 19	syl2an 595	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘𝑛))) → ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑘)))
21	20	anassrs 467	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑘)))
22		sstr2 3982	. . . . . . . . . . . . . 14 ⊢ (((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑘)) → (((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) → ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))))
23	21, 22	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) → ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))))
24	23	expcom 413	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ≥‘𝑛) → ((𝜑 ∧ 𝑛 ∈ ℕ) → (((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) → ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)))))
25	24	a2d 29	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (ℤ≥‘𝑛) → (((𝜑 ∧ 𝑛 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))) → ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘(𝑘 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)))))
26	4, 7, 10, 7, 12, 25	uzind4 12889	. . . . . . . . . 10 ⊢ (𝑘 ∈ (ℤ≥‘𝑛) → ((𝜑 ∧ 𝑛 ∈ ℕ) → ((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))))
27	26	com12 32	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑘 ∈ (ℤ≥‘𝑛) → ((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))))
28	27	ad2ant2r 744	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) → (𝑘 ∈ (ℤ≥‘𝑛) → ((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛))))
29		relxp 5685	. . . . . . . . . . . . . . . 16 ⊢ Rel (𝑋 × ℝ+)
30		caubl.3	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹:ℕ⟶(𝑋 × ℝ+))
31	30	ad3antrrr 727	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝐹:ℕ⟶(𝑋 × ℝ+))
32		simplrl 774	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝑛 ∈ ℕ)
33	31, 32	ffvelcdmd 7078	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑛) ∈ (𝑋 × ℝ+))
34		1st2nd 8019	. . . . . . . . . . . . . . . 16 ⊢ ((Rel (𝑋 × ℝ+) ∧ (𝐹‘𝑛) ∈ (𝑋 × ℝ+)) → (𝐹‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
35	29, 33, 34	sylancr 586	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
36	35	fveq2d 6886	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((ball‘𝐷)‘(𝐹‘𝑛)) = ((ball‘𝐷)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩))
37		df-ov 7405	. . . . . . . . . . . . . 14 ⊢ ((1st ‘(𝐹‘𝑛))(ball‘𝐷)(2nd ‘(𝐹‘𝑛))) = ((ball‘𝐷)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
38	36, 37	eqtr4di 2782	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((ball‘𝐷)‘(𝐹‘𝑛)) = ((1st ‘(𝐹‘𝑛))(ball‘𝐷)(2nd ‘(𝐹‘𝑛))))
39		caubl.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))
40	39	ad3antrrr 727	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝐷 ∈ (∞Met‘𝑋))
41		xp1st 8001	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑛) ∈ (𝑋 × ℝ+) → (1st ‘(𝐹‘𝑛)) ∈ 𝑋)
42	33, 41	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (1st ‘(𝐹‘𝑛)) ∈ 𝑋)
43		xp2nd 8002	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑛) ∈ (𝑋 × ℝ+) → (2nd ‘(𝐹‘𝑛)) ∈ ℝ+)
44	33, 43	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (2nd ‘(𝐹‘𝑛)) ∈ ℝ+)
45	44	rpxrd 13018	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (2nd ‘(𝐹‘𝑛)) ∈ ℝ*)
46		simpllr 773	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝑟 ∈ ℝ+)
47	46	rpxrd 13018	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝑟 ∈ ℝ*)
48		simplrr 775	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (2nd ‘(𝐹‘𝑛)) < 𝑟)
49		rpre 12983	. . . . . . . . . . . . . . . . 17 ⊢ ((2nd ‘(𝐹‘𝑛)) ∈ ℝ+ → (2nd ‘(𝐹‘𝑛)) ∈ ℝ)
50		rpre 12983	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ)
51		ltle 11301	. . . . . . . . . . . . . . . . 17 ⊢ (((2nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ 𝑟 ∈ ℝ) → ((2nd ‘(𝐹‘𝑛)) < 𝑟 → (2nd ‘(𝐹‘𝑛)) ≤ 𝑟))
52	49, 50, 51	syl2an 595	. . . . . . . . . . . . . . . 16 ⊢ (((2nd ‘(𝐹‘𝑛)) ∈ ℝ+ ∧ 𝑟 ∈ ℝ+) → ((2nd ‘(𝐹‘𝑛)) < 𝑟 → (2nd ‘(𝐹‘𝑛)) ≤ 𝑟))
53	44, 46, 52	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((2nd ‘(𝐹‘𝑛)) < 𝑟 → (2nd ‘(𝐹‘𝑛)) ≤ 𝑟))
54	48, 53	mpd 15	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (2nd ‘(𝐹‘𝑛)) ≤ 𝑟)
55		ssbl 24273	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (1st ‘(𝐹‘𝑛)) ∈ 𝑋) ∧ ((2nd ‘(𝐹‘𝑛)) ∈ ℝ* ∧ 𝑟 ∈ ℝ*) ∧ (2nd ‘(𝐹‘𝑛)) ≤ 𝑟) → ((1st ‘(𝐹‘𝑛))(ball‘𝐷)(2nd ‘(𝐹‘𝑛))) ⊆ ((1st ‘(𝐹‘𝑛))(ball‘𝐷)𝑟))
56	40, 42, 45, 47, 54, 55	syl221anc 1378	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((1st ‘(𝐹‘𝑛))(ball‘𝐷)(2nd ‘(𝐹‘𝑛))) ⊆ ((1st ‘(𝐹‘𝑛))(ball‘𝐷)𝑟))
57	38, 56	eqsstrd 4013	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((ball‘𝐷)‘(𝐹‘𝑛)) ⊆ ((1st ‘(𝐹‘𝑛))(ball‘𝐷)𝑟))
58		sstr2 3982	. . . . . . . . . . . 12 ⊢ (((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) → (((ball‘𝐷)‘(𝐹‘𝑛)) ⊆ ((1st ‘(𝐹‘𝑛))(ball‘𝐷)𝑟) → ((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((1st ‘(𝐹‘𝑛))(ball‘𝐷)𝑟)))
59	57, 58	syl5com 31	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) → ((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((1st ‘(𝐹‘𝑛))(ball‘𝐷)𝑟)))
60		simprl 768	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) → 𝑛 ∈ ℕ)
61	60, 14	sylan 579	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝑘 ∈ ℕ)
62	31, 61	ffvelcdmd 7078	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑘) ∈ (𝑋 × ℝ+))
63		xp1st 8001	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑘) ∈ (𝑋 × ℝ+) → (1st ‘(𝐹‘𝑘)) ∈ 𝑋)
64	62, 63	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (1st ‘(𝐹‘𝑘)) ∈ 𝑋)
65		xp2nd 8002	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑘) ∈ (𝑋 × ℝ+) → (2nd ‘(𝐹‘𝑘)) ∈ ℝ+)
66	62, 65	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (2nd ‘(𝐹‘𝑘)) ∈ ℝ+)
67		blcntr 24263	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (1st ‘(𝐹‘𝑘)) ∈ 𝑋 ∧ (2nd ‘(𝐹‘𝑘)) ∈ ℝ+) → (1st ‘(𝐹‘𝑘)) ∈ ((1st ‘(𝐹‘𝑘))(ball‘𝐷)(2nd ‘(𝐹‘𝑘))))
68	40, 64, 66, 67	syl3anc 1368	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (1st ‘(𝐹‘𝑘)) ∈ ((1st ‘(𝐹‘𝑘))(ball‘𝐷)(2nd ‘(𝐹‘𝑘))))
69		1st2nd 8019	. . . . . . . . . . . . . . 15 ⊢ ((Rel (𝑋 × ℝ+) ∧ (𝐹‘𝑘) ∈ (𝑋 × ℝ+)) → (𝐹‘𝑘) = ⟨(1st ‘(𝐹‘𝑘)), (2nd ‘(𝐹‘𝑘))⟩)
70	29, 62, 69	sylancr 586	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑘) = ⟨(1st ‘(𝐹‘𝑘)), (2nd ‘(𝐹‘𝑘))⟩)
71	70	fveq2d 6886	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((ball‘𝐷)‘(𝐹‘𝑘)) = ((ball‘𝐷)‘⟨(1st ‘(𝐹‘𝑘)), (2nd ‘(𝐹‘𝑘))⟩))
72		df-ov 7405	. . . . . . . . . . . . 13 ⊢ ((1st ‘(𝐹‘𝑘))(ball‘𝐷)(2nd ‘(𝐹‘𝑘))) = ((ball‘𝐷)‘⟨(1st ‘(𝐹‘𝑘)), (2nd ‘(𝐹‘𝑘))⟩)
73	71, 72	eqtr4di 2782	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((ball‘𝐷)‘(𝐹‘𝑘)) = ((1st ‘(𝐹‘𝑘))(ball‘𝐷)(2nd ‘(𝐹‘𝑘))))
74	68, 73	eleqtrrd 2828	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (1st ‘(𝐹‘𝑘)) ∈ ((ball‘𝐷)‘(𝐹‘𝑘)))
75		ssel 3968	. . . . . . . . . . 11 ⊢ (((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((1st ‘(𝐹‘𝑛))(ball‘𝐷)𝑟) → ((1st ‘(𝐹‘𝑘)) ∈ ((ball‘𝐷)‘(𝐹‘𝑘)) → (1st ‘(𝐹‘𝑘)) ∈ ((1st ‘(𝐹‘𝑛))(ball‘𝐷)𝑟)))
76	59, 74, 75	syl6ci 71	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) → (1st ‘(𝐹‘𝑘)) ∈ ((1st ‘(𝐹‘𝑛))(ball‘𝐷)𝑟)))
77		elbl2 24240	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑟 ∈ ℝ*) ∧ ((1st ‘(𝐹‘𝑛)) ∈ 𝑋 ∧ (1st ‘(𝐹‘𝑘)) ∈ 𝑋)) → ((1st ‘(𝐹‘𝑘)) ∈ ((1st ‘(𝐹‘𝑛))(ball‘𝐷)𝑟) ↔ ((1st ‘(𝐹‘𝑛))𝐷(1st ‘(𝐹‘𝑘))) < 𝑟))
78	40, 47, 42, 64, 77	syl22anc 836	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((1st ‘(𝐹‘𝑘)) ∈ ((1st ‘(𝐹‘𝑛))(ball‘𝐷)𝑟) ↔ ((1st ‘(𝐹‘𝑛))𝐷(1st ‘(𝐹‘𝑘))) < 𝑟))
79	76, 78	sylibd 238	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) → ((1st ‘(𝐹‘𝑛))𝐷(1st ‘(𝐹‘𝑘))) < 𝑟))
80	79	ex 412	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) → (𝑘 ∈ (ℤ≥‘𝑛) → (((ball‘𝐷)‘(𝐹‘𝑘)) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)) → ((1st ‘(𝐹‘𝑛))𝐷(1st ‘(𝐹‘𝑘))) < 𝑟)))
81	28, 80	mpdd 43	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) → (𝑘 ∈ (ℤ≥‘𝑛) → ((1st ‘(𝐹‘𝑛))𝐷(1st ‘(𝐹‘𝑘))) < 𝑟))
82	81	ralrimiv 3137	. . . . . 6 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ ℕ ∧ (2nd ‘(𝐹‘𝑛)) < 𝑟)) → ∀𝑘 ∈ (ℤ≥‘𝑛)((1st ‘(𝐹‘𝑛))𝐷(1st ‘(𝐹‘𝑘))) < 𝑟)
83	82	expr 456	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑛 ∈ ℕ) → ((2nd ‘(𝐹‘𝑛)) < 𝑟 → ∀𝑘 ∈ (ℤ≥‘𝑛)((1st ‘(𝐹‘𝑛))𝐷(1st ‘(𝐹‘𝑘))) < 𝑟))
84	83	reximdva 3160	. . . 4 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (∃𝑛 ∈ ℕ (2nd ‘(𝐹‘𝑛)) < 𝑟 → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((1st ‘(𝐹‘𝑛))𝐷(1st ‘(𝐹‘𝑘))) < 𝑟))
85	84	ralimdva 3159	. . 3 ⊢ (𝜑 → (∀𝑟 ∈ ℝ+ ∃𝑛 ∈ ℕ (2nd ‘(𝐹‘𝑛)) < 𝑟 → ∀𝑟 ∈ ℝ+ ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((1st ‘(𝐹‘𝑛))𝐷(1st ‘(𝐹‘𝑘))) < 𝑟))
86	1, 85	mpd 15	. 2 ⊢ (𝜑 → ∀𝑟 ∈ ℝ+ ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((1st ‘(𝐹‘𝑛))𝐷(1st ‘(𝐹‘𝑘))) < 𝑟)
87		nnuz 12864	. . 3 ⊢ ℕ = (ℤ≥‘1)
88		1zzd 12592	. . 3 ⊢ (𝜑 → 1 ∈ ℤ)
89		fvco3 6981	. . . 4 ⊢ ((𝐹:ℕ⟶(𝑋 × ℝ+) ∧ 𝑘 ∈ ℕ) → ((1st ∘ 𝐹)‘𝑘) = (1st ‘(𝐹‘𝑘)))
90	30, 89	sylan 579	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((1st ∘ 𝐹)‘𝑘) = (1st ‘(𝐹‘𝑘)))
91		fvco3 6981	. . . 4 ⊢ ((𝐹:ℕ⟶(𝑋 × ℝ+) ∧ 𝑛 ∈ ℕ) → ((1st ∘ 𝐹)‘𝑛) = (1st ‘(𝐹‘𝑛)))
92	30, 91	sylan 579	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st ∘ 𝐹)‘𝑛) = (1st ‘(𝐹‘𝑛)))
93		1stcof 7999	. . . 4 ⊢ (𝐹:ℕ⟶(𝑋 × ℝ+) → (1st ∘ 𝐹):ℕ⟶𝑋)
94	30, 93	syl 17	. . 3 ⊢ (𝜑 → (1st ∘ 𝐹):ℕ⟶𝑋)
95	87, 39, 88, 90, 92, 94	iscauf 25152	. 2 ⊢ (𝜑 → ((1st ∘ 𝐹) ∈ (Cau‘𝐷) ↔ ∀𝑟 ∈ ℝ+ ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)((1st ‘(𝐹‘𝑛))𝐷(1st ‘(𝐹‘𝑘))) < 𝑟))
96	86, 95	mpbird 257	1 ⊢ (𝜑 → (1st ∘ 𝐹) ∈ (Cau‘𝐷))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1533   ∈ wcel 2098  ∀wral 3053  ∃wrex 3062   ⊆ wss 3941  ⟨cop 4627   class class class wbr 5139   × cxp 5665   ∘ ccom 5671  Rel wrel 5672  ⟶wf 6530  ‘cfv 6534  (class class class)co 7402  1^st c1st 7967  2^nd c2nd 7968  ℝcr 11106  1c1 11108   + caddc 11110  ℝ^*cxr 11246   < clt 11247   ≤ cle 11248  ℕcn 12211  ℤcz 12557  ℤ_≥cuz 12821  ℝ⁺crp 12975  ∞Metcxmet 21219  ballcbl 21221  Cauccau 25125

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5290  ax-nul 5297  ax-pow 5354  ax-pr 5418  ax-un 7719  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3960  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-iun 4990  df-br 5140  df-opab 5202  df-mpt 5223  df-tr 5257  df-id 5565  df-eprel 5571  df-po 5579  df-so 5580  df-fr 5622  df-we 5624  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-pred 6291  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-riota 7358  df-ov 7405  df-oprab 7406  df-mpo 7407  df-om 7850  df-1st 7969  df-2nd 7970  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-er 8700  df-map 8819  df-pm 8820  df-en 8937  df-dom 8938  df-sdom 8939  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253  df-sub 11445  df-neg 11446  df-div 11871  df-nn 12212  df-2 12274  df-n0 12472  df-z 12558  df-uz 12822  df-rp 12976  df-xneg 13093  df-xadd 13094  df-xmul 13095  df-psmet 21226  df-xmet 21227  df-bl 21229  df-cau 25128

This theorem is referenced by:  bcthlem4  25199  heiborlem9  37191