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 ⊢U∈UnifOn⁡X→F∈CauFilU⁡U↔F∈fBas⁡X∧∀v∈U∃a∈Fa×a⊆v

Proof

Step Hyp Ref Expression
1 elfvunirn ⊢U∈UnifOn⁡X→U∈⋃ran⁡UnifOn
2 unieq ⊢u=U→⋃u=⋃U
3 2 dmeqd ⊢u=U→dom⁡⋃u=dom⁡⋃U
4 3 fveq2d ⊢u=U→fBas⁡dom⁡⋃u=fBas⁡dom⁡⋃U
5 raleq ⊢u=U→∀v∈u∃a∈fa×a⊆v↔∀v∈U∃a∈fa×a⊆v
6 4 5 rabeqbidv ⊢u=U→f∈fBas⁡dom⁡⋃u|∀v∈u∃a∈fa×a⊆v=f∈fBas⁡dom⁡⋃U|∀v∈U∃a∈fa×a⊆v
7 df-cfilu ⊢CauFilU=u∈⋃ran⁡UnifOn⟼f∈fBas⁡dom⁡⋃u|∀v∈u∃a∈fa×a⊆v
8 fvex ⊢fBas⁡dom⁡⋃U∈V
9 8 rabex ⊢f∈fBas⁡dom⁡⋃U|∀v∈U∃a∈fa×a⊆v∈V
10 6 7 9 fvmpt ⊢U∈⋃ran⁡UnifOn→CauFilU⁡U=f∈fBas⁡dom⁡⋃U|∀v∈U∃a∈fa×a⊆v
11 1 10 syl ⊢U∈UnifOn⁡X→CauFilU⁡U=f∈fBas⁡dom⁡⋃U|∀v∈U∃a∈fa×a⊆v
12 11 eleq2d ⊢U∈UnifOn⁡X→F∈CauFilU⁡U↔F∈f∈fBas⁡dom⁡⋃U|∀v∈U∃a∈fa×a⊆v
13 rexeq ⊢f=F→∃a∈fa×a⊆v↔∃a∈Fa×a⊆v
14 13 ralbidv ⊢f=F→∀v∈U∃a∈fa×a⊆v↔∀v∈U∃a∈Fa×a⊆v
15 14 elrab ⊢F∈f∈fBas⁡dom⁡⋃U|∀v∈U∃a∈fa×a⊆v↔F∈fBas⁡dom⁡⋃U∧∀v∈U∃a∈Fa×a⊆v
16 12 15 bitrdi ⊢U∈UnifOn⁡X→F∈CauFilU⁡U↔F∈fBas⁡dom⁡⋃U∧∀v∈U∃a∈Fa×a⊆v
17 ustbas2 ⊢U∈UnifOn⁡X→X=dom⁡⋃U
18 17 fveq2d ⊢U∈UnifOn⁡X→fBas⁡X=fBas⁡dom⁡⋃U
19 18 eleq2d ⊢U∈UnifOn⁡X→F∈fBas⁡X↔F∈fBas⁡dom⁡⋃U
20 19 anbi1d ⊢U∈UnifOn⁡X→F∈fBas⁡X∧∀v∈U∃a∈Fa×a⊆v↔F∈fBas⁡dom⁡⋃U∧∀v∈U∃a∈Fa×a⊆v
21 16 20 bitr4d ⊢U∈UnifOn⁡X→F∈CauFilU⁡U↔F∈fBas⁡X∧∀v∈U∃a∈Fa×a⊆v