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 𝑐 ) ≠ ∅ ) ) )