Metamath Proof Explorer

Theorem iscfilu

Description: The predicate " F is a Cauchy filter base on uniform space U ". (Contributed by Thierry Arnoux, 18-Nov-2017)

Ref Expression
Assertion iscfilu ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ↔ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) ) )

Proof

Step Hyp Ref Expression
1 elrnust ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑈 ∈ ∪ ran UnifOn )
2 unieq ⊢ ( 𝑢 = 𝑈 → ∪ 𝑢 = ∪ 𝑈 )
3 2 dmeqd ⊢ ( 𝑢 = 𝑈 → dom ∪ 𝑢 = dom ∪ 𝑈 )
4 3 fveq2d ⊢ ( 𝑢 = 𝑈 → ( fBas ‘ dom ∪ 𝑢 ) = ( fBas ‘ dom ∪ 𝑈 ) )
5 raleq ⊢ ( 𝑢 = 𝑈 → ( ∀ 𝑣 ∈ 𝑢 ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣 ↔ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) )
6 4 5 rabeqbidv ⊢ ( 𝑢 = 𝑈 → { 𝑓 ∈ ( fBas ‘ dom ∪ 𝑢 ) ∣ ∀ 𝑣 ∈ 𝑢 ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣 } = { 𝑓 ∈ ( fBas ‘ dom ∪ 𝑈 ) ∣ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣 } )
7 df-cfilu ⊢ CauFilu = ( 𝑢 ∈ ∪ ran UnifOn ↦ { 𝑓 ∈ ( fBas ‘ dom ∪ 𝑢 ) ∣ ∀ 𝑣 ∈ 𝑢 ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣 } )
8 fvex ⊢ ( fBas ‘ dom ∪ 𝑈 ) ∈ V
9 8 rabex ⊢ { 𝑓 ∈ ( fBas ‘ dom ∪ 𝑈 ) ∣ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣 } ∈ V
10 6 7 9 fvmpt ⊢ ( 𝑈 ∈ ∪ ran UnifOn → ( CauFilu ‘ 𝑈 ) = { 𝑓 ∈ ( fBas ‘ dom ∪ 𝑈 ) ∣ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣 } )
11 1 10 syl ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( CauFilu ‘ 𝑈 ) = { 𝑓 ∈ ( fBas ‘ dom ∪ 𝑈 ) ∣ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣 } )
12 11 eleq2d ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ↔ 𝐹 ∈ { 𝑓 ∈ ( fBas ‘ dom ∪ 𝑈 ) ∣ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣 } ) )
13 rexeq ⊢ ( 𝑓 = 𝐹 → ( ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣 ↔ ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) )
14 13 ralbidv ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣 ↔ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) )
15 14 elrab ⊢ ( 𝐹 ∈ { 𝑓 ∈ ( fBas ‘ dom ∪ 𝑈 ) ∣ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣 } ↔ ( 𝐹 ∈ ( fBas ‘ dom ∪ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) )
16 12 15 bitrdi ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ↔ ( 𝐹 ∈ ( fBas ‘ dom ∪ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) ) )
17 ustbas2 ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 = dom ∪ 𝑈 )
18 17 fveq2d ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( fBas ‘ 𝑋 ) = ( fBas ‘ dom ∪ 𝑈 ) )
19 18 eleq2d ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ↔ 𝐹 ∈ ( fBas ‘ dom ∪ 𝑈 ) ) )
20 19 anbi1d ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) ↔ ( 𝐹 ∈ ( fBas ‘ dom ∪ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) ) )
21 16 20 bitr4d ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ↔ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) ) )