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

Metamath Proof Explorer

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 ‘ 𝑈 ) ∧ 𝑉 ∈ 𝑈 ) → ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑉 )