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 ⊢ U ∈ UnifOn ⁡ X ∧ F ∈ CauFilU ⁡ U ∧ V ∈ U → ∃ a ∈ F a × a ⊆ V

Proof

Step Hyp Ref Expression
1 iscfilu ⊢ U ∈ UnifOn ⁡ X → F ∈ CauFilU ⁡ U ↔ F ∈ fBas ⁡ X ∧ ∀ v ∈ U ∃ a ∈ F a × a ⊆ v
2 1 simplbda ⊢ U ∈ UnifOn ⁡ X ∧ F ∈ CauFilU ⁡ U → ∀ v ∈ U ∃ a ∈ F a × a ⊆ v
3 2 3adant3 ⊢ U ∈ UnifOn ⁡ X ∧ F ∈ CauFilU ⁡ U ∧ V ∈ U → ∀ v ∈ U ∃ a ∈ F a × a ⊆ v
4 sseq2 ⊢ v = V → a × a ⊆ v ↔ a × a ⊆ V
5 4 rexbidv ⊢ v = V → ∃ a ∈ F a × a ⊆ v ↔ ∃ a ∈ F a × a ⊆ V
6 5 rspcv ⊢ V ∈ U → ∀ v ∈ U ∃ a ∈ F a × a ⊆ v → ∃ a ∈ F a × a ⊆ V
7 6 3ad2ant3 ⊢ U ∈ UnifOn ⁡ X ∧ F ∈ CauFilU ⁡ U ∧ V ∈ U → ∀ v ∈ U ∃ a ∈ F a × a ⊆ v → ∃ a ∈ F a × a ⊆ V
8 3 7 mpd ⊢ U ∈ UnifOn ⁡ X ∧ F ∈ CauFilU ⁡ U ∧ V ∈ U → ∃ a ∈ F a × a ⊆ V