Theorem iscmet3 24362

Description: The property "𝐷 is a complete metric" expressed in terms of functions on ℕ (or any other upper integer set). Thus, we only have to look at functions on ℕ, and not all possible Cauchy filters, to determine completeness. (The proof uses countable choice.) (Contributed by NM, 18-Dec-2006.) (Revised by Mario Carneiro, 5-May-2014.)

Hypotheses

Ref	Expression
iscmet3.1	⊢ 𝑍 = (ℤ≥‘𝑀)
iscmet3.2	⊢ 𝐽 = (MetOpen‘𝐷)
iscmet3.3	⊢ (𝜑 → 𝑀 ∈ ℤ)
iscmet3.4	⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))

Assertion

Ref	Expression
iscmet3	⊢ (𝜑 → (𝐷 ∈ (CMet‘𝑋) ↔ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))))

Distinct variable groups:   𝐷,𝑓   𝑓,𝑋   𝑓,𝐽   𝑓,𝑍   𝑓,𝑀   𝜑,𝑓

Proof of Theorem iscmet3

Dummy variables 𝑔 𝑖 𝑗 𝑘 𝑛 𝑠 𝑡 𝑢 𝑣 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		iscmet3.2	. . . . 5 ⊢ 𝐽 = (MetOpen‘𝐷)
2	1	cmetcau 24358	. . . 4 ⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑓 ∈ (Cau‘𝐷)) → 𝑓 ∈ dom (⇝𝑡‘𝐽))
3	2	a1d 25	. . 3 ⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑓 ∈ (Cau‘𝐷)) → (𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽)))
4	3	ralrimiva 3107	. 2 ⊢ (𝐷 ∈ (CMet‘𝑋) → ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽)))
5		iscmet3.4	. . . . 5 ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))
6	5	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) → 𝐷 ∈ (Met‘𝑋))
7		simpr 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ 𝑔 ∈ (CauFil‘𝐷)) → 𝑔 ∈ (CauFil‘𝐷))
8		1rp 12663	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ+
9		rphalfcl 12686	. . . . . . . . . . 11 ⊢ (1 ∈ ℝ+ → (1 / 2) ∈ ℝ+)
10	8, 9	ax-mp 5	. . . . . . . . . 10 ⊢ (1 / 2) ∈ ℝ+
11		rpexpcl 13729	. . . . . . . . . 10 ⊢ (((1 / 2) ∈ ℝ+ ∧ 𝑘 ∈ ℤ) → ((1 / 2)↑𝑘) ∈ ℝ+)
12	10, 11	mpan 686	. . . . . . . . 9 ⊢ (𝑘 ∈ ℤ → ((1 / 2)↑𝑘) ∈ ℝ+)
13		cfili 24337	. . . . . . . . 9 ⊢ ((𝑔 ∈ (CauFil‘𝐷) ∧ ((1 / 2)↑𝑘) ∈ ℝ+) → ∃𝑡 ∈ 𝑔 ∀𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 (𝑢𝐷𝑣) < ((1 / 2)↑𝑘))
14	7, 12, 13	syl2an 595	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ 𝑔 ∈ (CauFil‘𝐷)) ∧ 𝑘 ∈ ℤ) → ∃𝑡 ∈ 𝑔 ∀𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 (𝑢𝐷𝑣) < ((1 / 2)↑𝑘))
15	14	ralrimiva 3107	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ 𝑔 ∈ (CauFil‘𝐷)) → ∀𝑘 ∈ ℤ ∃𝑡 ∈ 𝑔 ∀𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 (𝑢𝐷𝑣) < ((1 / 2)↑𝑘))
16		vex 3426	. . . . . . . 8 ⊢ 𝑔 ∈ V
17		znnen 15849	. . . . . . . . 9 ⊢ ℤ ≈ ℕ
18		nnenom 13628	. . . . . . . . 9 ⊢ ℕ ≈ ω
19	17, 18	entri 8749	. . . . . . . 8 ⊢ ℤ ≈ ω
20		raleq 3333	. . . . . . . . 9 ⊢ (𝑡 = (𝑠‘𝑘) → (∀𝑣 ∈ 𝑡 (𝑢𝐷𝑣) < ((1 / 2)↑𝑘) ↔ ∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))
21	20	raleqbi1dv 3331	. . . . . . . 8 ⊢ (𝑡 = (𝑠‘𝑘) → (∀𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 (𝑢𝐷𝑣) < ((1 / 2)↑𝑘) ↔ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))
22	16, 19, 21	axcc4 10126	. . . . . . 7 ⊢ (∀𝑘 ∈ ℤ ∃𝑡 ∈ 𝑔 ∀𝑢 ∈ 𝑡 ∀𝑣 ∈ 𝑡 (𝑢𝐷𝑣) < ((1 / 2)↑𝑘) → ∃𝑠(𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))
23	15, 22	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ 𝑔 ∈ (CauFil‘𝐷)) → ∃𝑠(𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))
24		iscmet3.3	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℤ)
25	24	ad2antrr 722	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) → 𝑀 ∈ ℤ)
26		iscmet3.1	. . . . . . . . . . . 12 ⊢ 𝑍 = (ℤ≥‘𝑀)
27	26	uzenom 13612	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℤ → 𝑍 ≈ ω)
28		endom 8722	. . . . . . . . . . 11 ⊢ (𝑍 ≈ ω → 𝑍 ≼ ω)
29	25, 27, 28	3syl 18	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) → 𝑍 ≼ ω)
30		dfin5 3891	. . . . . . . . . . . . . . 15 ⊢ (( I ‘𝑋) ∩ ∩ 𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛)) = {𝑥 ∈ ( I ‘𝑋) ∣ 𝑥 ∈ ∩ 𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛)}
31		fzn0 13199	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀...𝑘) ≠ ∅ ↔ 𝑘 ∈ (ℤ≥‘𝑀))
32	31	biimpri 227	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (ℤ≥‘𝑀) → (𝑀...𝑘) ≠ ∅)
33	32, 26	eleq2s 2857	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ 𝑍 → (𝑀...𝑘) ≠ ∅)
34		metxmet 23395	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
35	5, 34	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))
36	35	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) → 𝐷 ∈ (∞Met‘𝑋))
37		simpl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔) → 𝑔 ∈ (CauFil‘𝐷))
38		cfilfil 24336	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑔 ∈ (CauFil‘𝐷)) → 𝑔 ∈ (Fil‘𝑋))
39	36, 37, 38	syl2an 595	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) → 𝑔 ∈ (Fil‘𝑋))
40		simprr 769	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) → 𝑠:ℤ⟶𝑔)
41		elfzelz 13185	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ (𝑀...𝑘) → 𝑛 ∈ ℤ)
42		ffvelrn 6941	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑠:ℤ⟶𝑔 ∧ 𝑛 ∈ ℤ) → (𝑠‘𝑛) ∈ 𝑔)
43	40, 41, 42	syl2an 595	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑛 ∈ (𝑀...𝑘)) → (𝑠‘𝑛) ∈ 𝑔)
44		filelss 22911	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑔 ∈ (Fil‘𝑋) ∧ (𝑠‘𝑛) ∈ 𝑔) → (𝑠‘𝑛) ⊆ 𝑋)
45	39, 43, 44	syl2an2r 681	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑛 ∈ (𝑀...𝑘)) → (𝑠‘𝑛) ⊆ 𝑋)
46	45	ralrimiva 3107	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) → ∀𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛) ⊆ 𝑋)
47		r19.2z 4422	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀...𝑘) ≠ ∅ ∧ ∀𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛) ⊆ 𝑋) → ∃𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛) ⊆ 𝑋)
48	33, 46, 47	syl2anr 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘 ∈ 𝑍) → ∃𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛) ⊆ 𝑋)
49		iinss 4982	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛) ⊆ 𝑋 → ∩ 𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛) ⊆ 𝑋)
50	48, 49	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘 ∈ 𝑍) → ∩ 𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛) ⊆ 𝑋)
51	6	ad2antrr 722	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘 ∈ 𝑍) → 𝐷 ∈ (Met‘𝑋))
52		elfvdm 6788	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐷 ∈ (Met‘𝑋) → 𝑋 ∈ dom Met)
53		fvi 6826	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋 ∈ dom Met → ( I ‘𝑋) = 𝑋)
54	51, 52, 53	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘 ∈ 𝑍) → ( I ‘𝑋) = 𝑋)
55	50, 54	sseqtrrd 3958	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘 ∈ 𝑍) → ∩ 𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛) ⊆ ( I ‘𝑋))
56		sseqin2 4146	. . . . . . . . . . . . . . . 16 ⊢ (∩ 𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛) ⊆ ( I ‘𝑋) ↔ (( I ‘𝑋) ∩ ∩ 𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛)) = ∩ 𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛))
57	55, 56	sylib 217	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘 ∈ 𝑍) → (( I ‘𝑋) ∩ ∩ 𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛)) = ∩ 𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛))
58	30, 57	eqtr3id 2793	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘 ∈ 𝑍) → {𝑥 ∈ ( I ‘𝑋) ∣ 𝑥 ∈ ∩ 𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛)} = ∩ 𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛))
59	39	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘 ∈ 𝑍) → 𝑔 ∈ (Fil‘𝑋))
60	43	ralrimiva 3107	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) → ∀𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛) ∈ 𝑔)
61	60	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘 ∈ 𝑍) → ∀𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛) ∈ 𝑔)
62	33	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘 ∈ 𝑍) → (𝑀...𝑘) ≠ ∅)
63		fzfid 13621	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘 ∈ 𝑍) → (𝑀...𝑘) ∈ Fin)
64		iinfi 9106	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 ∈ (Fil‘𝑋) ∧ (∀𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛) ∈ 𝑔 ∧ (𝑀...𝑘) ≠ ∅ ∧ (𝑀...𝑘) ∈ Fin)) → ∩ 𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛) ∈ (fi‘𝑔))
65	59, 61, 62, 63, 64	syl13anc 1370	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘 ∈ 𝑍) → ∩ 𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛) ∈ (fi‘𝑔))
66		filfi 22918	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ∈ (Fil‘𝑋) → (fi‘𝑔) = 𝑔)
67	59, 66	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘 ∈ 𝑍) → (fi‘𝑔) = 𝑔)
68	65, 67	eleqtrd 2841	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘 ∈ 𝑍) → ∩ 𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛) ∈ 𝑔)
69		fileln0 22909	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 ∈ (Fil‘𝑋) ∧ ∩ 𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛) ∈ 𝑔) → ∩ 𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛) ≠ ∅)
70	39, 68, 69	syl2an2r 681	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘 ∈ 𝑍) → ∩ 𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛) ≠ ∅)
71	58, 70	eqnetrd 3010	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘 ∈ 𝑍) → {𝑥 ∈ ( I ‘𝑋) ∣ 𝑥 ∈ ∩ 𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛)} ≠ ∅)
72		rabn0 4316	. . . . . . . . . . . . 13 ⊢ ({𝑥 ∈ ( I ‘𝑋) ∣ 𝑥 ∈ ∩ 𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛)} ≠ ∅ ↔ ∃𝑥 ∈ ( I ‘𝑋)𝑥 ∈ ∩ 𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛))
73	71, 72	sylib 217	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘 ∈ 𝑍) → ∃𝑥 ∈ ( I ‘𝑋)𝑥 ∈ ∩ 𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛))
74	73	ralrimiva 3107	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) → ∀𝑘 ∈ 𝑍 ∃𝑥 ∈ ( I ‘𝑋)𝑥 ∈ ∩ 𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛))
75	74	adantrrr 721	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) → ∀𝑘 ∈ 𝑍 ∃𝑥 ∈ ( I ‘𝑋)𝑥 ∈ ∩ 𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛))
76		fvex 6769	. . . . . . . . . . 11 ⊢ ( I ‘𝑋) ∈ V
77		eleq1 2826	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑓‘𝑘) → (𝑥 ∈ ∩ 𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛) ↔ (𝑓‘𝑘) ∈ ∩ 𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛)))
78		fvex 6769	. . . . . . . . . . . . 13 ⊢ (𝑓‘𝑘) ∈ V
79		eliin 4926	. . . . . . . . . . . . 13 ⊢ ((𝑓‘𝑘) ∈ V → ((𝑓‘𝑘) ∈ ∩ 𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛) ↔ ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛)))
80	78, 79	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((𝑓‘𝑘) ∈ ∩ 𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛) ↔ ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛))
81	77, 80	bitrdi 286	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑓‘𝑘) → (𝑥 ∈ ∩ 𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛) ↔ ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛)))
82	76, 81	axcc4dom 10128	. . . . . . . . . 10 ⊢ ((𝑍 ≼ ω ∧ ∀𝑘 ∈ 𝑍 ∃𝑥 ∈ ( I ‘𝑋)𝑥 ∈ ∩ 𝑛 ∈ (𝑀...𝑘)(𝑠‘𝑛)) → ∃𝑓(𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛)))
83	29, 75, 82	syl2anc 583	. . . . . . . . 9 ⊢ (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) → ∃𝑓(𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛)))
84		df-ral 3068	. . . . . . . . . . . . 13 ⊢ (∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽)) ↔ ∀𝑓(𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))))
85		19.29 1877	. . . . . . . . . . . . 13 ⊢ ((∀𝑓(𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ ∃𝑓(𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛))) → ∃𝑓((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛))))
86	84, 85	sylanb 580	. . . . . . . . . . . 12 ⊢ ((∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽)) ∧ ∃𝑓(𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛))) → ∃𝑓((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛))))
87	24	ad2antrr 722	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛)))) → 𝑀 ∈ ℤ)
88	5	ad2antrr 722	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛)))) → 𝐷 ∈ (Met‘𝑋))
89		simprrl 777	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛)))) → 𝑓:𝑍⟶( I ‘𝑋))
90		feq3 6567	. . . . . . . . . . . . . . . . 17 ⊢ (( I ‘𝑋) = 𝑋 → (𝑓:𝑍⟶( I ‘𝑋) ↔ 𝑓:𝑍⟶𝑋))
91	88, 52, 53, 90	4syl 19	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛)))) → (𝑓:𝑍⟶( I ‘𝑋) ↔ 𝑓:𝑍⟶𝑋))
92	89, 91	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛)))) → 𝑓:𝑍⟶𝑋)
93		simplrr 774	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛)))) → (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))
94	93	simprd 495	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛)))) → ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘))
95		fveq2 6756	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑖 → (𝑠‘𝑘) = (𝑠‘𝑖))
96		oveq2 7263	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑖 → ((1 / 2)↑𝑘) = ((1 / 2)↑𝑖))
97	96	breq2d 5082	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑖 → ((𝑢𝐷𝑣) < ((1 / 2)↑𝑘) ↔ (𝑢𝐷𝑣) < ((1 / 2)↑𝑖)))
98	95, 97	raleqbidv 3327	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑖 → (∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘) ↔ ∀𝑣 ∈ (𝑠‘𝑖)(𝑢𝐷𝑣) < ((1 / 2)↑𝑖)))
99	95, 98	raleqbidv 3327	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑖 → (∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘) ↔ ∀𝑢 ∈ (𝑠‘𝑖)∀𝑣 ∈ (𝑠‘𝑖)(𝑢𝐷𝑣) < ((1 / 2)↑𝑖)))
100	99	cbvralvw 3372	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘) ↔ ∀𝑖 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑖)∀𝑣 ∈ (𝑠‘𝑖)(𝑢𝐷𝑣) < ((1 / 2)↑𝑖))
101	94, 100	sylib 217	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛)))) → ∀𝑖 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑖)∀𝑣 ∈ (𝑠‘𝑖)(𝑢𝐷𝑣) < ((1 / 2)↑𝑖))
102		simprrr 778	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛)))) → ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛))
103		fveq2 6756	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑗 → (𝑠‘𝑛) = (𝑠‘𝑗))
104	103	eleq2d 2824	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑗 → ((𝑓‘𝑘) ∈ (𝑠‘𝑛) ↔ (𝑓‘𝑘) ∈ (𝑠‘𝑗)))
105	104	cbvralvw 3372	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛) ↔ ∀𝑗 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑗))
106		oveq2 7263	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑖 → (𝑀...𝑘) = (𝑀...𝑖))
107		fveq2 6756	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑖 → (𝑓‘𝑘) = (𝑓‘𝑖))
108	107	eleq1d 2823	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑖 → ((𝑓‘𝑘) ∈ (𝑠‘𝑗) ↔ (𝑓‘𝑖) ∈ (𝑠‘𝑗)))
109	106, 108	raleqbidv 3327	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑖 → (∀𝑗 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑗) ↔ ∀𝑗 ∈ (𝑀...𝑖)(𝑓‘𝑖) ∈ (𝑠‘𝑗)))
110	105, 109	syl5bb 282	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑖 → (∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛) ↔ ∀𝑗 ∈ (𝑀...𝑖)(𝑓‘𝑖) ∈ (𝑠‘𝑗)))
111	110	cbvralvw 3372	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛) ↔ ∀𝑖 ∈ 𝑍 ∀𝑗 ∈ (𝑀...𝑖)(𝑓‘𝑖) ∈ (𝑠‘𝑗))
112	102, 111	sylib 217	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛)))) → ∀𝑖 ∈ 𝑍 ∀𝑗 ∈ (𝑀...𝑖)(𝑓‘𝑖) ∈ (𝑠‘𝑗))
113	88, 34	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛)))) → 𝐷 ∈ (∞Met‘𝑋))
114		simplrl 773	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛)))) → 𝑔 ∈ (CauFil‘𝐷))
115	113, 114, 38	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛)))) → 𝑔 ∈ (Fil‘𝑋))
116	93	simpld 494	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛)))) → 𝑠:ℤ⟶𝑔)
117	26, 1, 87, 88, 92, 101, 112	iscmet3lem1 24360	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛)))) → 𝑓 ∈ (Cau‘𝐷))
118		simprl 767	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛)))) → (𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))))
119	117, 92, 118	mp2d 49	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛)))) → 𝑓 ∈ dom (⇝𝑡‘𝐽))
120	26, 1, 87, 88, 92, 101, 112, 115, 116, 119	iscmet3lem2 24361	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛)))) → (𝐽 fLim 𝑔) ≠ ∅)
121	120	ex 412	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) → (((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛))) → (𝐽 fLim 𝑔) ≠ ∅))
122	121	exlimdv 1937	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) → (∃𝑓((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛))) → (𝐽 fLim 𝑔) ≠ ∅))
123	86, 122	syl5 34	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) → ((∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽)) ∧ ∃𝑓(𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛))) → (𝐽 fLim 𝑔) ≠ ∅))
124	123	expdimp 452	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) → (∃𝑓(𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛)) → (𝐽 fLim 𝑔) ≠ ∅))
125	124	an32s 648	. . . . . . . . 9 ⊢ (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) → (∃𝑓(𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝑓‘𝑘) ∈ (𝑠‘𝑛)) → (𝐽 fLim 𝑔) ≠ ∅))
126	83, 125	mpd 15	. . . . . . . 8 ⊢ (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) → (𝐽 fLim 𝑔) ≠ ∅)
127	126	expr 456	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ 𝑔 ∈ (CauFil‘𝐷)) → ((𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)) → (𝐽 fLim 𝑔) ≠ ∅))
128	127	exlimdv 1937	. . . . . 6 ⊢ (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ 𝑔 ∈ (CauFil‘𝐷)) → (∃𝑠(𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠‘𝑘)∀𝑣 ∈ (𝑠‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)) → (𝐽 fLim 𝑔) ≠ ∅))
129	23, 128	mpd 15	. . . . 5 ⊢ (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) ∧ 𝑔 ∈ (CauFil‘𝐷)) → (𝐽 fLim 𝑔) ≠ ∅)
130	129	ralrimiva 3107	. . . 4 ⊢ ((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) → ∀𝑔 ∈ (CauFil‘𝐷)(𝐽 fLim 𝑔) ≠ ∅)
131	1	iscmet 24353	. . . 4 ⊢ (𝐷 ∈ (CMet‘𝑋) ↔ (𝐷 ∈ (Met‘𝑋) ∧ ∀𝑔 ∈ (CauFil‘𝐷)(𝐽 fLim 𝑔) ≠ ∅))
132	6, 130, 131	sylanbrc 582	. . 3 ⊢ ((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))) → 𝐷 ∈ (CMet‘𝑋))
133	132	ex 412	. 2 ⊢ (𝜑 → (∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽)) → 𝐷 ∈ (CMet‘𝑋)))
134	4, 133	impbid2 225	1 ⊢ (𝜑 → (𝐷 ∈ (CMet‘𝑋) ↔ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395  ∀wal 1537   = wceq 1539  ∃wex 1783   ∈ wcel 2108   ≠ wne 2942  ∀wral 3063  ∃wrex 3064  {crab 3067  Vcvv 3422   ∩ cin 3882   ⊆ wss 3883  ∅c0 4253  ∩ ciin 4922   class class class wbr 5070   I cid 5479  dom cdm 5580  ⟶wf 6414  ‘cfv 6418  (class class class)co 7255  ωcom 7687   ≈ cen 8688   ≼ cdom 8689  Fincfn 8691  ficfi 9099  1c1 10803   < clt 10940   / cdiv 11562  ℕcn 11903  2c2 11958  ℤcz 12249  ℤ_≥cuz 12511  ℝ⁺crp 12659  ...cfz 13168  ↑cexp 13710  ∞Metcxmet 20495  Metcmet 20496  MetOpencmopn 20500  ⇝_𝑡clm 22285  Filcfil 22904   fLim cflim 22993  CauFilccfil 24321  Cauccau 24322  CMetccmet 24323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-inf2 9329  ax-cc 10122  ax-cnex 10858  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879  ax-pre-sup 10880

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-int 4877  df-iun 4923  df-iin 4924  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-se 5536  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-isom 6427  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-1st 7804  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-1o 8267  df-oadd 8271  df-omul 8272  df-er 8456  df-map 8575  df-pm 8576  df-en 8692  df-dom 8693  df-sdom 8694  df-fin 8695  df-fi 9100  df-sup 9131  df-inf 9132  df-oi 9199  df-card 9628  df-acn 9631  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-div 11563  df-nn 11904  df-2 11966  df-3 11967  df-n0 12164  df-z 12250  df-uz 12512  df-q 12618  df-rp 12660  df-xneg 12777  df-xadd 12778  df-xmul 12779  df-ico 13014  df-fz 13169  df-fl 13440  df-seq 13650  df-exp 13711  df-cj 14738  df-re 14739  df-im 14740  df-sqrt 14874  df-abs 14875  df-clim 15125  df-rlim 15126  df-rest 17050  df-topgen 17071  df-psmet 20502  df-xmet 20503  df-met 20504  df-bl 20505  df-mopn 20506  df-fbas 20507  df-fg 20508  df-top 21951  df-topon 21968  df-bases 22004  df-ntr 22079  df-nei 22157  df-lm 22288  df-fil 22905  df-fm 22997  df-flim 22998  df-flf 22999  df-cfil 24324  df-cau 24325  df-cmet 24326

This theorem is referenced by:  iscmet2  24363  iscmet3i  24381  heibor1  35895  rrncms  35918