This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐵 = ( Base ‘ 𝑊 )
iscusp2.2 ⊢ 𝑈 = ( UnifSt ‘ 𝑊 )
iscusp2.3 ⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
Assertion iscusp2 ( 𝑊 ∈ CUnifSp ↔ ( 𝑊 ∈ UnifSp ∧ ∀ 𝑐 ∈ ( Fil ‘ 𝐵 ) ( 𝑐 ∈ ( CauFilu ‘ 𝑈 ) → ( 𝐽 fLim 𝑐 ) ≠ ∅ ) ) )

Proof

Step Hyp Ref Expression
1 iscusp2.1 ⊢ 𝐵 = ( Base ‘ 𝑊 )
2 iscusp2.2 ⊢ 𝑈 = ( UnifSt ‘ 𝑊 )
3 iscusp2.3 ⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
4 iscusp ⊢ ( 𝑊 ∈ CUnifSp ↔ ( 𝑊 ∈ UnifSp ∧ ∀ 𝑐 ∈ ( Fil ‘ ( Base ‘ 𝑊 ) ) ( 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑊 ) ) → ( ( TopOpen ‘ 𝑊 ) fLim 𝑐 ) ≠ ∅ ) ) )
5 1 fveq2i ⊢ ( Fil ‘ 𝐵 ) = ( Fil ‘ ( Base ‘ 𝑊 ) )
6 2 fveq2i ⊢ ( CauFilu ‘ 𝑈 ) = ( CauFilu ‘ ( UnifSt ‘ 𝑊 ) )
7 6 eleq2i ⊢ ( 𝑐 ∈ ( CauFilu ‘ 𝑈 ) ↔ 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑊 ) ) )
8 3 oveq1i ⊢ ( 𝐽 fLim 𝑐 ) = ( ( TopOpen ‘ 𝑊 ) fLim 𝑐 )
9 8 neeq1i ⊢ ( ( 𝐽 fLim 𝑐 ) ≠ ∅ ↔ ( ( TopOpen ‘ 𝑊 ) fLim 𝑐 ) ≠ ∅ )
10 7 9 imbi12i ⊢ ( ( 𝑐 ∈ ( CauFilu ‘ 𝑈 ) → ( 𝐽 fLim 𝑐 ) ≠ ∅ ) ↔ ( 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑊 ) ) → ( ( TopOpen ‘ 𝑊 ) fLim 𝑐 ) ≠ ∅ ) )
11 5 10 raleqbii ⊢ ( ∀ 𝑐 ∈ ( Fil ‘ 𝐵 ) ( 𝑐 ∈ ( CauFilu ‘ 𝑈 ) → ( 𝐽 fLim 𝑐 ) ≠ ∅ ) ↔ ∀ 𝑐 ∈ ( Fil ‘ ( Base ‘ 𝑊 ) ) ( 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑊 ) ) → ( ( TopOpen ‘ 𝑊 ) fLim 𝑐 ) ≠ ∅ ) )
12 11 anbi2i ⊢ ( ( 𝑊 ∈ UnifSp ∧ ∀ 𝑐 ∈ ( Fil ‘ 𝐵 ) ( 𝑐 ∈ ( CauFilu ‘ 𝑈 ) → ( 𝐽 fLim 𝑐 ) ≠ ∅ ) ) ↔ ( 𝑊 ∈ UnifSp ∧ ∀ 𝑐 ∈ ( Fil ‘ ( Base ‘ 𝑊 ) ) ( 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑊 ) ) → ( ( TopOpen ‘ 𝑊 ) fLim 𝑐 ) ≠ ∅ ) ) )
13 4 12 bitr4i ⊢ ( 𝑊 ∈ CUnifSp ↔ ( 𝑊 ∈ UnifSp ∧ ∀ 𝑐 ∈ ( Fil ‘ 𝐵 ) ( 𝑐 ∈ ( CauFilu ‘ 𝑈 ) → ( 𝐽 fLim 𝑐 ) ≠ ∅ ) ) )