This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) → ( ( 𝑋 filGen 𝐵 ) ∈ ( CauFil ‘ 𝐷 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 ) )

Proof

Step Hyp Ref Expression
1 cfili ⊢ ( ( ( 𝑋 filGen 𝐵 ) ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑢 ∈ ( 𝑋 filGen 𝐵 ) ∀ 𝑧 ∈ 𝑢 ∀ 𝑤 ∈ 𝑢 ( 𝑧 𝐷 𝑤 ) < 𝑥 )
2 1 adantll ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ ( 𝑋 filGen 𝐵 ) ∈ ( CauFil ‘ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑢 ∈ ( 𝑋 filGen 𝐵 ) ∀ 𝑧 ∈ 𝑢 ∀ 𝑤 ∈ 𝑢 ( 𝑧 𝐷 𝑤 ) < 𝑥 )
3 elfg ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑋 ) → ( 𝑢 ∈ ( 𝑋 filGen 𝐵 ) ↔ ( 𝑢 ⊆ 𝑋 ∧ ∃ 𝑦 ∈ 𝐵 𝑦 ⊆ 𝑢 ) ) )
4 3 ad3antlr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ ( 𝑋 filGen 𝐵 ) ∈ ( CauFil ‘ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝑢 ∈ ( 𝑋 filGen 𝐵 ) ↔ ( 𝑢 ⊆ 𝑋 ∧ ∃ 𝑦 ∈ 𝐵 𝑦 ⊆ 𝑢 ) ) )
5 ssralv ⊢ ( 𝑦 ⊆ 𝑢 → ( ∀ 𝑤 ∈ 𝑢 ( 𝑧 𝐷 𝑤 ) < 𝑥 → ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 ) )
6 5 ralimdv ⊢ ( 𝑦 ⊆ 𝑢 → ( ∀ 𝑧 ∈ 𝑢 ∀ 𝑤 ∈ 𝑢 ( 𝑧 𝐷 𝑤 ) < 𝑥 → ∀ 𝑧 ∈ 𝑢 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 ) )
7 ssralv ⊢ ( 𝑦 ⊆ 𝑢 → ( ∀ 𝑧 ∈ 𝑢 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 → ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 ) )
8 6 7 syldc ⊢ ( ∀ 𝑧 ∈ 𝑢 ∀ 𝑤 ∈ 𝑢 ( 𝑧 𝐷 𝑤 ) < 𝑥 → ( 𝑦 ⊆ 𝑢 → ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 ) )
9 8 reximdv ⊢ ( ∀ 𝑧 ∈ 𝑢 ∀ 𝑤 ∈ 𝑢 ( 𝑧 𝐷 𝑤 ) < 𝑥 → ( ∃ 𝑦 ∈ 𝐵 𝑦 ⊆ 𝑢 → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 ) )
10 9 com12 ⊢ ( ∃ 𝑦 ∈ 𝐵 𝑦 ⊆ 𝑢 → ( ∀ 𝑧 ∈ 𝑢 ∀ 𝑤 ∈ 𝑢 ( 𝑧 𝐷 𝑤 ) < 𝑥 → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 ) )
11 10 adantl ⊢ ( ( 𝑢 ⊆ 𝑋 ∧ ∃ 𝑦 ∈ 𝐵 𝑦 ⊆ 𝑢 ) → ( ∀ 𝑧 ∈ 𝑢 ∀ 𝑤 ∈ 𝑢 ( 𝑧 𝐷 𝑤 ) < 𝑥 → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 ) )
12 4 11 biimtrdi ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ ( 𝑋 filGen 𝐵 ) ∈ ( CauFil ‘ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝑢 ∈ ( 𝑋 filGen 𝐵 ) → ( ∀ 𝑧 ∈ 𝑢 ∀ 𝑤 ∈ 𝑢 ( 𝑧 𝐷 𝑤 ) < 𝑥 → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 ) ) )
13 12 rexlimdv ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ ( 𝑋 filGen 𝐵 ) ∈ ( CauFil ‘ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑢 ∈ ( 𝑋 filGen 𝐵 ) ∀ 𝑧 ∈ 𝑢 ∀ 𝑤 ∈ 𝑢 ( 𝑧 𝐷 𝑤 ) < 𝑥 → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 ) )
14 2 13 mpd ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ ( 𝑋 filGen 𝐵 ) ∈ ( CauFil ‘ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 )
15 14 ralrimiva ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ ( 𝑋 filGen 𝐵 ) ∈ ( CauFil ‘ 𝐷 ) ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 )
16 15 ex ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) → ( ( 𝑋 filGen 𝐵 ) ∈ ( CauFil ‘ 𝐷 ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 ) )
17 ssfg ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑋 ) → 𝐵 ⊆ ( 𝑋 filGen 𝐵 ) )
18 17 adantl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) → 𝐵 ⊆ ( 𝑋 filGen 𝐵 ) )
19 ssrexv ⊢ ( 𝐵 ⊆ ( 𝑋 filGen 𝐵 ) → ( ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 → ∃ 𝑦 ∈ ( 𝑋 filGen 𝐵 ) ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 ) )
20 19 ralimdv ⊢ ( 𝐵 ⊆ ( 𝑋 filGen 𝐵 ) → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ( 𝑋 filGen 𝐵 ) ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 ) )
21 18 20 syl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ( 𝑋 filGen 𝐵 ) ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 ) )
22 fgcl ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑋 ) → ( 𝑋 filGen 𝐵 ) ∈ ( Fil ‘ 𝑋 ) )
23 22 adantl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) → ( 𝑋 filGen 𝐵 ) ∈ ( Fil ‘ 𝑋 ) )
24 21 23 jctild ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 → ( ( 𝑋 filGen 𝐵 ) ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ( 𝑋 filGen 𝐵 ) ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 ) ) )
25 iscfil2 ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ( 𝑋 filGen 𝐵 ) ∈ ( CauFil ‘ 𝐷 ) ↔ ( ( 𝑋 filGen 𝐵 ) ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ( 𝑋 filGen 𝐵 ) ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 ) ) )
26 25 adantr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) → ( ( 𝑋 filGen 𝐵 ) ∈ ( CauFil ‘ 𝐷 ) ↔ ( ( 𝑋 filGen 𝐵 ) ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ( 𝑋 filGen 𝐵 ) ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 ) ) )
27 24 26 sylibrd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 → ( 𝑋 filGen 𝐵 ) ∈ ( CauFil ‘ 𝐷 ) ) )
28 16 27 impbid ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) → ( ( 𝑋 filGen 𝐵 ) ∈ ( CauFil ‘ 𝐷 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 ) )