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

Theorem caucfil 23062
Description: A Cauchy sequence predicate can be expressed in terms of the Cauchy filter predicate for a suitably chosen filter. (Contributed by Mario Carneiro, 13-Oct-2015.)
Hypotheses
Ref Expression
caucfil.1 𝑍 = (ℤ𝑀)
caucfil.2 𝐿 = ((𝑋 FilMap 𝐹)‘(ℤ𝑍))
Assertion
Ref Expression
caucfil ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) → (𝐹 ∈ (Cau‘𝐷) ↔ 𝐿 ∈ (CauFil‘𝐷)))

Proof of Theorem caucfil
Dummy variables 𝑗 𝑘 𝑚 𝑢 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-3an 1038 . . . . . . . 8 ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋) ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
2 caucfil.1 . . . . . . . . . . . . . 14 𝑍 = (ℤ𝑀)
32uztrn2 11690 . . . . . . . . . . . . 13 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → 𝑘𝑍)
43adantll 749 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝑘𝑍)
5 simpll3 1100 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝐹:𝑍𝑋)
6 fdm 6038 . . . . . . . . . . . . 13 (𝐹:𝑍𝑋 → dom 𝐹 = 𝑍)
75, 6syl 17 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → dom 𝐹 = 𝑍)
84, 7eleqtrrd 2702 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝑘 ∈ dom 𝐹)
95, 4ffvelrnd 6346 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) ∈ 𝑋)
108, 9jca 554 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋))
1110biantrurd 529 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥 ↔ ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋) ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)))
12 uzss 11693 . . . . . . . . . . . . . . 15 (𝑘 ∈ (ℤ𝑗) → (ℤ𝑘) ⊆ (ℤ𝑗))
1312adantl 482 . . . . . . . . . . . . . 14 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (ℤ𝑘) ⊆ (ℤ𝑗))
1413sseld 3594 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝑚 ∈ (ℤ𝑘) → 𝑚 ∈ (ℤ𝑗)))
1514pm4.71rd 666 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝑚 ∈ (ℤ𝑘) ↔ (𝑚 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑘))))
1615imbi1d 331 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → ((𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ ((𝑚 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑘)) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)))
17 impexp 462 . . . . . . . . . . 11 (((𝑚 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑘)) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ (𝑚 ∈ (ℤ𝑗) → (𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)))
1816, 17syl6bb 276 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → ((𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ (𝑚 ∈ (ℤ𝑗) → (𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))))
1918ralbidv2 2981 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥 ↔ ∀𝑚 ∈ (ℤ𝑗)(𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)))
2011, 19bitr3d 270 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋) ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ ∀𝑚 ∈ (ℤ𝑗)(𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)))
211, 20syl5bb 272 . . . . . . 7 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ ∀𝑚 ∈ (ℤ𝑗)(𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)))
2221ralbidva 2982 . . . . . 6 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)(𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)))
23 r19.26-2 3061 . . . . . . . 8 (∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)((𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ∧ (𝑘 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑘)) < 𝑥)) ↔ (∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)(𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ∧ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)(𝑘 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑘)) < 𝑥)))
24 eleq1 2687 . . . . . . . . . . . . 13 (𝑢 = 𝑘 → (𝑢 ∈ (ℤ𝑚) ↔ 𝑘 ∈ (ℤ𝑚)))
25 fveq2 6178 . . . . . . . . . . . . . . 15 (𝑢 = 𝑘 → (𝐹𝑢) = (𝐹𝑘))
2625oveq2d 6651 . . . . . . . . . . . . . 14 (𝑢 = 𝑘 → ((𝐹𝑚)𝐷(𝐹𝑢)) = ((𝐹𝑚)𝐷(𝐹𝑘)))
2726breq1d 4654 . . . . . . . . . . . . 13 (𝑢 = 𝑘 → (((𝐹𝑚)𝐷(𝐹𝑢)) < 𝑥 ↔ ((𝐹𝑚)𝐷(𝐹𝑘)) < 𝑥))
2824, 27imbi12d 334 . . . . . . . . . . . 12 (𝑢 = 𝑘 → ((𝑢 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑢)) < 𝑥) ↔ (𝑘 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑘)) < 𝑥)))
2928cbvralv 3166 . . . . . . . . . . 11 (∀𝑢 ∈ (ℤ𝑗)(𝑢 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑢)) < 𝑥) ↔ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑘)) < 𝑥))
3029ralbii 2977 . . . . . . . . . 10 (∀𝑚 ∈ (ℤ𝑗)∀𝑢 ∈ (ℤ𝑗)(𝑢 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑢)) < 𝑥) ↔ ∀𝑚 ∈ (ℤ𝑗)∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑘)) < 𝑥))
31 fveq2 6178 . . . . . . . . . . . . 13 (𝑚 = 𝑘 → (ℤ𝑚) = (ℤ𝑘))
3231eleq2d 2685 . . . . . . . . . . . 12 (𝑚 = 𝑘 → (𝑢 ∈ (ℤ𝑚) ↔ 𝑢 ∈ (ℤ𝑘)))
33 fveq2 6178 . . . . . . . . . . . . . 14 (𝑚 = 𝑘 → (𝐹𝑚) = (𝐹𝑘))
3433oveq1d 6650 . . . . . . . . . . . . 13 (𝑚 = 𝑘 → ((𝐹𝑚)𝐷(𝐹𝑢)) = ((𝐹𝑘)𝐷(𝐹𝑢)))
3534breq1d 4654 . . . . . . . . . . . 12 (𝑚 = 𝑘 → (((𝐹𝑚)𝐷(𝐹𝑢)) < 𝑥 ↔ ((𝐹𝑘)𝐷(𝐹𝑢)) < 𝑥))
3632, 35imbi12d 334 . . . . . . . . . . 11 (𝑚 = 𝑘 → ((𝑢 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑢)) < 𝑥) ↔ (𝑢 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑢)) < 𝑥)))
37 eleq1 2687 . . . . . . . . . . . 12 (𝑢 = 𝑚 → (𝑢 ∈ (ℤ𝑘) ↔ 𝑚 ∈ (ℤ𝑘)))
38 fveq2 6178 . . . . . . . . . . . . . 14 (𝑢 = 𝑚 → (𝐹𝑢) = (𝐹𝑚))
3938oveq2d 6651 . . . . . . . . . . . . 13 (𝑢 = 𝑚 → ((𝐹𝑘)𝐷(𝐹𝑢)) = ((𝐹𝑘)𝐷(𝐹𝑚)))
4039breq1d 4654 . . . . . . . . . . . 12 (𝑢 = 𝑚 → (((𝐹𝑘)𝐷(𝐹𝑢)) < 𝑥 ↔ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
4137, 40imbi12d 334 . . . . . . . . . . 11 (𝑢 = 𝑚 → ((𝑢 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑢)) < 𝑥) ↔ (𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)))
4236, 41cbvral2v 3174 . . . . . . . . . 10 (∀𝑚 ∈ (ℤ𝑗)∀𝑢 ∈ (ℤ𝑗)(𝑢 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑢)) < 𝑥) ↔ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)(𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
43 ralcom 3093 . . . . . . . . . 10 (∀𝑚 ∈ (ℤ𝑗)∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑘)) < 𝑥) ↔ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)(𝑘 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑘)) < 𝑥))
4430, 42, 433bitr3i 290 . . . . . . . . 9 (∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)(𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)(𝑘 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑘)) < 𝑥))
4544anbi2i 729 . . . . . . . 8 ((∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)(𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ∧ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)(𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)) ↔ (∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)(𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ∧ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)(𝑘 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑘)) < 𝑥)))
46 anidm 675 . . . . . . . 8 ((∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)(𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ∧ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)(𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)) ↔ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)(𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
4723, 45, 463bitr2i 288 . . . . . . 7 (∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)((𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ∧ (𝑘 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑘)) < 𝑥)) ↔ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)(𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
48 simpll1 1098 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ (𝑘 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑗))) → 𝐷 ∈ (∞Met‘𝑋))
49 simpll3 1100 . . . . . . . . . . . . . 14 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ (𝑘 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑗))) → 𝐹:𝑍𝑋)
502uztrn2 11690 . . . . . . . . . . . . . . 15 ((𝑗𝑍𝑚 ∈ (ℤ𝑗)) → 𝑚𝑍)
5150ad2ant2l 781 . . . . . . . . . . . . . 14 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ (𝑘 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑗))) → 𝑚𝑍)
5249, 51ffvelrnd 6346 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ (𝑘 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑗))) → (𝐹𝑚) ∈ 𝑋)
539adantrr 752 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ (𝑘 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑗))) → (𝐹𝑘) ∈ 𝑋)
54 xmetsym 22133 . . . . . . . . . . . . 13 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐹𝑚) ∈ 𝑋 ∧ (𝐹𝑘) ∈ 𝑋) → ((𝐹𝑚)𝐷(𝐹𝑘)) = ((𝐹𝑘)𝐷(𝐹𝑚)))
5548, 52, 53, 54syl3anc 1324 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ (𝑘 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑗))) → ((𝐹𝑚)𝐷(𝐹𝑘)) = ((𝐹𝑘)𝐷(𝐹𝑚)))
5655breq1d 4654 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ (𝑘 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑗))) → (((𝐹𝑚)𝐷(𝐹𝑘)) < 𝑥 ↔ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
5756imbi2d 330 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ (𝑘 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑗))) → ((𝑘 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑘)) < 𝑥) ↔ (𝑘 ∈ (ℤ𝑚) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)))
5857anbi2d 739 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ (𝑘 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑗))) → (((𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ∧ (𝑘 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑘)) < 𝑥)) ↔ ((𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ∧ (𝑘 ∈ (ℤ𝑚) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))))
59 jaob 821 . . . . . . . . . 10 (((𝑚 ∈ (ℤ𝑘) ∨ 𝑘 ∈ (ℤ𝑚)) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ ((𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ∧ (𝑘 ∈ (ℤ𝑚) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)))
60 eluzelz 11682 . . . . . . . . . . . . 13 (𝑘 ∈ (ℤ𝑗) → 𝑘 ∈ ℤ)
61 eluzelz 11682 . . . . . . . . . . . . 13 (𝑚 ∈ (ℤ𝑗) → 𝑚 ∈ ℤ)
62 uztric 11694 . . . . . . . . . . . . 13 ((𝑘 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑚 ∈ (ℤ𝑘) ∨ 𝑘 ∈ (ℤ𝑚)))
6360, 61, 62syl2an 494 . . . . . . . . . . . 12 ((𝑘 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑗)) → (𝑚 ∈ (ℤ𝑘) ∨ 𝑘 ∈ (ℤ𝑚)))
6463adantl 482 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ (𝑘 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑗))) → (𝑚 ∈ (ℤ𝑘) ∨ 𝑘 ∈ (ℤ𝑚)))
65 pm5.5 351 . . . . . . . . . . 11 ((𝑚 ∈ (ℤ𝑘) ∨ 𝑘 ∈ (ℤ𝑚)) → (((𝑚 ∈ (ℤ𝑘) ∨ 𝑘 ∈ (ℤ𝑚)) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
6664, 65syl 17 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ (𝑘 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑗))) → (((𝑚 ∈ (ℤ𝑘) ∨ 𝑘 ∈ (ℤ𝑚)) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
6759, 66syl5bbr 274 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ (𝑘 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑗))) → (((𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ∧ (𝑘 ∈ (ℤ𝑚) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)) ↔ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
6858, 67bitrd 268 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ (𝑘 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑗))) → (((𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ∧ (𝑘 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑘)) < 𝑥)) ↔ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
69682ralbidva 2985 . . . . . . 7 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)((𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ∧ (𝑘 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑘)) < 𝑥)) ↔ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
7047, 69syl5bbr 274 . . . . . 6 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)(𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
7122, 70bitrd 268 . . . . 5 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
7271rexbidva 3045 . . . 4 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
73 uzf 11675 . . . . . 6 :ℤ⟶𝒫 ℤ
74 ffn 6032 . . . . . 6 (ℤ:ℤ⟶𝒫 ℤ → ℤ Fn ℤ)
7573, 74ax-mp 5 . . . . 5 Fn ℤ
76 uzssz 11692 . . . . . 6 (ℤ𝑀) ⊆ ℤ
772, 76eqsstri 3627 . . . . 5 𝑍 ⊆ ℤ
78 raleq 3133 . . . . . . 7 (𝑢 = (ℤ𝑗) → (∀𝑚𝑢 ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥 ↔ ∀𝑚 ∈ (ℤ𝑗)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
7978raleqbi1dv 3141 . . . . . 6 (𝑢 = (ℤ𝑗) → (∀𝑘𝑢𝑚𝑢 ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥 ↔ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
8079rexima 6482 . . . . 5 ((ℤ Fn ℤ ∧ 𝑍 ⊆ ℤ) → (∃𝑢 ∈ (ℤ𝑍)∀𝑘𝑢𝑚𝑢 ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥 ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
8175, 77, 80mp2an 707 . . . 4 (∃𝑢 ∈ (ℤ𝑍)∀𝑘𝑢𝑚𝑢 ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥 ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)
8272, 81syl6bbr 278 . . 3 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ ∃𝑢 ∈ (ℤ𝑍)∀𝑘𝑢𝑚𝑢 ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
8382ralbidv 2983 . 2 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) → (∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ ∀𝑥 ∈ ℝ+𝑢 ∈ (ℤ𝑍)∀𝑘𝑢𝑚𝑢 ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
84 elfvdm 6207 . . . . . . 7 (𝐷 ∈ (∞Met‘𝑋) → 𝑋 ∈ dom ∞Met)
8584adantr 481 . . . . . 6 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ) → 𝑋 ∈ dom ∞Met)
86 cnex 10002 . . . . . 6 ℂ ∈ V
8785, 86jctir 560 . . . . 5 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ) → (𝑋 ∈ dom ∞Met ∧ ℂ ∈ V))
88 zsscn 11370 . . . . . . 7 ℤ ⊆ ℂ
8977, 88sstri 3604 . . . . . 6 𝑍 ⊆ ℂ
9089jctr 564 . . . . 5 (𝐹:𝑍𝑋 → (𝐹:𝑍𝑋𝑍 ⊆ ℂ))
91 elpm2r 7860 . . . . 5 (((𝑋 ∈ dom ∞Met ∧ ℂ ∈ V) ∧ (𝐹:𝑍𝑋𝑍 ⊆ ℂ)) → 𝐹 ∈ (𝑋pm ℂ))
9287, 90, 91syl2an 494 . . . 4 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ) ∧ 𝐹:𝑍𝑋) → 𝐹 ∈ (𝑋pm ℂ))
93 simpl 473 . . . . . 6 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ) → 𝐷 ∈ (∞Met‘𝑋))
94 simpr 477 . . . . . 6 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ) → 𝑀 ∈ ℤ)
952, 93, 94iscau3 23057 . . . . 5 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ) → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋pm ℂ) ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))))
9695baibd 947 . . . 4 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ) ∧ 𝐹 ∈ (𝑋pm ℂ)) → (𝐹 ∈ (Cau‘𝐷) ↔ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)))
9792, 96syldan 487 . . 3 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ) ∧ 𝐹:𝑍𝑋) → (𝐹 ∈ (Cau‘𝐷) ↔ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)))
98973impa 1257 . 2 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) → (𝐹 ∈ (Cau‘𝐷) ↔ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)))
99 caucfil.2 . . . 4 𝐿 = ((𝑋 FilMap 𝐹)‘(ℤ𝑍))
10099eleq1i 2690 . . 3 (𝐿 ∈ (CauFil‘𝐷) ↔ ((𝑋 FilMap 𝐹)‘(ℤ𝑍)) ∈ (CauFil‘𝐷))
1012uzfbas 21683 . . . 4 (𝑀 ∈ ℤ → (ℤ𝑍) ∈ (fBas‘𝑍))
102 fmcfil 23051 . . . 4 ((𝐷 ∈ (∞Met‘𝑋) ∧ (ℤ𝑍) ∈ (fBas‘𝑍) ∧ 𝐹:𝑍𝑋) → (((𝑋 FilMap 𝐹)‘(ℤ𝑍)) ∈ (CauFil‘𝐷) ↔ ∀𝑥 ∈ ℝ+𝑢 ∈ (ℤ𝑍)∀𝑘𝑢𝑚𝑢 ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
103101, 102syl3an2 1358 . . 3 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) → (((𝑋 FilMap 𝐹)‘(ℤ𝑍)) ∈ (CauFil‘𝐷) ↔ ∀𝑥 ∈ ℝ+𝑢 ∈ (ℤ𝑍)∀𝑘𝑢𝑚𝑢 ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
104100, 103syl5bb 272 . 2 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) → (𝐿 ∈ (CauFil‘𝐷) ↔ ∀𝑥 ∈ ℝ+𝑢 ∈ (ℤ𝑍)∀𝑘𝑢𝑚𝑢 ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
10583, 98, 1043bitr4d 300 1 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) → (𝐹 ∈ (Cau‘𝐷) ↔ 𝐿 ∈ (CauFil‘𝐷)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 383  wa 384  w3a 1036   = wceq 1481  wcel 1988  wral 2909  wrex 2910  Vcvv 3195  wss 3567  𝒫 cpw 4149   class class class wbr 4644  dom cdm 5104  cima 5107   Fn wfn 5871  wf 5872  cfv 5876  (class class class)co 6635  pm cpm 7843  cc 9919   < clt 10059  cz 11362  cuz 11672  +crp 11817  ∞Metcxmt 19712  fBascfbas 19715   FilMap cfm 21718  CauFilccfil 23031  Caucca 23032
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-cnex 9977  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-om 7051  df-1st 7153  df-2nd 7154  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-er 7727  df-map 7844  df-pm 7845  df-en 7941  df-dom 7942  df-sdom 7943  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-div 10670  df-nn 11006  df-2 11064  df-z 11363  df-uz 11673  df-rp 11818  df-xneg 11931  df-xadd 11932  df-xmul 11933  df-ico 12166  df-rest 16064  df-psmet 19719  df-xmet 19720  df-bl 19722  df-fbas 19724  df-fg 19725  df-fil 21631  df-fm 21723  df-cfil 23034  df-cau 23035
This theorem is referenced by:  cmetcaulem  23067
  Copyright terms: Public domain W3C validator