Metamath Proof Explorer

Theorem cfilufg

Description: The filter generated by a Cauchy filter base is still a Cauchy filter base. (Contributed by Thierry Arnoux, 24-Jan-2018)

Ref Expression
Assertion cfilufg ⊢ U ∈ UnifOn ⁡ X ∧ F ∈ CauFilU ⁡ U → X filGen F ∈ CauFilU ⁡ U

Proof

Step Hyp Ref Expression
1 cfilufbas ⊢ U ∈ UnifOn ⁡ X ∧ F ∈ CauFilU ⁡ U → F ∈ fBas ⁡ X
2 fgcl ⊢ F ∈ fBas ⁡ X → X filGen F ∈ Fil ⁡ X
3 filfbas ⊢ X filGen F ∈ Fil ⁡ X → X filGen F ∈ fBas ⁡ X
4 1 2 3 3syl ⊢ U ∈ UnifOn ⁡ X ∧ F ∈ CauFilU ⁡ U → X filGen F ∈ fBas ⁡ X
5 1 ad3antrrr ⊢ U ∈ UnifOn ⁡ X ∧ F ∈ CauFilU ⁡ U ∧ v ∈ U ∧ b ∈ F ∧ b × b ⊆ v → F ∈ fBas ⁡ X
6 ssfg ⊢ F ∈ fBas ⁡ X → F ⊆ X filGen F
7 5 6 syl ⊢ U ∈ UnifOn ⁡ X ∧ F ∈ CauFilU ⁡ U ∧ v ∈ U ∧ b ∈ F ∧ b × b ⊆ v → F ⊆ X filGen F
8 simplr ⊢ U ∈ UnifOn ⁡ X ∧ F ∈ CauFilU ⁡ U ∧ v ∈ U ∧ b ∈ F ∧ b × b ⊆ v → b ∈ F
9 7 8 sseldd ⊢ U ∈ UnifOn ⁡ X ∧ F ∈ CauFilU ⁡ U ∧ v ∈ U ∧ b ∈ F ∧ b × b ⊆ v → b ∈ X filGen F
10 id ⊢ a = b → a = b
11 10 sqxpeqd ⊢ a = b → a × a = b × b
12 11 sseq1d ⊢ a = b → a × a ⊆ v ↔ b × b ⊆ v
13 12 rspcev ⊢ b ∈ X filGen F ∧ b × b ⊆ v → ∃ a ∈ X filGen F a × a ⊆ v
14 9 13 sylancom ⊢ U ∈ UnifOn ⁡ X ∧ F ∈ CauFilU ⁡ U ∧ v ∈ U ∧ b ∈ F ∧ b × b ⊆ v → ∃ a ∈ X filGen F a × a ⊆ v
15 iscfilu ⊢ U ∈ UnifOn ⁡ X → F ∈ CauFilU ⁡ U ↔ F ∈ fBas ⁡ X ∧ ∀ v ∈ U ∃ b ∈ F b × b ⊆ v
16 15 simplbda ⊢ U ∈ UnifOn ⁡ X ∧ F ∈ CauFilU ⁡ U → ∀ v ∈ U ∃ b ∈ F b × b ⊆ v
17 16 r19.21bi ⊢ U ∈ UnifOn ⁡ X ∧ F ∈ CauFilU ⁡ U ∧ v ∈ U → ∃ b ∈ F b × b ⊆ v
18 14 17 r19.29a ⊢ U ∈ UnifOn ⁡ X ∧ F ∈ CauFilU ⁡ U ∧ v ∈ U → ∃ a ∈ X filGen F a × a ⊆ v
19 18 ralrimiva ⊢ U ∈ UnifOn ⁡ X ∧ F ∈ CauFilU ⁡ U → ∀ v ∈ U ∃ a ∈ X filGen F a × a ⊆ v
20 iscfilu ⊢ U ∈ UnifOn ⁡ X → X filGen F ∈ CauFilU ⁡ U ↔ X filGen F ∈ fBas ⁡ X ∧ ∀ v ∈ U ∃ a ∈ X filGen F a × a ⊆ v
21 20 adantr ⊢ U ∈ UnifOn ⁡ X ∧ F ∈ CauFilU ⁡ U → X filGen F ∈ CauFilU ⁡ U ↔ X filGen F ∈ fBas ⁡ X ∧ ∀ v ∈ U ∃ a ∈ X filGen F a × a ⊆ v
22 4 19 21 mpbir2and ⊢ U ∈ UnifOn ⁡ X ∧ F ∈ CauFilU ⁡ U → X filGen F ∈ CauFilU ⁡ U