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

Theorem iscfil2 25314
Description: The property of being a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.)
Assertion
Ref Expression
iscfil2 (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (CauFil‘𝐷) ↔ (𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐹𝑧𝑦𝑤𝑦 (𝑧𝐷𝑤) < 𝑥)))
Distinct variable groups:   𝑥,𝑤,𝑦,𝑧,𝐹   𝑤,𝑋,𝑥,𝑦,𝑧   𝑤,𝐷,𝑥,𝑦,𝑧

Proof of Theorem iscfil2
StepHypRef Expression
1 iscfil 25313 . 2 (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (CauFil‘𝐷) ↔ (𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐹 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))))
2 xmetf 24355 . . . . . . . . 9 (𝐷 ∈ (∞Met‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
32ad3antrrr 730 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦𝐹) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
43ffund 6741 . . . . . . 7 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦𝐹) → Fun 𝐷)
5 filelss 23876 . . . . . . . . . 10 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑦𝐹) → 𝑦𝑋)
65ad4ant24 754 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦𝐹) → 𝑦𝑋)
7 xpss12 5704 . . . . . . . . 9 ((𝑦𝑋𝑦𝑋) → (𝑦 × 𝑦) ⊆ (𝑋 × 𝑋))
86, 6, 7syl2anc 584 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦𝐹) → (𝑦 × 𝑦) ⊆ (𝑋 × 𝑋))
93fdmd 6747 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦𝐹) → dom 𝐷 = (𝑋 × 𝑋))
108, 9sseqtrrd 4037 . . . . . . 7 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦𝐹) → (𝑦 × 𝑦) ⊆ dom 𝐷)
11 funimassov 7610 . . . . . . 7 ((Fun 𝐷 ∧ (𝑦 × 𝑦) ⊆ dom 𝐷) → ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) ↔ ∀𝑧𝑦𝑤𝑦 (𝑧𝐷𝑤) ∈ (0[,)𝑥)))
124, 10, 11syl2anc 584 . . . . . 6 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦𝐹) → ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) ↔ ∀𝑧𝑦𝑤𝑦 (𝑧𝐷𝑤) ∈ (0[,)𝑥)))
13 0xr 11306 . . . . . . . . 9 0 ∈ ℝ*
1413a1i 11 . . . . . . . 8 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦𝐹) ∧ (𝑧𝑦𝑤𝑦)) → 0 ∈ ℝ*)
15 simpllr 776 . . . . . . . . 9 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦𝐹) ∧ (𝑧𝑦𝑤𝑦)) → 𝑥 ∈ ℝ+)
1615rpxrd 13076 . . . . . . . 8 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦𝐹) ∧ (𝑧𝑦𝑤𝑦)) → 𝑥 ∈ ℝ*)
17 simp-4l 783 . . . . . . . . 9 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦𝐹) ∧ (𝑧𝑦𝑤𝑦)) → 𝐷 ∈ (∞Met‘𝑋))
186sselda 3995 . . . . . . . . . 10 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦𝐹) ∧ 𝑧𝑦) → 𝑧𝑋)
1918adantrr 717 . . . . . . . . 9 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦𝐹) ∧ (𝑧𝑦𝑤𝑦)) → 𝑧𝑋)
206sselda 3995 . . . . . . . . . 10 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦𝐹) ∧ 𝑤𝑦) → 𝑤𝑋)
2120adantrl 716 . . . . . . . . 9 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦𝐹) ∧ (𝑧𝑦𝑤𝑦)) → 𝑤𝑋)
22 xmetcl 24357 . . . . . . . . 9 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑧𝑋𝑤𝑋) → (𝑧𝐷𝑤) ∈ ℝ*)
2317, 19, 21, 22syl3anc 1370 . . . . . . . 8 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦𝐹) ∧ (𝑧𝑦𝑤𝑦)) → (𝑧𝐷𝑤) ∈ ℝ*)
24 xmetge0 24370 . . . . . . . . 9 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑧𝑋𝑤𝑋) → 0 ≤ (𝑧𝐷𝑤))
2517, 19, 21, 24syl3anc 1370 . . . . . . . 8 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦𝐹) ∧ (𝑧𝑦𝑤𝑦)) → 0 ≤ (𝑧𝐷𝑤))
26 elico1 13427 . . . . . . . . . 10 ((0 ∈ ℝ*𝑥 ∈ ℝ*) → ((𝑧𝐷𝑤) ∈ (0[,)𝑥) ↔ ((𝑧𝐷𝑤) ∈ ℝ* ∧ 0 ≤ (𝑧𝐷𝑤) ∧ (𝑧𝐷𝑤) < 𝑥)))
27 df-3an 1088 . . . . . . . . . 10 (((𝑧𝐷𝑤) ∈ ℝ* ∧ 0 ≤ (𝑧𝐷𝑤) ∧ (𝑧𝐷𝑤) < 𝑥) ↔ (((𝑧𝐷𝑤) ∈ ℝ* ∧ 0 ≤ (𝑧𝐷𝑤)) ∧ (𝑧𝐷𝑤) < 𝑥))
2826, 27bitrdi 287 . . . . . . . . 9 ((0 ∈ ℝ*𝑥 ∈ ℝ*) → ((𝑧𝐷𝑤) ∈ (0[,)𝑥) ↔ (((𝑧𝐷𝑤) ∈ ℝ* ∧ 0 ≤ (𝑧𝐷𝑤)) ∧ (𝑧𝐷𝑤) < 𝑥)))
2928baibd 539 . . . . . . . 8 (((0 ∈ ℝ*𝑥 ∈ ℝ*) ∧ ((𝑧𝐷𝑤) ∈ ℝ* ∧ 0 ≤ (𝑧𝐷𝑤))) → ((𝑧𝐷𝑤) ∈ (0[,)𝑥) ↔ (𝑧𝐷𝑤) < 𝑥))
3014, 16, 23, 25, 29syl22anc 839 . . . . . . 7 (((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦𝐹) ∧ (𝑧𝑦𝑤𝑦)) → ((𝑧𝐷𝑤) ∈ (0[,)𝑥) ↔ (𝑧𝐷𝑤) < 𝑥))
31302ralbidva 3217 . . . . . 6 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦𝐹) → (∀𝑧𝑦𝑤𝑦 (𝑧𝐷𝑤) ∈ (0[,)𝑥) ↔ ∀𝑧𝑦𝑤𝑦 (𝑧𝐷𝑤) < 𝑥))
3212, 31bitrd 279 . . . . 5 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) ∧ 𝑦𝐹) → ((𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) ↔ ∀𝑧𝑦𝑤𝑦 (𝑧𝐷𝑤) < 𝑥))
3332rexbidva 3175 . . . 4 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) ∧ 𝑥 ∈ ℝ+) → (∃𝑦𝐹 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) ↔ ∃𝑦𝐹𝑧𝑦𝑤𝑦 (𝑧𝐷𝑤) < 𝑥))
3433ralbidva 3174 . . 3 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (∀𝑥 ∈ ℝ+𝑦𝐹 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥) ↔ ∀𝑥 ∈ ℝ+𝑦𝐹𝑧𝑦𝑤𝑦 (𝑧𝐷𝑤) < 𝑥))
3534pm5.32da 579 . 2 (𝐷 ∈ (∞Met‘𝑋) → ((𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐹 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)) ↔ (𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐹𝑧𝑦𝑤𝑦 (𝑧𝐷𝑤) < 𝑥)))
361, 35bitrd 279 1 (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (CauFil‘𝐷) ↔ (𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑥 ∈ ℝ+𝑦𝐹𝑧𝑦𝑤𝑦 (𝑧𝐷𝑤) < 𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086  wcel 2106  wral 3059  wrex 3068  wss 3963   class class class wbr 5148   × cxp 5687  dom cdm 5689  cima 5692  Fun wfun 6557  wf 6559  cfv 6563  (class class class)co 7431  0cc0 11153  *cxr 11292   < clt 11293  cle 11294  +crp 13032  [,)cico 13386  ∞Metcxmet 21367  Filcfil 23869  CauFilccfil 25300
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-po 5597  df-so 5598  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8013  df-2nd 8014  df-er 8744  df-map 8867  df-en 8985  df-dom 8986  df-sdom 8987  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-div 11919  df-2 12327  df-rp 13033  df-xneg 13152  df-xadd 13153  df-xmul 13154  df-ico 13390  df-xmet 21375  df-fbas 21379  df-fil 23870  df-cfil 25303
This theorem is referenced by:  cfili  25316  fgcfil  25319  iscfil3  25321  cfilresi  25343  cfilres  25344
  Copyright terms: Public domain W3C validator