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

Theorem caucfil 22834
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 1032 . . . . . . . 8 ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋) ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
2 caucfil.1 . . . . . . . . . . . . . 14 𝑍 = (ℤ𝑀)
32uztrn2 11540 . . . . . . . . . . . . 13 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → 𝑘𝑍)
43adantll 745 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝑘𝑍)
5 simpll3 1094 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝐹:𝑍𝑋)
6 fdm 5950 . . . . . . . . . . . . 13 (𝐹:𝑍𝑋 → dom 𝐹 = 𝑍)
75, 6syl 17 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → dom 𝐹 = 𝑍)
84, 7eleqtrrd 2690 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝑘 ∈ dom 𝐹)
95, 4ffvelrnd 6253 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) ∈ 𝑋)
108, 9jca 552 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋))
1110biantrurd 527 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥 ↔ ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋) ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)))
12 uzss 11543 . . . . . . . . . . . . . . 15 (𝑘 ∈ (ℤ𝑗) → (ℤ𝑘) ⊆ (ℤ𝑗))
1312adantl 480 . . . . . . . . . . . . . 14 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (ℤ𝑘) ⊆ (ℤ𝑗))
1413sseld 3566 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝑚 ∈ (ℤ𝑘) → 𝑚 ∈ (ℤ𝑗)))
1514pm4.71rd 664 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝑚 ∈ (ℤ𝑘) ↔ (𝑚 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑘))))
1615imbi1d 329 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → ((𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ ((𝑚 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑘)) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)))
17 impexp 460 . . . . . . . . . . 11 (((𝑚 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑘)) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ (𝑚 ∈ (ℤ𝑗) → (𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)))
1816, 17syl6bb 274 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → ((𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ (𝑚 ∈ (ℤ𝑗) → (𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))))
1918ralbidv2 2966 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥 ↔ ∀𝑚 ∈ (ℤ𝑗)(𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)))
2011, 19bitr3d 268 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋) ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ ∀𝑚 ∈ (ℤ𝑗)(𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)))
211, 20syl5bb 270 . . . . . . 7 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → ((𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ ∀𝑚 ∈ (ℤ𝑗)(𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)))
2221ralbidva 2967 . . . . . 6 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)(𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)))
23 r19.26-2 3046 . . . . . . . 8 (∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)((𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ∧ (𝑘 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑘)) < 𝑥)) ↔ (∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)(𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ∧ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)(𝑘 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑘)) < 𝑥)))
24 eleq1 2675 . . . . . . . . . . . . 13 (𝑢 = 𝑘 → (𝑢 ∈ (ℤ𝑚) ↔ 𝑘 ∈ (ℤ𝑚)))
25 fveq2 6088 . . . . . . . . . . . . . . 15 (𝑢 = 𝑘 → (𝐹𝑢) = (𝐹𝑘))
2625oveq2d 6543 . . . . . . . . . . . . . 14 (𝑢 = 𝑘 → ((𝐹𝑚)𝐷(𝐹𝑢)) = ((𝐹𝑚)𝐷(𝐹𝑘)))
2726breq1d 4587 . . . . . . . . . . . . 13 (𝑢 = 𝑘 → (((𝐹𝑚)𝐷(𝐹𝑢)) < 𝑥 ↔ ((𝐹𝑚)𝐷(𝐹𝑘)) < 𝑥))
2824, 27imbi12d 332 . . . . . . . . . . . 12 (𝑢 = 𝑘 → ((𝑢 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑢)) < 𝑥) ↔ (𝑘 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑘)) < 𝑥)))
2928cbvralv 3146 . . . . . . . . . . 11 (∀𝑢 ∈ (ℤ𝑗)(𝑢 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑢)) < 𝑥) ↔ ∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑘)) < 𝑥))
3029ralbii 2962 . . . . . . . . . 10 (∀𝑚 ∈ (ℤ𝑗)∀𝑢 ∈ (ℤ𝑗)(𝑢 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑢)) < 𝑥) ↔ ∀𝑚 ∈ (ℤ𝑗)∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑘)) < 𝑥))
31 fveq2 6088 . . . . . . . . . . . . 13 (𝑚 = 𝑘 → (ℤ𝑚) = (ℤ𝑘))
3231eleq2d 2672 . . . . . . . . . . . 12 (𝑚 = 𝑘 → (𝑢 ∈ (ℤ𝑚) ↔ 𝑢 ∈ (ℤ𝑘)))
33 fveq2 6088 . . . . . . . . . . . . . 14 (𝑚 = 𝑘 → (𝐹𝑚) = (𝐹𝑘))
3433oveq1d 6542 . . . . . . . . . . . . 13 (𝑚 = 𝑘 → ((𝐹𝑚)𝐷(𝐹𝑢)) = ((𝐹𝑘)𝐷(𝐹𝑢)))
3534breq1d 4587 . . . . . . . . . . . 12 (𝑚 = 𝑘 → (((𝐹𝑚)𝐷(𝐹𝑢)) < 𝑥 ↔ ((𝐹𝑘)𝐷(𝐹𝑢)) < 𝑥))
3632, 35imbi12d 332 . . . . . . . . . . 11 (𝑚 = 𝑘 → ((𝑢 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑢)) < 𝑥) ↔ (𝑢 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑢)) < 𝑥)))
37 eleq1 2675 . . . . . . . . . . . 12 (𝑢 = 𝑚 → (𝑢 ∈ (ℤ𝑘) ↔ 𝑚 ∈ (ℤ𝑘)))
38 fveq2 6088 . . . . . . . . . . . . . 14 (𝑢 = 𝑚 → (𝐹𝑢) = (𝐹𝑚))
3938oveq2d 6543 . . . . . . . . . . . . 13 (𝑢 = 𝑚 → ((𝐹𝑘)𝐷(𝐹𝑢)) = ((𝐹𝑘)𝐷(𝐹𝑚)))
4039breq1d 4587 . . . . . . . . . . . 12 (𝑢 = 𝑚 → (((𝐹𝑘)𝐷(𝐹𝑢)) < 𝑥 ↔ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
4137, 40imbi12d 332 . . . . . . . . . . 11 (𝑢 = 𝑚 → ((𝑢 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑢)) < 𝑥) ↔ (𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)))
4236, 41cbvral2v 3154 . . . . . . . . . 10 (∀𝑚 ∈ (ℤ𝑗)∀𝑢 ∈ (ℤ𝑗)(𝑢 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑢)) < 𝑥) ↔ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)(𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
43 ralcom 3078 . . . . . . . . . 10 (∀𝑚 ∈ (ℤ𝑗)∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑘)) < 𝑥) ↔ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)(𝑘 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑘)) < 𝑥))
4430, 42, 433bitr3i 288 . . . . . . . . 9 (∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)(𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)(𝑘 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑘)) < 𝑥))
4544anbi2i 725 . . . . . . . 8 ((∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)(𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ∧ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)(𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)) ↔ (∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)(𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ∧ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)(𝑘 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑘)) < 𝑥)))
46 anidm 673 . . . . . . . 8 ((∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)(𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ∧ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)(𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)) ↔ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)(𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
4723, 45, 463bitr2i 286 . . . . . . 7 (∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)((𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ∧ (𝑘 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑘)) < 𝑥)) ↔ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)(𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
48 simpll1 1092 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ (𝑘 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑗))) → 𝐷 ∈ (∞Met‘𝑋))
49 simpll3 1094 . . . . . . . . . . . . . 14 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ (𝑘 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑗))) → 𝐹:𝑍𝑋)
502uztrn2 11540 . . . . . . . . . . . . . . 15 ((𝑗𝑍𝑚 ∈ (ℤ𝑗)) → 𝑚𝑍)
5150ad2ant2l 777 . . . . . . . . . . . . . 14 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ (𝑘 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑗))) → 𝑚𝑍)
5249, 51ffvelrnd 6253 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ (𝑘 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑗))) → (𝐹𝑚) ∈ 𝑋)
539adantrr 748 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ (𝑘 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑗))) → (𝐹𝑘) ∈ 𝑋)
54 xmetsym 21910 . . . . . . . . . . . . 13 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐹𝑚) ∈ 𝑋 ∧ (𝐹𝑘) ∈ 𝑋) → ((𝐹𝑚)𝐷(𝐹𝑘)) = ((𝐹𝑘)𝐷(𝐹𝑚)))
5548, 52, 53, 54syl3anc 1317 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ (𝑘 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑗))) → ((𝐹𝑚)𝐷(𝐹𝑘)) = ((𝐹𝑘)𝐷(𝐹𝑚)))
5655breq1d 4587 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ (𝑘 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑗))) → (((𝐹𝑚)𝐷(𝐹𝑘)) < 𝑥 ↔ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
5756imbi2d 328 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ (𝑘 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑗))) → ((𝑘 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑘)) < 𝑥) ↔ (𝑘 ∈ (ℤ𝑚) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)))
5857anbi2d 735 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ (𝑘 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑗))) → (((𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ∧ (𝑘 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑘)) < 𝑥)) ↔ ((𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ∧ (𝑘 ∈ (ℤ𝑚) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))))
59 jaob 817 . . . . . . . . . 10 (((𝑚 ∈ (ℤ𝑘) ∨ 𝑘 ∈ (ℤ𝑚)) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ ((𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ∧ (𝑘 ∈ (ℤ𝑚) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)))
60 eluzelz 11532 . . . . . . . . . . . . 13 (𝑘 ∈ (ℤ𝑗) → 𝑘 ∈ ℤ)
61 eluzelz 11532 . . . . . . . . . . . . 13 (𝑚 ∈ (ℤ𝑗) → 𝑚 ∈ ℤ)
62 uztric 11544 . . . . . . . . . . . . 13 ((𝑘 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑚 ∈ (ℤ𝑘) ∨ 𝑘 ∈ (ℤ𝑚)))
6360, 61, 62syl2an 492 . . . . . . . . . . . 12 ((𝑘 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑗)) → (𝑚 ∈ (ℤ𝑘) ∨ 𝑘 ∈ (ℤ𝑚)))
6463adantl 480 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ (𝑘 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑗))) → (𝑚 ∈ (ℤ𝑘) ∨ 𝑘 ∈ (ℤ𝑚)))
65 pm5.5 349 . . . . . . . . . . 11 ((𝑚 ∈ (ℤ𝑘) ∨ 𝑘 ∈ (ℤ𝑚)) → (((𝑚 ∈ (ℤ𝑘) ∨ 𝑘 ∈ (ℤ𝑚)) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
6664, 65syl 17 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ (𝑘 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑗))) → (((𝑚 ∈ (ℤ𝑘) ∨ 𝑘 ∈ (ℤ𝑚)) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
6759, 66syl5bbr 272 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ (𝑘 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑗))) → (((𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ∧ (𝑘 ∈ (ℤ𝑚) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)) ↔ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
6858, 67bitrd 266 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) ∧ (𝑘 ∈ (ℤ𝑗) ∧ 𝑚 ∈ (ℤ𝑗))) → (((𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ∧ (𝑘 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑘)) < 𝑥)) ↔ ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
69682ralbidva 2970 . . . . . . 7 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)((𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ∧ (𝑘 ∈ (ℤ𝑚) → ((𝐹𝑚)𝐷(𝐹𝑘)) < 𝑥)) ↔ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
7047, 69syl5bbr 272 . . . . . 6 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)(𝑚 ∈ (ℤ𝑘) → ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
7122, 70bitrd 266 . . . . 5 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) ∧ 𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
7271rexbidva 3030 . . . 4 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
73 uzf 11525 . . . . . 6 :ℤ⟶𝒫 ℤ
74 ffn 5944 . . . . . 6 (ℤ:ℤ⟶𝒫 ℤ → ℤ Fn ℤ)
7573, 74ax-mp 5 . . . . 5 Fn ℤ
76 uzssz 11542 . . . . . 6 (ℤ𝑀) ⊆ ℤ
772, 76eqsstri 3597 . . . . 5 𝑍 ⊆ ℤ
78 raleq 3114 . . . . . . 7 (𝑢 = (ℤ𝑗) → (∀𝑚𝑢 ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥 ↔ ∀𝑚 ∈ (ℤ𝑗)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
7978raleqbi1dv 3122 . . . . . 6 (𝑢 = (ℤ𝑗) → (∀𝑘𝑢𝑚𝑢 ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥 ↔ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
8079rexima 6379 . . . . 5 ((ℤ Fn ℤ ∧ 𝑍 ⊆ ℤ) → (∃𝑢 ∈ (ℤ𝑍)∀𝑘𝑢𝑚𝑢 ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥 ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
8175, 77, 80mp2an 703 . . . 4 (∃𝑢 ∈ (ℤ𝑍)∀𝑘𝑢𝑚𝑢 ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥 ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑗)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)
8272, 81syl6bbr 276 . . 3 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ ∃𝑢 ∈ (ℤ𝑍)∀𝑘𝑢𝑚𝑢 ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
8382ralbidv 2968 . 2 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) → (∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥) ↔ ∀𝑥 ∈ ℝ+𝑢 ∈ (ℤ𝑍)∀𝑘𝑢𝑚𝑢 ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
84 elfvdm 6115 . . . . . . 7 (𝐷 ∈ (∞Met‘𝑋) → 𝑋 ∈ dom ∞Met)
8584adantr 479 . . . . . 6 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ) → 𝑋 ∈ dom ∞Met)
86 cnex 9874 . . . . . 6 ℂ ∈ V
8785, 86jctir 558 . . . . 5 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ) → (𝑋 ∈ dom ∞Met ∧ ℂ ∈ V))
88 zsscn 11221 . . . . . . 7 ℤ ⊆ ℂ
8977, 88sstri 3576 . . . . . 6 𝑍 ⊆ ℂ
9089jctr 562 . . . . 5 (𝐹:𝑍𝑋 → (𝐹:𝑍𝑋𝑍 ⊆ ℂ))
91 elpm2r 7739 . . . . 5 (((𝑋 ∈ dom ∞Met ∧ ℂ ∈ V) ∧ (𝐹:𝑍𝑋𝑍 ⊆ ℂ)) → 𝐹 ∈ (𝑋pm ℂ))
9287, 90, 91syl2an 492 . . . 4 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ) ∧ 𝐹:𝑍𝑋) → 𝐹 ∈ (𝑋pm ℂ))
93 simpl 471 . . . . . 6 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ) → 𝐷 ∈ (∞Met‘𝑋))
94 simpr 475 . . . . . 6 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ) → 𝑀 ∈ ℤ)
952, 93, 94iscau3 22829 . . . . 5 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ) → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋pm ℂ) ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))))
9695baibd 945 . . . 4 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ) ∧ 𝐹 ∈ (𝑋pm ℂ)) → (𝐹 ∈ (Cau‘𝐷) ↔ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)))
9792, 96syldan 485 . . 3 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ) ∧ 𝐹:𝑍𝑋) → (𝐹 ∈ (Cau‘𝐷) ↔ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)))
98973impa 1250 . 2 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) → (𝐹 ∈ (Cau‘𝐷) ↔ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥)))
99 caucfil.2 . . . 4 𝐿 = ((𝑋 FilMap 𝐹)‘(ℤ𝑍))
10099eleq1i 2678 . . 3 (𝐿 ∈ (CauFil‘𝐷) ↔ ((𝑋 FilMap 𝐹)‘(ℤ𝑍)) ∈ (CauFil‘𝐷))
1012uzfbas 21460 . . . 4 (𝑀 ∈ ℤ → (ℤ𝑍) ∈ (fBas‘𝑍))
102 fmcfil 22823 . . . 4 ((𝐷 ∈ (∞Met‘𝑋) ∧ (ℤ𝑍) ∈ (fBas‘𝑍) ∧ 𝐹:𝑍𝑋) → (((𝑋 FilMap 𝐹)‘(ℤ𝑍)) ∈ (CauFil‘𝐷) ↔ ∀𝑥 ∈ ℝ+𝑢 ∈ (ℤ𝑍)∀𝑘𝑢𝑚𝑢 ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
103101, 102syl3an2 1351 . . 3 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) → (((𝑋 FilMap 𝐹)‘(ℤ𝑍)) ∈ (CauFil‘𝐷) ↔ ∀𝑥 ∈ ℝ+𝑢 ∈ (ℤ𝑍)∀𝑘𝑢𝑚𝑢 ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
104100, 103syl5bb 270 . 2 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) → (𝐿 ∈ (CauFil‘𝐷) ↔ ∀𝑥 ∈ ℝ+𝑢 ∈ (ℤ𝑍)∀𝑘𝑢𝑚𝑢 ((𝐹𝑘)𝐷(𝐹𝑚)) < 𝑥))
10583, 98, 1043bitr4d 298 1 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍𝑋) → (𝐹 ∈ (Cau‘𝐷) ↔ 𝐿 ∈ (CauFil‘𝐷)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wo 381  wa 382  w3a 1030   = wceq 1474  wcel 1976  wral 2895  wrex 2896  Vcvv 3172  wss 3539  𝒫 cpw 4107   class class class wbr 4577  dom cdm 5028  cima 5031   Fn wfn 5785  wf 5786  cfv 5790  (class class class)co 6527  pm cpm 7723  cc 9791   < clt 9931  cz 11213  cuz 11522  +crp 11667  ∞Metcxmt 19501  fBascfbas 19504   FilMap cfm 21495  CauFilccfil 22803  Caucca 22804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-cnex 9849  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869  ax-pre-mulgt0 9870
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6936  df-1st 7037  df-2nd 7038  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-er 7607  df-map 7724  df-pm 7725  df-en 7820  df-dom 7821  df-sdom 7822  df-pnf 9933  df-mnf 9934  df-xr 9935  df-ltxr 9936  df-le 9937  df-sub 10120  df-neg 10121  df-div 10537  df-nn 10871  df-2 10929  df-z 11214  df-uz 11523  df-rp 11668  df-xneg 11781  df-xadd 11782  df-xmul 11783  df-ico 12011  df-rest 15855  df-psmet 19508  df-xmet 19509  df-bl 19511  df-fbas 19513  df-fg 19514  df-fil 21408  df-fm 21500  df-cfil 22806  df-cau 22807
This theorem is referenced by:  cmetcaulem  22839
  Copyright terms: Public domain W3C validator