Metamath Proof Explorer


Theorem iscusp

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

Ref Expression
Assertion iscusp ( 𝑊 ∈ CUnifSp ↔ ( 𝑊 ∈ UnifSp ∧ ∀ 𝑐 ∈ ( Fil ‘ ( Base ‘ 𝑊 ) ) ( 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑊 ) ) → ( ( TopOpen ‘ 𝑊 ) fLim 𝑐 ) ≠ ∅ ) ) )

Proof

Step Hyp Ref Expression
1 2fveq3 ( 𝑤 = 𝑊 → ( Fil ‘ ( Base ‘ 𝑤 ) ) = ( Fil ‘ ( Base ‘ 𝑊 ) ) )
2 2fveq3 ( 𝑤 = 𝑊 → ( CauFilu ‘ ( UnifSt ‘ 𝑤 ) ) = ( CauFilu ‘ ( UnifSt ‘ 𝑊 ) ) )
3 2 eleq2d ( 𝑤 = 𝑊 → ( 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑤 ) ) ↔ 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑊 ) ) ) )
4 fveq2 ( 𝑤 = 𝑊 → ( TopOpen ‘ 𝑤 ) = ( TopOpen ‘ 𝑊 ) )
5 4 oveq1d ( 𝑤 = 𝑊 → ( ( TopOpen ‘ 𝑤 ) fLim 𝑐 ) = ( ( TopOpen ‘ 𝑊 ) fLim 𝑐 ) )
6 5 neeq1d ( 𝑤 = 𝑊 → ( ( ( TopOpen ‘ 𝑤 ) fLim 𝑐 ) ≠ ∅ ↔ ( ( TopOpen ‘ 𝑊 ) fLim 𝑐 ) ≠ ∅ ) )
7 3 6 imbi12d ( 𝑤 = 𝑊 → ( ( 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑤 ) ) → ( ( TopOpen ‘ 𝑤 ) fLim 𝑐 ) ≠ ∅ ) ↔ ( 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑊 ) ) → ( ( TopOpen ‘ 𝑊 ) fLim 𝑐 ) ≠ ∅ ) ) )
8 1 7 raleqbidv ( 𝑤 = 𝑊 → ( ∀ 𝑐 ∈ ( Fil ‘ ( Base ‘ 𝑤 ) ) ( 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑤 ) ) → ( ( TopOpen ‘ 𝑤 ) fLim 𝑐 ) ≠ ∅ ) ↔ ∀ 𝑐 ∈ ( Fil ‘ ( Base ‘ 𝑊 ) ) ( 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑊 ) ) → ( ( TopOpen ‘ 𝑊 ) fLim 𝑐 ) ≠ ∅ ) ) )
9 df-cusp CUnifSp = { 𝑤 ∈ UnifSp ∣ ∀ 𝑐 ∈ ( Fil ‘ ( Base ‘ 𝑤 ) ) ( 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑤 ) ) → ( ( TopOpen ‘ 𝑤 ) fLim 𝑐 ) ≠ ∅ ) }
10 8 9 elrab2 ( 𝑊 ∈ CUnifSp ↔ ( 𝑊 ∈ UnifSp ∧ ∀ 𝑐 ∈ ( Fil ‘ ( Base ‘ 𝑊 ) ) ( 𝑐 ∈ ( CauFilu ‘ ( UnifSt ‘ 𝑊 ) ) → ( ( TopOpen ‘ 𝑊 ) fLim 𝑐 ) ≠ ∅ ) ) )