Metamath Proof Explorer

Theorem iscusp2

Description: The predicate " W is a complete uniform space." (Contributed by Thierry Arnoux, 15-Dec-2017)

Ref Expression
Hypotheses iscusp2.1 ⊢ B = Base W
iscusp2.2 ⊢ U = UnifSt ⁡ W
iscusp2.3 ⊢ J = TopOpen ⁡ W
Assertion iscusp2 ⊢ W ∈ CUnifSp ↔ W ∈ UnifSp ∧ ∀ c ∈ Fil ⁡ B c ∈ CauFilU ⁡ U → J fLim c ≠ ∅

Proof

Step Hyp Ref Expression
1 iscusp2.1 ⊢ B = Base W
2 iscusp2.2 ⊢ U = UnifSt ⁡ W
3 iscusp2.3 ⊢ J = TopOpen ⁡ W
4 iscusp ⊢ W ∈ CUnifSp ↔ W ∈ UnifSp ∧ ∀ c ∈ Fil ⁡ Base W c ∈ CauFilU ⁡ UnifSt ⁡ W → TopOpen ⁡ W fLim c ≠ ∅
5 1 fveq2i ⊢ Fil ⁡ B = Fil ⁡ Base W
6 2 fveq2i ⊢ CauFilU ⁡ U = CauFilU ⁡ UnifSt ⁡ W
7 6 eleq2i ⊢ c ∈ CauFilU ⁡ U ↔ c ∈ CauFilU ⁡ UnifSt ⁡ W
8 3 oveq1i ⊢ J fLim c = TopOpen ⁡ W fLim c
9 8 neeq1i ⊢ J fLim c ≠ ∅ ↔ TopOpen ⁡ W fLim c ≠ ∅
10 7 9 imbi12i ⊢ c ∈ CauFilU ⁡ U → J fLim c ≠ ∅ ↔ c ∈ CauFilU ⁡ UnifSt ⁡ W → TopOpen ⁡ W fLim c ≠ ∅
11 5 10 raleqbii ⊢ ∀ c ∈ Fil ⁡ B c ∈ CauFilU ⁡ U → J fLim c ≠ ∅ ↔ ∀ c ∈ Fil ⁡ Base W c ∈ CauFilU ⁡ UnifSt ⁡ W → TopOpen ⁡ W fLim c ≠ ∅
12 11 anbi2i ⊢ W ∈ UnifSp ∧ ∀ c ∈ Fil ⁡ B c ∈ CauFilU ⁡ U → J fLim c ≠ ∅ ↔ W ∈ UnifSp ∧ ∀ c ∈ Fil ⁡ Base W c ∈ CauFilU ⁡ UnifSt ⁡ W → TopOpen ⁡ W fLim c ≠ ∅
13 4 12 bitr4i ⊢ W ∈ CUnifSp ↔ W ∈ UnifSp ∧ ∀ c ∈ Fil ⁡ B c ∈ CauFilU ⁡ U → J fLim c ≠ ∅