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 ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ) → ( 𝑋 filGen 𝐹 ) ∈ ( CauFilu ‘ 𝑈 ) )

Proof

Step Hyp Ref Expression
1 cfilufbas ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
2 fgcl ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝑋 filGen 𝐹 ) ∈ ( Fil ‘ 𝑋 ) )
3 filfbas ⊢ ( ( 𝑋 filGen 𝐹 ) ∈ ( Fil ‘ 𝑋 ) → ( 𝑋 filGen 𝐹 ) ∈ ( fBas ‘ 𝑋 ) )
4 1 2 3 3syl ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ) → ( 𝑋 filGen 𝐹 ) ∈ ( fBas ‘ 𝑋 ) )
5 1 ad3antrrr ⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝐹 ) ∧ ( 𝑏 × 𝑏 ) ⊆ 𝑣 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
6 ssfg ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → 𝐹 ⊆ ( 𝑋 filGen 𝐹 ) )
7 5 6 syl ⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝐹 ) ∧ ( 𝑏 × 𝑏 ) ⊆ 𝑣 ) → 𝐹 ⊆ ( 𝑋 filGen 𝐹 ) )
8 simplr ⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝐹 ) ∧ ( 𝑏 × 𝑏 ) ⊆ 𝑣 ) → 𝑏 ∈ 𝐹 )
9 7 8 sseldd ⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝐹 ) ∧ ( 𝑏 × 𝑏 ) ⊆ 𝑣 ) → 𝑏 ∈ ( 𝑋 filGen 𝐹 ) )
10 id ⊢ ( 𝑎 = 𝑏 → 𝑎 = 𝑏 )
11 10 sqxpeqd ⊢ ( 𝑎 = 𝑏 → ( 𝑎 × 𝑎 ) = ( 𝑏 × 𝑏 ) )
12 11 sseq1d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑎 × 𝑎 ) ⊆ 𝑣 ↔ ( 𝑏 × 𝑏 ) ⊆ 𝑣 ) )
13 12 rspcev ⊢ ( ( 𝑏 ∈ ( 𝑋 filGen 𝐹 ) ∧ ( 𝑏 × 𝑏 ) ⊆ 𝑣 ) → ∃ 𝑎 ∈ ( 𝑋 filGen 𝐹 ) ( 𝑎 × 𝑎 ) ⊆ 𝑣 )
14 9 13 sylancom ⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑏 ∈ 𝐹 ) ∧ ( 𝑏 × 𝑏 ) ⊆ 𝑣 ) → ∃ 𝑎 ∈ ( 𝑋 filGen 𝐹 ) ( 𝑎 × 𝑎 ) ⊆ 𝑣 )
15 iscfilu ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ↔ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑣 ∈ 𝑈 ∃ 𝑏 ∈ 𝐹 ( 𝑏 × 𝑏 ) ⊆ 𝑣 ) ) )
16 15 simplbda ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ) → ∀ 𝑣 ∈ 𝑈 ∃ 𝑏 ∈ 𝐹 ( 𝑏 × 𝑏 ) ⊆ 𝑣 )
17 16 r19.21bi ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ) ∧ 𝑣 ∈ 𝑈 ) → ∃ 𝑏 ∈ 𝐹 ( 𝑏 × 𝑏 ) ⊆ 𝑣 )
18 14 17 r19.29a ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ) ∧ 𝑣 ∈ 𝑈 ) → ∃ 𝑎 ∈ ( 𝑋 filGen 𝐹 ) ( 𝑎 × 𝑎 ) ⊆ 𝑣 )
19 18 ralrimiva ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ) → ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ ( 𝑋 filGen 𝐹 ) ( 𝑎 × 𝑎 ) ⊆ 𝑣 )
20 iscfilu ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( ( 𝑋 filGen 𝐹 ) ∈ ( CauFilu ‘ 𝑈 ) ↔ ( ( 𝑋 filGen 𝐹 ) ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ ( 𝑋 filGen 𝐹 ) ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) ) )
21 20 adantr ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ) → ( ( 𝑋 filGen 𝐹 ) ∈ ( CauFilu ‘ 𝑈 ) ↔ ( ( 𝑋 filGen 𝐹 ) ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ ( 𝑋 filGen 𝐹 ) ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) ) )
22 4 19 21 mpbir2and ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ) → ( 𝑋 filGen 𝐹 ) ∈ ( CauFilu ‘ 𝑈 ) )