Theorem cfiluexsm

Description: For a Cauchy filter base and any entourage V , there is an element of the filter small in V . (Contributed by Thierry Arnoux, 19-Nov-2017)

	Ref	Expression
Assertion	cfiluexsm	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ 𝑉 ∈ 𝑈 ) → ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		iscfilu	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ↔ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) ) )
2	1	simplbda	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ) → ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 )
3	2	3adant3	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ 𝑉 ∈ 𝑈 ) → ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 )
4		sseq2	⊢ ( 𝑣 = 𝑉 → ( ( 𝑎 × 𝑎 ) ⊆ 𝑣 ↔ ( 𝑎 × 𝑎 ) ⊆ 𝑉 ) )
5	4	rexbidv	⊢ ( 𝑣 = 𝑉 → ( ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 ↔ ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑉 ) )
6	5	rspcv	⊢ ( 𝑉 ∈ 𝑈 → ( ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 → ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑉 ) )
7	6	3ad2ant3	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ 𝑉 ∈ 𝑈 ) → ( ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 → ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑉 ) )
8	3 7	mpd	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ 𝑉 ∈ 𝑈 ) → ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑉 )