Metamath Proof Explorer

Theorem fgcfil

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

Ref Expression
Assertion fgcfil ⊢ D ∈ ∞Met ⁡ X ∧ B ∈ fBas ⁡ X → X filGen B ∈ CauFil ⁡ D ↔ ∀ x ∈ ℝ + ∃ y ∈ B ∀ z ∈ y ∀ w ∈ y z D w < x

Proof

Step Hyp Ref Expression
1 cfili ⊢ X filGen B ∈ CauFil ⁡ D ∧ x ∈ ℝ + → ∃ u ∈ X filGen B ∀ z ∈ u ∀ w ∈ u z D w < x
2 1 adantll ⊢ D ∈ ∞Met ⁡ X ∧ B ∈ fBas ⁡ X ∧ X filGen B ∈ CauFil ⁡ D ∧ x ∈ ℝ + → ∃ u ∈ X filGen B ∀ z ∈ u ∀ w ∈ u z D w < x
3 elfg ⊢ B ∈ fBas ⁡ X → u ∈ X filGen B ↔ u ⊆ X ∧ ∃ y ∈ B y ⊆ u
4 3 ad3antlr ⊢ D ∈ ∞Met ⁡ X ∧ B ∈ fBas ⁡ X ∧ X filGen B ∈ CauFil ⁡ D ∧ x ∈ ℝ + → u ∈ X filGen B ↔ u ⊆ X ∧ ∃ y ∈ B y ⊆ u
5 ssralv ⊢ y ⊆ u → ∀ w ∈ u z D w < x → ∀ w ∈ y z D w < x
6 5 ralimdv ⊢ y ⊆ u → ∀ z ∈ u ∀ w ∈ u z D w < x → ∀ z ∈ u ∀ w ∈ y z D w < x
7 ssralv ⊢ y ⊆ u → ∀ z ∈ u ∀ w ∈ y z D w < x → ∀ z ∈ y ∀ w ∈ y z D w < x
8 6 7 syldc ⊢ ∀ z ∈ u ∀ w ∈ u z D w < x → y ⊆ u → ∀ z ∈ y ∀ w ∈ y z D w < x
9 8 reximdv ⊢ ∀ z ∈ u ∀ w ∈ u z D w < x → ∃ y ∈ B y ⊆ u → ∃ y ∈ B ∀ z ∈ y ∀ w ∈ y z D w < x
10 9 com12 ⊢ ∃ y ∈ B y ⊆ u → ∀ z ∈ u ∀ w ∈ u z D w < x → ∃ y ∈ B ∀ z ∈ y ∀ w ∈ y z D w < x
11 10 adantl ⊢ u ⊆ X ∧ ∃ y ∈ B y ⊆ u → ∀ z ∈ u ∀ w ∈ u z D w < x → ∃ y ∈ B ∀ z ∈ y ∀ w ∈ y z D w < x
12 4 11 biimtrdi ⊢ D ∈ ∞Met ⁡ X ∧ B ∈ fBas ⁡ X ∧ X filGen B ∈ CauFil ⁡ D ∧ x ∈ ℝ + → u ∈ X filGen B → ∀ z ∈ u ∀ w ∈ u z D w < x → ∃ y ∈ B ∀ z ∈ y ∀ w ∈ y z D w < x
13 12 rexlimdv ⊢ D ∈ ∞Met ⁡ X ∧ B ∈ fBas ⁡ X ∧ X filGen B ∈ CauFil ⁡ D ∧ x ∈ ℝ + → ∃ u ∈ X filGen B ∀ z ∈ u ∀ w ∈ u z D w < x → ∃ y ∈ B ∀ z ∈ y ∀ w ∈ y z D w < x
14 2 13 mpd ⊢ D ∈ ∞Met ⁡ X ∧ B ∈ fBas ⁡ X ∧ X filGen B ∈ CauFil ⁡ D ∧ x ∈ ℝ + → ∃ y ∈ B ∀ z ∈ y ∀ w ∈ y z D w < x
15 14 ralrimiva ⊢ D ∈ ∞Met ⁡ X ∧ B ∈ fBas ⁡ X ∧ X filGen B ∈ CauFil ⁡ D → ∀ x ∈ ℝ + ∃ y ∈ B ∀ z ∈ y ∀ w ∈ y z D w < x
16 15 ex ⊢ D ∈ ∞Met ⁡ X ∧ B ∈ fBas ⁡ X → X filGen B ∈ CauFil ⁡ D → ∀ x ∈ ℝ + ∃ y ∈ B ∀ z ∈ y ∀ w ∈ y z D w < x
17 ssfg ⊢ B ∈ fBas ⁡ X → B ⊆ X filGen B
18 17 adantl ⊢ D ∈ ∞Met ⁡ X ∧ B ∈ fBas ⁡ X → B ⊆ X filGen B
19 ssrexv ⊢ B ⊆ X filGen B → ∃ y ∈ B ∀ z ∈ y ∀ w ∈ y z D w < x → ∃ y ∈ X filGen B ∀ z ∈ y ∀ w ∈ y z D w < x
20 19 ralimdv ⊢ B ⊆ X filGen B → ∀ x ∈ ℝ + ∃ y ∈ B ∀ z ∈ y ∀ w ∈ y z D w < x → ∀ x ∈ ℝ + ∃ y ∈ X filGen B ∀ z ∈ y ∀ w ∈ y z D w < x
21 18 20 syl ⊢ D ∈ ∞Met ⁡ X ∧ B ∈ fBas ⁡ X → ∀ x ∈ ℝ + ∃ y ∈ B ∀ z ∈ y ∀ w ∈ y z D w < x → ∀ x ∈ ℝ + ∃ y ∈ X filGen B ∀ z ∈ y ∀ w ∈ y z D w < x
22 fgcl ⊢ B ∈ fBas ⁡ X → X filGen B ∈ Fil ⁡ X
23 22 adantl ⊢ D ∈ ∞Met ⁡ X ∧ B ∈ fBas ⁡ X → X filGen B ∈ Fil ⁡ X
24 21 23 jctild ⊢ D ∈ ∞Met ⁡ X ∧ B ∈ fBas ⁡ X → ∀ x ∈ ℝ + ∃ y ∈ B ∀ z ∈ y ∀ w ∈ y z D w < x → X filGen B ∈ Fil ⁡ X ∧ ∀ x ∈ ℝ + ∃ y ∈ X filGen B ∀ z ∈ y ∀ w ∈ y z D w < x
25 iscfil2 ⊢ D ∈ ∞Met ⁡ X → X filGen B ∈ CauFil ⁡ D ↔ X filGen B ∈ Fil ⁡ X ∧ ∀ x ∈ ℝ + ∃ y ∈ X filGen B ∀ z ∈ y ∀ w ∈ y z D w < x
26 25 adantr ⊢ D ∈ ∞Met ⁡ X ∧ B ∈ fBas ⁡ X → X filGen B ∈ CauFil ⁡ D ↔ X filGen B ∈ Fil ⁡ X ∧ ∀ x ∈ ℝ + ∃ y ∈ X filGen B ∀ z ∈ y ∀ w ∈ y z D w < x
27 24 26 sylibrd ⊢ D ∈ ∞Met ⁡ X ∧ B ∈ fBas ⁡ X → ∀ x ∈ ℝ + ∃ y ∈ B ∀ z ∈ y ∀ w ∈ y z D w < x → X filGen B ∈ CauFil ⁡ D
28 16 27 impbid ⊢ D ∈ ∞Met ⁡ X ∧ B ∈ fBas ⁡ X → X filGen B ∈ CauFil ⁡ D ↔ ∀ x ∈ ℝ + ∃ y ∈ B ∀ z ∈ y ∀ w ∈ y z D w < x