Metamath Proof Explorer

Theorem fmcfil

Description: The Cauchy filter condition for a filter map. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Assertion fmcfil ⊢D∈∞Met⁡X∧B∈fBas⁡Y∧F:Y⟶X→XFilMapF⁡B∈CauFil⁡D↔∀x∈ℝ+∃y∈B∀z∈y∀w∈yF⁡zDF⁡w<x

Proof

Step Hyp Ref Expression
1 elfvdm ⊢D∈∞Met⁡X→X∈dom⁡∞Met
2 fmval ⊢X∈dom⁡∞Met∧B∈fBas⁡Y∧F:Y⟶X→XFilMapF⁡B=XfilGenran⁡y∈B⟼Fy
3 1 2 syl3an1 ⊢D∈∞Met⁡X∧B∈fBas⁡Y∧F:Y⟶X→XFilMapF⁡B=XfilGenran⁡y∈B⟼Fy
4 3 eleq1d ⊢D∈∞Met⁡X∧B∈fBas⁡Y∧F:Y⟶X→XFilMapF⁡B∈CauFil⁡D↔XfilGenran⁡y∈B⟼Fy∈CauFil⁡D
5 simp1 ⊢D∈∞Met⁡X∧B∈fBas⁡Y∧F:Y⟶X→D∈∞Met⁡X
6 simp2 ⊢D∈∞Met⁡X∧B∈fBas⁡Y∧F:Y⟶X→B∈fBas⁡Y
7 simp3 ⊢D∈∞Met⁡X∧B∈fBas⁡Y∧F:Y⟶X→F:Y⟶X
8 1 3ad2ant1 ⊢D∈∞Met⁡X∧B∈fBas⁡Y∧F:Y⟶X→X∈dom⁡∞Met
9 eqid ⊢ran⁡y∈B⟼Fy=ran⁡y∈B⟼Fy
10 9 fbasrn ⊢B∈fBas⁡Y∧F:Y⟶X∧X∈dom⁡∞Met→ran⁡y∈B⟼Fy∈fBas⁡X
11 6 7 8 10 syl3anc ⊢D∈∞Met⁡X∧B∈fBas⁡Y∧F:Y⟶X→ran⁡y∈B⟼Fy∈fBas⁡X
12 fgcfil ⊢D∈∞Met⁡X∧ran⁡y∈B⟼Fy∈fBas⁡X→XfilGenran⁡y∈B⟼Fy∈CauFil⁡D↔∀x∈ℝ+∃s∈ran⁡y∈B⟼Fy∀u∈s∀v∈suDv<x
13 5 11 12 syl2anc ⊢D∈∞Met⁡X∧B∈fBas⁡Y∧F:Y⟶X→XfilGenran⁡y∈B⟼Fy∈CauFil⁡D↔∀x∈ℝ+∃s∈ran⁡y∈B⟼Fy∀u∈s∀v∈suDv<x
14 imassrn ⊢Fy⊆ran⁡F
15 frn ⊢F:Y⟶X→ran⁡F⊆X
16 15 3ad2ant3 ⊢D∈∞Met⁡X∧B∈fBas⁡Y∧F:Y⟶X→ran⁡F⊆X
17 14 16 sstrid ⊢D∈∞Met⁡X∧B∈fBas⁡Y∧F:Y⟶X→Fy⊆X
18 8 17 ssexd ⊢D∈∞Met⁡X∧B∈fBas⁡Y∧F:Y⟶X→Fy∈V
19 18 ralrimivw ⊢D∈∞Met⁡X∧B∈fBas⁡Y∧F:Y⟶X→∀y∈BFy∈V
20 eqid ⊢y∈B⟼Fy=y∈B⟼Fy
21 raleq ⊢s=Fy→∀v∈suDv<x↔∀v∈FyuDv<x
22 21 raleqbi1dv ⊢s=Fy→∀u∈s∀v∈suDv<x↔∀u∈Fy∀v∈FyuDv<x
23 20 22 rexrnmptw ⊢∀y∈BFy∈V→∃s∈ran⁡y∈B⟼Fy∀u∈s∀v∈suDv<x↔∃y∈B∀u∈Fy∀v∈FyuDv<x
24 19 23 syl ⊢D∈∞Met⁡X∧B∈fBas⁡Y∧F:Y⟶X→∃s∈ran⁡y∈B⟼Fy∀u∈s∀v∈suDv<x↔∃y∈B∀u∈Fy∀v∈FyuDv<x
25 simpl3 ⊢D∈∞Met⁡X∧B∈fBas⁡Y∧F:Y⟶X∧y∈B→F:Y⟶X
26 25 ffnd ⊢D∈∞Met⁡X∧B∈fBas⁡Y∧F:Y⟶X∧y∈B→FFnY
27 fbelss ⊢B∈fBas⁡Y∧y∈B→y⊆Y
28 6 27 sylan ⊢D∈∞Met⁡X∧B∈fBas⁡Y∧F:Y⟶X∧y∈B→y⊆Y
29 oveq1 ⊢u=F⁡z→uDv=F⁡zDv
30 29 breq1d ⊢u=F⁡z→uDv<x↔F⁡zDv<x
31 30 ralbidv ⊢u=F⁡z→∀v∈FyuDv<x↔∀v∈FyF⁡zDv<x
32 31 ralima ⊢FFnY∧y⊆Y→∀u∈Fy∀v∈FyuDv<x↔∀z∈y∀v∈FyF⁡zDv<x
33 26 28 32 syl2anc ⊢D∈∞Met⁡X∧B∈fBas⁡Y∧F:Y⟶X∧y∈B→∀u∈Fy∀v∈FyuDv<x↔∀z∈y∀v∈FyF⁡zDv<x
34 oveq2 ⊢v=F⁡w→F⁡zDv=F⁡zDF⁡w
35 34 breq1d ⊢v=F⁡w→F⁡zDv<x↔F⁡zDF⁡w<x
36 35 ralima ⊢FFnY∧y⊆Y→∀v∈FyF⁡zDv<x↔∀w∈yF⁡zDF⁡w<x
37 26 28 36 syl2anc ⊢D∈∞Met⁡X∧B∈fBas⁡Y∧F:Y⟶X∧y∈B→∀v∈FyF⁡zDv<x↔∀w∈yF⁡zDF⁡w<x
38 37 ralbidv ⊢D∈∞Met⁡X∧B∈fBas⁡Y∧F:Y⟶X∧y∈B→∀z∈y∀v∈FyF⁡zDv<x↔∀z∈y∀w∈yF⁡zDF⁡w<x
39 33 38 bitrd ⊢D∈∞Met⁡X∧B∈fBas⁡Y∧F:Y⟶X∧y∈B→∀u∈Fy∀v∈FyuDv<x↔∀z∈y∀w∈yF⁡zDF⁡w<x
40 39 rexbidva ⊢D∈∞Met⁡X∧B∈fBas⁡Y∧F:Y⟶X→∃y∈B∀u∈Fy∀v∈FyuDv<x↔∃y∈B∀z∈y∀w∈yF⁡zDF⁡w<x
41 24 40 bitrd ⊢D∈∞Met⁡X∧B∈fBas⁡Y∧F:Y⟶X→∃s∈ran⁡y∈B⟼Fy∀u∈s∀v∈suDv<x↔∃y∈B∀z∈y∀w∈yF⁡zDF⁡w<x
42 41 ralbidv ⊢D∈∞Met⁡X∧B∈fBas⁡Y∧F:Y⟶X→∀x∈ℝ+∃s∈ran⁡y∈B⟼Fy∀u∈s∀v∈suDv<x↔∀x∈ℝ+∃y∈B∀z∈y∀w∈yF⁡zDF⁡w<x
43 4 13 42 3bitrd ⊢D∈∞Met⁡X∧B∈fBas⁡Y∧F:Y⟶X→XFilMapF⁡B∈CauFil⁡D↔∀x∈ℝ+∃y∈B∀z∈y∀w∈yF⁡zDF⁡w<x