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 ‘ 𝐷 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 ) )