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 ∈ F a × a ⊆ v

Proof

Step Hyp Ref Expression
1 elrnust ⊢ 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 ∈ f a × a ⊆ v ↔ ∀ v ∈ U ∃ a ∈ f a × a ⊆ v
6 4 5 rabeqbidv ⊢ u = U → f ∈ fBas ⁡ dom ⁡ ⋃ u | ∀ v ∈ u ∃ a ∈ f a × a ⊆ v = f ∈ fBas ⁡ dom ⁡ ⋃ U | ∀ v ∈ U ∃ a ∈ f a × a ⊆ v
7 df-cfilu ⊢ CauFilU = u ∈ ⋃ ran ⁡ UnifOn ⟼ f ∈ fBas ⁡ dom ⁡ ⋃ u | ∀ v ∈ u ∃ a ∈ f a × a ⊆ v
8 fvex ⊢ fBas ⁡ dom ⁡ ⋃ U ∈ V
9 8 rabex ⊢ f ∈ fBas ⁡ dom ⁡ ⋃ U | ∀ v ∈ U ∃ a ∈ f a × a ⊆ v ∈ V
10 6 7 9 fvmpt ⊢ U ∈ ⋃ ran ⁡ UnifOn → CauFilU ⁡ U = f ∈ fBas ⁡ dom ⁡ ⋃ U | ∀ v ∈ U ∃ a ∈ f a × a ⊆ v
11 1 10 syl ⊢ U ∈ UnifOn ⁡ X → CauFilU ⁡ U = f ∈ fBas ⁡ dom ⁡ ⋃ U | ∀ v ∈ U ∃ a ∈ f a × a ⊆ v
12 11 eleq2d ⊢ U ∈ UnifOn ⁡ X → F ∈ CauFilU ⁡ U ↔ F ∈ f ∈ fBas ⁡ dom ⁡ ⋃ U | ∀ v ∈ U ∃ a ∈ f a × a ⊆ v
13 rexeq ⊢ f = F → ∃ a ∈ f a × a ⊆ v ↔ ∃ a ∈ F a × a ⊆ v
14 13 ralbidv ⊢ f = F → ∀ v ∈ U ∃ a ∈ f a × a ⊆ v ↔ ∀ v ∈ U ∃ a ∈ F a × a ⊆ v
15 14 elrab ⊢ F ∈ f ∈ fBas ⁡ dom ⁡ ⋃ U | ∀ v ∈ U ∃ a ∈ f a × a ⊆ v ↔ F ∈ fBas ⁡ dom ⁡ ⋃ U ∧ ∀ v ∈ U ∃ a ∈ F a × a ⊆ v
16 12 15 bitrdi ⊢ U ∈ UnifOn ⁡ X → F ∈ CauFilU ⁡ U ↔ F ∈ fBas ⁡ dom ⁡ ⋃ U ∧ ∀ v ∈ U ∃ a ∈ F a × 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 ∈ F a × a ⊆ v ↔ F ∈ fBas ⁡ dom ⁡ ⋃ U ∧ ∀ v ∈ U ∃ a ∈ F a × a ⊆ v
21 16 20 bitr4d ⊢ U ∈ UnifOn ⁡ X → F ∈ CauFilU ⁡ U ↔ F ∈ fBas ⁡ X ∧ ∀ v ∈ U ∃ a ∈ F a × a ⊆ v