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

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 ‘ 𝑊 ) ) ( 𝑐 ∈ ( CauFil_u ‘ ( UnifSt ‘ 𝑊 ) ) → ( ( TopOpen ‘ 𝑊 ) fLim 𝑐 ) ≠ ∅ ) ) )

Proof

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