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 ‘ 𝑋 ) ∧ ∀ 𝑣𝑈𝑎𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) ) )