Metamath Proof Explorer

Theorem cfiluweak

Description: A Cauchy filter base is also a Cauchy filter base on any coarser uniform structure. (Contributed by Thierry Arnoux, 24-Jan-2018)

Ref Expression
Assertion cfiluweak ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝐹 ∈ ( CauFilu ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) → 𝐹 ∈ ( CauFilu ‘ 𝑈 ) )

Proof

Step Hyp Ref Expression
1 trust ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ∈ ( UnifOn ‘ 𝐴 ) )
2 iscfilu ⊢ ( ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ∈ ( UnifOn ‘ 𝐴 ) → ( 𝐹 ∈ ( CauFilu ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ↔ ( 𝐹 ∈ ( fBas ‘ 𝐴 ) ∧ ∀ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑢 ) ) )
3 2 biimpa ⊢ ( ( ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ∈ ( UnifOn ‘ 𝐴 ) ∧ 𝐹 ∈ ( CauFilu ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) → ( 𝐹 ∈ ( fBas ‘ 𝐴 ) ∧ ∀ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑢 ) )
4 1 3 stoic3 ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝐹 ∈ ( CauFilu ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) → ( 𝐹 ∈ ( fBas ‘ 𝐴 ) ∧ ∀ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑢 ) )
5 4 simpld ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝐹 ∈ ( CauFilu ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) → 𝐹 ∈ ( fBas ‘ 𝐴 ) )
6 fbsspw ⊢ ( 𝐹 ∈ ( fBas ‘ 𝐴 ) → 𝐹 ⊆ 𝒫 𝐴 )
7 5 6 syl ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝐹 ∈ ( CauFilu ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) → 𝐹 ⊆ 𝒫 𝐴 )
8 simp2 ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝐹 ∈ ( CauFilu ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) → 𝐴 ⊆ 𝑋 )
9 8 sspwd ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝐹 ∈ ( CauFilu ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) → 𝒫 𝐴 ⊆ 𝒫 𝑋 )
10 7 9 sstrd ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝐹 ∈ ( CauFilu ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) → 𝐹 ⊆ 𝒫 𝑋 )
11 simp1 ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝐹 ∈ ( CauFilu ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
12 11 elfvexd ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝐹 ∈ ( CauFilu ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) → 𝑋 ∈ V )
13 fbasweak ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝐴 ) ∧ 𝐹 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ V ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
14 5 10 12 13 syl3anc ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝐹 ∈ ( CauFilu ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
15 sseq2 ⊢ ( 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) → ( ( 𝑎 × 𝑎 ) ⊆ 𝑢 ↔ ( 𝑎 × 𝑎 ) ⊆ ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) )
16 15 rexbidv ⊢ ( 𝑢 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) → ( ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑢 ↔ ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) )
17 4 simprd ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝐹 ∈ ( CauFilu ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) → ∀ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑢 )
18 17 adantr ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝐹 ∈ ( CauFilu ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑣 ∈ 𝑈 ) → ∀ 𝑢 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑢 )
19 11 adantr ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝐹 ∈ ( CauFilu ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑣 ∈ 𝑈 ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
20 12 adantr ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝐹 ∈ ( CauFilu ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑣 ∈ 𝑈 ) → 𝑋 ∈ V )
21 8 adantr ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝐹 ∈ ( CauFilu ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑣 ∈ 𝑈 ) → 𝐴 ⊆ 𝑋 )
22 20 21 ssexd ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝐹 ∈ ( CauFilu ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑣 ∈ 𝑈 ) → 𝐴 ∈ V )
23 22 22 xpexd ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝐹 ∈ ( CauFilu ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑣 ∈ 𝑈 ) → ( 𝐴 × 𝐴 ) ∈ V )
24 simpr ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝐹 ∈ ( CauFilu ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑣 ∈ 𝑈 ) → 𝑣 ∈ 𝑈 )
25 elrestr ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐴 × 𝐴 ) ∈ V ∧ 𝑣 ∈ 𝑈 ) → ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) )
26 19 23 24 25 syl3anc ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝐹 ∈ ( CauFilu ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑣 ∈ 𝑈 ) → ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) )
27 16 18 26 rspcdva ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝐹 ∈ ( CauFilu ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑣 ∈ 𝑈 ) → ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) )
28 inss1 ⊢ ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ⊆ 𝑣
29 sstr ⊢ ( ( ( 𝑎 × 𝑎 ) ⊆ ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ∧ ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ⊆ 𝑣 ) → ( 𝑎 × 𝑎 ) ⊆ 𝑣 )
30 28 29 mpan2 ⊢ ( ( 𝑎 × 𝑎 ) ⊆ ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) → ( 𝑎 × 𝑎 ) ⊆ 𝑣 )
31 30 reximi ⊢ ( ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) → ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 )
32 27 31 syl ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝐹 ∈ ( CauFilu ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) ∧ 𝑣 ∈ 𝑈 ) → ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 )
33 32 ralrimiva ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝐹 ∈ ( CauFilu ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) → ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 )
34 iscfilu ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ↔ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) ) )
35 34 3ad2ant1 ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝐹 ∈ ( CauFilu ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) → ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ↔ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) ) )
36 14 33 35 mpbir2and ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ 𝐹 ∈ ( CauFilu ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ) → 𝐹 ∈ ( CauFilu ‘ 𝑈 ) )