MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iscmet3 Structured version   Visualization version   GIF version

Theorem iscmet3 23010
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.
StepHypRef Expression
1 iscmet3.2 . . . . 5 𝐽 = (MetOpen‘𝐷)
21cmetcau 23006 . . . 4 ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑓 ∈ (Cau‘𝐷)) → 𝑓 ∈ dom (⇝𝑡𝐽))
32a1d 25 . . 3 ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑓 ∈ (Cau‘𝐷)) → (𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽)))
43ralrimiva 2961 . 2 (𝐷 ∈ (CMet‘𝑋) → ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽)))
5 iscmet3.4 . . . . 5 (𝜑𝐷 ∈ (Met‘𝑋))
65adantr 481 . . . 4 ((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) → 𝐷 ∈ (Met‘𝑋))
7 simpr 477 . . . . . . . . 9 (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ 𝑔 ∈ (CauFil‘𝐷)) → 𝑔 ∈ (CauFil‘𝐷))
8 1rp 11787 . . . . . . . . . . 11 1 ∈ ℝ+
9 rphalfcl 11809 . . . . . . . . . . 11 (1 ∈ ℝ+ → (1 / 2) ∈ ℝ+)
108, 9ax-mp 5 . . . . . . . . . 10 (1 / 2) ∈ ℝ+
11 rpexpcl 12826 . . . . . . . . . 10 (((1 / 2) ∈ ℝ+𝑘 ∈ ℤ) → ((1 / 2)↑𝑘) ∈ ℝ+)
1210, 11mpan 705 . . . . . . . . 9 (𝑘 ∈ ℤ → ((1 / 2)↑𝑘) ∈ ℝ+)
13 cfili 22985 . . . . . . . . 9 ((𝑔 ∈ (CauFil‘𝐷) ∧ ((1 / 2)↑𝑘) ∈ ℝ+) → ∃𝑡𝑔𝑢𝑡𝑣𝑡 (𝑢𝐷𝑣) < ((1 / 2)↑𝑘))
147, 12, 13syl2an 494 . . . . . . . 8 ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ 𝑔 ∈ (CauFil‘𝐷)) ∧ 𝑘 ∈ ℤ) → ∃𝑡𝑔𝑢𝑡𝑣𝑡 (𝑢𝐷𝑣) < ((1 / 2)↑𝑘))
1514ralrimiva 2961 . . . . . . 7 (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ 𝑔 ∈ (CauFil‘𝐷)) → ∀𝑘 ∈ ℤ ∃𝑡𝑔𝑢𝑡𝑣𝑡 (𝑢𝐷𝑣) < ((1 / 2)↑𝑘))
16 vex 3192 . . . . . . . 8 𝑔 ∈ V
17 znnen 14873 . . . . . . . . 9 ℤ ≈ ℕ
18 nnenom 12726 . . . . . . . . 9 ℕ ≈ ω
1917, 18entri 7961 . . . . . . . 8 ℤ ≈ ω
20 raleq 3130 . . . . . . . . 9 (𝑡 = (𝑠𝑘) → (∀𝑣𝑡 (𝑢𝐷𝑣) < ((1 / 2)↑𝑘) ↔ ∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))
2120raleqbi1dv 3138 . . . . . . . 8 (𝑡 = (𝑠𝑘) → (∀𝑢𝑡𝑣𝑡 (𝑢𝐷𝑣) < ((1 / 2)↑𝑘) ↔ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))
2216, 19, 21axcc4 9212 . . . . . . 7 (∀𝑘 ∈ ℤ ∃𝑡𝑔𝑢𝑡𝑣𝑡 (𝑢𝐷𝑣) < ((1 / 2)↑𝑘) → ∃𝑠(𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))
2315, 22syl 17 . . . . . 6 (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ 𝑔 ∈ (CauFil‘𝐷)) → ∃𝑠(𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))
24 iscmet3.3 . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℤ)
2524ad2antrr 761 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) → 𝑀 ∈ ℤ)
26 iscmet3.1 . . . . . . . . . . . 12 𝑍 = (ℤ𝑀)
2726uzenom 12710 . . . . . . . . . . 11 (𝑀 ∈ ℤ → 𝑍 ≈ ω)
28 endom 7933 . . . . . . . . . . 11 (𝑍 ≈ ω → 𝑍 ≼ ω)
2925, 27, 283syl 18 . . . . . . . . . 10 (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) → 𝑍 ≼ ω)
30 dfin5 3567 . . . . . . . . . . . . . . 15 (( I ‘𝑋) ∩ 𝑛 ∈ (𝑀...𝑘)(𝑠𝑛)) = {𝑥 ∈ ( I ‘𝑋) ∣ 𝑥 𝑛 ∈ (𝑀...𝑘)(𝑠𝑛)}
31 fzn0 12304 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀...𝑘) ≠ ∅ ↔ 𝑘 ∈ (ℤ𝑀))
3231biimpri 218 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ (ℤ𝑀) → (𝑀...𝑘) ≠ ∅)
3332, 26eleq2s 2716 . . . . . . . . . . . . . . . . . . 19 (𝑘𝑍 → (𝑀...𝑘) ≠ ∅)
34 simprr 795 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) → 𝑠:ℤ⟶𝑔)
35 elfzelz 12291 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (𝑀...𝑘) → 𝑛 ∈ ℤ)
36 ffvelrn 6318 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑠:ℤ⟶𝑔𝑛 ∈ ℤ) → (𝑠𝑛) ∈ 𝑔)
3734, 35, 36syl2an 494 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑛 ∈ (𝑀...𝑘)) → (𝑠𝑛) ∈ 𝑔)
38 metxmet 22058 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
395, 38syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐷 ∈ (∞Met‘𝑋))
4039adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) → 𝐷 ∈ (∞Met‘𝑋))
41 simpl 473 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔) → 𝑔 ∈ (CauFil‘𝐷))
42 cfilfil 22984 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑔 ∈ (CauFil‘𝐷)) → 𝑔 ∈ (Fil‘𝑋))
4340, 41, 42syl2an 494 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) → 𝑔 ∈ (Fil‘𝑋))
44 filelss 21575 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 ∈ (Fil‘𝑋) ∧ (𝑠𝑛) ∈ 𝑔) → (𝑠𝑛) ⊆ 𝑋)
4543, 44sylan 488 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ (𝑠𝑛) ∈ 𝑔) → (𝑠𝑛) ⊆ 𝑋)
4637, 45syldan 487 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑛 ∈ (𝑀...𝑘)) → (𝑠𝑛) ⊆ 𝑋)
4746ralrimiva 2961 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) → ∀𝑛 ∈ (𝑀...𝑘)(𝑠𝑛) ⊆ 𝑋)
48 r19.2z 4037 . . . . . . . . . . . . . . . . . . 19 (((𝑀...𝑘) ≠ ∅ ∧ ∀𝑛 ∈ (𝑀...𝑘)(𝑠𝑛) ⊆ 𝑋) → ∃𝑛 ∈ (𝑀...𝑘)(𝑠𝑛) ⊆ 𝑋)
4933, 47, 48syl2anr 495 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘𝑍) → ∃𝑛 ∈ (𝑀...𝑘)(𝑠𝑛) ⊆ 𝑋)
50 iinss 4542 . . . . . . . . . . . . . . . . . 18 (∃𝑛 ∈ (𝑀...𝑘)(𝑠𝑛) ⊆ 𝑋 𝑛 ∈ (𝑀...𝑘)(𝑠𝑛) ⊆ 𝑋)
5149, 50syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘𝑍) → 𝑛 ∈ (𝑀...𝑘)(𝑠𝑛) ⊆ 𝑋)
526ad2antrr 761 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘𝑍) → 𝐷 ∈ (Met‘𝑋))
53 elfvdm 6182 . . . . . . . . . . . . . . . . . 18 (𝐷 ∈ (Met‘𝑋) → 𝑋 ∈ dom Met)
54 fvi 6217 . . . . . . . . . . . . . . . . . 18 (𝑋 ∈ dom Met → ( I ‘𝑋) = 𝑋)
5552, 53, 543syl 18 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘𝑍) → ( I ‘𝑋) = 𝑋)
5651, 55sseqtr4d 3626 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘𝑍) → 𝑛 ∈ (𝑀...𝑘)(𝑠𝑛) ⊆ ( I ‘𝑋))
57 sseqin2 3800 . . . . . . . . . . . . . . . 16 ( 𝑛 ∈ (𝑀...𝑘)(𝑠𝑛) ⊆ ( I ‘𝑋) ↔ (( I ‘𝑋) ∩ 𝑛 ∈ (𝑀...𝑘)(𝑠𝑛)) = 𝑛 ∈ (𝑀...𝑘)(𝑠𝑛))
5856, 57sylib 208 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘𝑍) → (( I ‘𝑋) ∩ 𝑛 ∈ (𝑀...𝑘)(𝑠𝑛)) = 𝑛 ∈ (𝑀...𝑘)(𝑠𝑛))
5930, 58syl5eqr 2669 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘𝑍) → {𝑥 ∈ ( I ‘𝑋) ∣ 𝑥 𝑛 ∈ (𝑀...𝑘)(𝑠𝑛)} = 𝑛 ∈ (𝑀...𝑘)(𝑠𝑛))
6043adantr 481 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘𝑍) → 𝑔 ∈ (Fil‘𝑋))
6137ralrimiva 2961 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) → ∀𝑛 ∈ (𝑀...𝑘)(𝑠𝑛) ∈ 𝑔)
6261adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘𝑍) → ∀𝑛 ∈ (𝑀...𝑘)(𝑠𝑛) ∈ 𝑔)
6333adantl 482 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘𝑍) → (𝑀...𝑘) ≠ ∅)
64 fzfid 12719 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘𝑍) → (𝑀...𝑘) ∈ Fin)
65 iinfi 8274 . . . . . . . . . . . . . . . . 17 ((𝑔 ∈ (Fil‘𝑋) ∧ (∀𝑛 ∈ (𝑀...𝑘)(𝑠𝑛) ∈ 𝑔 ∧ (𝑀...𝑘) ≠ ∅ ∧ (𝑀...𝑘) ∈ Fin)) → 𝑛 ∈ (𝑀...𝑘)(𝑠𝑛) ∈ (fi‘𝑔))
6660, 62, 63, 64, 65syl13anc 1325 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘𝑍) → 𝑛 ∈ (𝑀...𝑘)(𝑠𝑛) ∈ (fi‘𝑔))
67 filfi 21582 . . . . . . . . . . . . . . . . 17 (𝑔 ∈ (Fil‘𝑋) → (fi‘𝑔) = 𝑔)
6860, 67syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘𝑍) → (fi‘𝑔) = 𝑔)
6966, 68eleqtrd 2700 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘𝑍) → 𝑛 ∈ (𝑀...𝑘)(𝑠𝑛) ∈ 𝑔)
70 fileln0 21573 . . . . . . . . . . . . . . 15 ((𝑔 ∈ (Fil‘𝑋) ∧ 𝑛 ∈ (𝑀...𝑘)(𝑠𝑛) ∈ 𝑔) → 𝑛 ∈ (𝑀...𝑘)(𝑠𝑛) ≠ ∅)
7160, 69, 70syl2anc 692 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘𝑍) → 𝑛 ∈ (𝑀...𝑘)(𝑠𝑛) ≠ ∅)
7259, 71eqnetrd 2857 . . . . . . . . . . . . 13 ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘𝑍) → {𝑥 ∈ ( I ‘𝑋) ∣ 𝑥 𝑛 ∈ (𝑀...𝑘)(𝑠𝑛)} ≠ ∅)
73 rabn0 3937 . . . . . . . . . . . . 13 ({𝑥 ∈ ( I ‘𝑋) ∣ 𝑥 𝑛 ∈ (𝑀...𝑘)(𝑠𝑛)} ≠ ∅ ↔ ∃𝑥 ∈ ( I ‘𝑋)𝑥 𝑛 ∈ (𝑀...𝑘)(𝑠𝑛))
7472, 73sylib 208 . . . . . . . . . . . 12 ((((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) ∧ 𝑘𝑍) → ∃𝑥 ∈ ( I ‘𝑋)𝑥 𝑛 ∈ (𝑀...𝑘)(𝑠𝑛))
7574ralrimiva 2961 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ 𝑠:ℤ⟶𝑔)) → ∀𝑘𝑍𝑥 ∈ ( I ‘𝑋)𝑥 𝑛 ∈ (𝑀...𝑘)(𝑠𝑛))
7675adantrrr 760 . . . . . . . . . 10 (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) → ∀𝑘𝑍𝑥 ∈ ( I ‘𝑋)𝑥 𝑛 ∈ (𝑀...𝑘)(𝑠𝑛))
77 fvex 6163 . . . . . . . . . . 11 ( I ‘𝑋) ∈ V
78 eleq1 2686 . . . . . . . . . . . 12 (𝑥 = (𝑓𝑘) → (𝑥 𝑛 ∈ (𝑀...𝑘)(𝑠𝑛) ↔ (𝑓𝑘) ∈ 𝑛 ∈ (𝑀...𝑘)(𝑠𝑛)))
79 fvex 6163 . . . . . . . . . . . . 13 (𝑓𝑘) ∈ V
80 eliin 4496 . . . . . . . . . . . . 13 ((𝑓𝑘) ∈ V → ((𝑓𝑘) ∈ 𝑛 ∈ (𝑀...𝑘)(𝑠𝑛) ↔ ∀𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛)))
8179, 80ax-mp 5 . . . . . . . . . . . 12 ((𝑓𝑘) ∈ 𝑛 ∈ (𝑀...𝑘)(𝑠𝑛) ↔ ∀𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛))
8278, 81syl6bb 276 . . . . . . . . . . 11 (𝑥 = (𝑓𝑘) → (𝑥 𝑛 ∈ (𝑀...𝑘)(𝑠𝑛) ↔ ∀𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛)))
8377, 82axcc4dom 9214 . . . . . . . . . 10 ((𝑍 ≼ ω ∧ ∀𝑘𝑍𝑥 ∈ ( I ‘𝑋)𝑥 𝑛 ∈ (𝑀...𝑘)(𝑠𝑛)) → ∃𝑓(𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛)))
8429, 76, 83syl2anc 692 . . . . . . . . 9 (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) → ∃𝑓(𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛)))
85 df-ral 2912 . . . . . . . . . . . . 13 (∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽)) ↔ ∀𝑓(𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))))
86 19.29 1798 . . . . . . . . . . . . 13 ((∀𝑓(𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ ∃𝑓(𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛))) → ∃𝑓((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛))))
8785, 86sylanb 489 . . . . . . . . . . . 12 ((∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽)) ∧ ∃𝑓(𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛))) → ∃𝑓((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛))))
8824ad2antrr 761 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛)))) → 𝑀 ∈ ℤ)
895ad2antrr 761 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛)))) → 𝐷 ∈ (Met‘𝑋))
90 simprrl 803 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛)))) → 𝑓:𝑍⟶( I ‘𝑋))
91 feq3 5990 . . . . . . . . . . . . . . . . 17 (( I ‘𝑋) = 𝑋 → (𝑓:𝑍⟶( I ‘𝑋) ↔ 𝑓:𝑍𝑋))
9289, 53, 54, 914syl 19 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛)))) → (𝑓:𝑍⟶( I ‘𝑋) ↔ 𝑓:𝑍𝑋))
9390, 92mpbid 222 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛)))) → 𝑓:𝑍𝑋)
94 simplrr 800 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛)))) → (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))
9594simprd 479 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛)))) → ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘))
96 fveq2 6153 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑖 → (𝑠𝑘) = (𝑠𝑖))
97 oveq2 6618 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑖 → ((1 / 2)↑𝑘) = ((1 / 2)↑𝑖))
9897breq2d 4630 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑖 → ((𝑢𝐷𝑣) < ((1 / 2)↑𝑘) ↔ (𝑢𝐷𝑣) < ((1 / 2)↑𝑖)))
9996, 98raleqbidv 3144 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑖 → (∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘) ↔ ∀𝑣 ∈ (𝑠𝑖)(𝑢𝐷𝑣) < ((1 / 2)↑𝑖)))
10096, 99raleqbidv 3144 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑖 → (∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘) ↔ ∀𝑢 ∈ (𝑠𝑖)∀𝑣 ∈ (𝑠𝑖)(𝑢𝐷𝑣) < ((1 / 2)↑𝑖)))
101100cbvralv 3162 . . . . . . . . . . . . . . . 16 (∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘) ↔ ∀𝑖 ∈ ℤ ∀𝑢 ∈ (𝑠𝑖)∀𝑣 ∈ (𝑠𝑖)(𝑢𝐷𝑣) < ((1 / 2)↑𝑖))
10295, 101sylib 208 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛)))) → ∀𝑖 ∈ ℤ ∀𝑢 ∈ (𝑠𝑖)∀𝑣 ∈ (𝑠𝑖)(𝑢𝐷𝑣) < ((1 / 2)↑𝑖))
103 simprrr 804 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛)))) → ∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛))
104 fveq2 6153 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑗 → (𝑠𝑛) = (𝑠𝑗))
105104eleq2d 2684 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑗 → ((𝑓𝑘) ∈ (𝑠𝑛) ↔ (𝑓𝑘) ∈ (𝑠𝑗)))
106105cbvralv 3162 . . . . . . . . . . . . . . . . . 18 (∀𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛) ↔ ∀𝑗 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑗))
107 oveq2 6618 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑖 → (𝑀...𝑘) = (𝑀...𝑖))
108 fveq2 6153 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑖 → (𝑓𝑘) = (𝑓𝑖))
109108eleq1d 2683 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑖 → ((𝑓𝑘) ∈ (𝑠𝑗) ↔ (𝑓𝑖) ∈ (𝑠𝑗)))
110107, 109raleqbidv 3144 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑖 → (∀𝑗 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑗) ↔ ∀𝑗 ∈ (𝑀...𝑖)(𝑓𝑖) ∈ (𝑠𝑗)))
111106, 110syl5bb 272 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑖 → (∀𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛) ↔ ∀𝑗 ∈ (𝑀...𝑖)(𝑓𝑖) ∈ (𝑠𝑗)))
112111cbvralv 3162 . . . . . . . . . . . . . . . 16 (∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛) ↔ ∀𝑖𝑍𝑗 ∈ (𝑀...𝑖)(𝑓𝑖) ∈ (𝑠𝑗))
113103, 112sylib 208 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛)))) → ∀𝑖𝑍𝑗 ∈ (𝑀...𝑖)(𝑓𝑖) ∈ (𝑠𝑗))
11489, 38syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛)))) → 𝐷 ∈ (∞Met‘𝑋))
115 simplrl 799 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛)))) → 𝑔 ∈ (CauFil‘𝐷))
116114, 115, 42syl2anc 692 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛)))) → 𝑔 ∈ (Fil‘𝑋))
11794simpld 475 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛)))) → 𝑠:ℤ⟶𝑔)
11826, 1, 88, 89, 93, 102, 113iscmet3lem1 23008 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛)))) → 𝑓 ∈ (Cau‘𝐷))
119 simprl 793 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛)))) → (𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))))
120118, 93, 119mp2d 49 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛)))) → 𝑓 ∈ dom (⇝𝑡𝐽))
12126, 1, 88, 89, 93, 102, 113, 116, 117, 120iscmet3lem2 23009 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛)))) → (𝐽 fLim 𝑔) ≠ ∅)
122121ex 450 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) → (((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛))) → (𝐽 fLim 𝑔) ≠ ∅))
123122exlimdv 1858 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) → (∃𝑓((𝑓 ∈ (Cau‘𝐷) → (𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛))) → (𝐽 fLim 𝑔) ≠ ∅))
12487, 123syl5 34 . . . . . . . . . . 11 ((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) → ((∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽)) ∧ ∃𝑓(𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛))) → (𝐽 fLim 𝑔) ≠ ∅))
125124expdimp 453 . . . . . . . . . 10 (((𝜑 ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) → (∃𝑓(𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛)) → (𝐽 fLim 𝑔) ≠ ∅))
126125an32s 845 . . . . . . . . 9 (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) → (∃𝑓(𝑓:𝑍⟶( I ‘𝑋) ∧ ∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝑓𝑘) ∈ (𝑠𝑛)) → (𝐽 fLim 𝑔) ≠ ∅))
12784, 126mpd 15 . . . . . . . 8 (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ (𝑔 ∈ (CauFil‘𝐷) ∧ (𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))) → (𝐽 fLim 𝑔) ≠ ∅)
128127expr 642 . . . . . . 7 (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ 𝑔 ∈ (CauFil‘𝐷)) → ((𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)) → (𝐽 fLim 𝑔) ≠ ∅))
129128exlimdv 1858 . . . . . 6 (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ 𝑔 ∈ (CauFil‘𝐷)) → (∃𝑠(𝑠:ℤ⟶𝑔 ∧ ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑠𝑘)∀𝑣 ∈ (𝑠𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)) → (𝐽 fLim 𝑔) ≠ ∅))
13023, 129mpd 15 . . . . 5 (((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) ∧ 𝑔 ∈ (CauFil‘𝐷)) → (𝐽 fLim 𝑔) ≠ ∅)
131130ralrimiva 2961 . . . 4 ((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) → ∀𝑔 ∈ (CauFil‘𝐷)(𝐽 fLim 𝑔) ≠ ∅)
1321iscmet 23001 . . . 4 (𝐷 ∈ (CMet‘𝑋) ↔ (𝐷 ∈ (Met‘𝑋) ∧ ∀𝑔 ∈ (CauFil‘𝐷)(𝐽 fLim 𝑔) ≠ ∅))
1336, 131, 132sylanbrc 697 . . 3 ((𝜑 ∧ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))) → 𝐷 ∈ (CMet‘𝑋))
134133ex 450 . 2 (𝜑 → (∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽)) → 𝐷 ∈ (CMet‘𝑋)))
1354, 134impbid2 216 1 (𝜑 → (𝐷 ∈ (CMet‘𝑋) ↔ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍𝑋𝑓 ∈ dom (⇝𝑡𝐽))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  wal 1478   = wceq 1480  wex 1701  wcel 1987  wne 2790  wral 2907  wrex 2908  {crab 2911  Vcvv 3189  cin 3558  wss 3559  c0 3896   ciin 4491   class class class wbr 4618   I cid 4989  dom cdm 5079  wf 5848  cfv 5852  (class class class)co 6610  ωcom 7019  cen 7903  cdom 7904  Fincfn 7906  ficfi 8267  1c1 9888   < clt 10025   / cdiv 10635  cn 10971  2c2 11021  cz 11328  cuz 11638  +crp 11783  ...cfz 12275  cexp 12807  ∞Metcxmt 19659  Metcme 19660  MetOpencmopn 19664  𝑡clm 20949  Filcfil 21568   fLim cflim 21657  CauFilccfil 22969  Caucca 22970  CMetcms 22971
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-inf2 8489  ax-cc 9208  ax-cnex 9943  ax-resscn 9944  ax-1cn 9945  ax-icn 9946  ax-addcl 9947  ax-addrcl 9948  ax-mulcl 9949  ax-mulrcl 9950  ax-mulcom 9951  ax-addass 9952  ax-mulass 9953  ax-distr 9954  ax-i2m1 9955  ax-1ne0 9956  ax-1rid 9957  ax-rnegex 9958  ax-rrecex 9959  ax-cnre 9960  ax-pre-lttri 9961  ax-pre-lttrn 9962  ax-pre-ltadd 9963  ax-pre-mulgt0 9964  ax-pre-sup 9965
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-iin 4493  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-oadd 7516  df-omul 7517  df-er 7694  df-map 7811  df-pm 7812  df-en 7907  df-dom 7908  df-sdom 7909  df-fin 7910  df-fi 8268  df-sup 8299  df-inf 8300  df-oi 8366  df-card 8716  df-acn 8719  df-pnf 10027  df-mnf 10028  df-xr 10029  df-ltxr 10030  df-le 10031  df-sub 10219  df-neg 10220  df-div 10636  df-nn 10972  df-2 11030  df-3 11031  df-n0 11244  df-z 11329  df-uz 11639  df-q 11740  df-rp 11784  df-xneg 11897  df-xadd 11898  df-xmul 11899  df-ico 12130  df-fz 12276  df-fl 12540  df-seq 12749  df-exp 12808  df-cj 13780  df-re 13781  df-im 13782  df-sqrt 13916  df-abs 13917  df-clim 14160  df-rlim 14161  df-rest 16011  df-topgen 16032  df-psmet 19666  df-xmet 19667  df-met 19668  df-bl 19669  df-mopn 19670  df-fbas 19671  df-fg 19672  df-top 20627  df-topon 20644  df-bases 20670  df-ntr 20743  df-nei 20821  df-lm 20952  df-fil 21569  df-fm 21661  df-flim 21662  df-flf 21663  df-cfil 22972  df-cau 22973  df-cmet 22974
This theorem is referenced by:  iscmet2  23011  iscmet3i  23029  heibor1  33268  rrncms  33291
  Copyright terms: Public domain W3C validator