Metamath Proof Explorer

Theorem ustexhalf

Description: For each entourage V there is an entourage w that is "not more than half as large". Condition U_III of BourbakiTop1 p. II.1. (Contributed by Thierry Arnoux, 2-Dec-2017)

Ref Expression
Assertion ustexhalf ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U → ∃ w ∈ U w ∘ w ⊆ V

Proof

Step Hyp Ref Expression
1 elfvex ⊢ U ∈ UnifOn ⁡ X → X ∈ V
2 isust ⊢ X ∈ V → U ∈ UnifOn ⁡ X ↔ U ⊆ 𝒫 X × X ∧ X × X ∈ U ∧ ∀ v ∈ U ∀ w ∈ 𝒫 X × X v ⊆ w → w ∈ U ∧ ∀ w ∈ U v ∩ w ∈ U ∧ I ↾ X ⊆ v ∧ v -1 ∈ U ∧ ∃ w ∈ U w ∘ w ⊆ v
3 1 2 syl ⊢ U ∈ UnifOn ⁡ X → U ∈ UnifOn ⁡ X ↔ U ⊆ 𝒫 X × X ∧ X × X ∈ U ∧ ∀ v ∈ U ∀ w ∈ 𝒫 X × X v ⊆ w → w ∈ U ∧ ∀ w ∈ U v ∩ w ∈ U ∧ I ↾ X ⊆ v ∧ v -1 ∈ U ∧ ∃ w ∈ U w ∘ w ⊆ v
4 3 ibi ⊢ U ∈ UnifOn ⁡ X → U ⊆ 𝒫 X × X ∧ X × X ∈ U ∧ ∀ v ∈ U ∀ w ∈ 𝒫 X × X v ⊆ w → w ∈ U ∧ ∀ w ∈ U v ∩ w ∈ U ∧ I ↾ X ⊆ v ∧ v -1 ∈ U ∧ ∃ w ∈ U w ∘ w ⊆ v
5 4 simp3d ⊢ U ∈ UnifOn ⁡ X → ∀ v ∈ U ∀ w ∈ 𝒫 X × X v ⊆ w → w ∈ U ∧ ∀ w ∈ U v ∩ w ∈ U ∧ I ↾ X ⊆ v ∧ v -1 ∈ U ∧ ∃ w ∈ U w ∘ w ⊆ v
6 sseq1 ⊢ v = V → v ⊆ w ↔ V ⊆ w
7 6 imbi1d ⊢ v = V → v ⊆ w → w ∈ U ↔ V ⊆ w → w ∈ U
8 7 ralbidv ⊢ v = V → ∀ w ∈ 𝒫 X × X v ⊆ w → w ∈ U ↔ ∀ w ∈ 𝒫 X × X V ⊆ w → w ∈ U
9 ineq1 ⊢ v = V → v ∩ w = V ∩ w
10 9 eleq1d ⊢ v = V → v ∩ w ∈ U ↔ V ∩ w ∈ U
11 10 ralbidv ⊢ v = V → ∀ w ∈ U v ∩ w ∈ U ↔ ∀ w ∈ U V ∩ w ∈ U
12 sseq2 ⊢ v = V → I ↾ X ⊆ v ↔ I ↾ X ⊆ V
13 cnveq ⊢ v = V → v -1 = V -1
14 13 eleq1d ⊢ v = V → v -1 ∈ U ↔ V -1 ∈ U
15 sseq2 ⊢ v = V → w ∘ w ⊆ v ↔ w ∘ w ⊆ V
16 15 rexbidv ⊢ v = V → ∃ w ∈ U w ∘ w ⊆ v ↔ ∃ w ∈ U w ∘ w ⊆ V
17 12 14 16 3anbi123d ⊢ v = V → I ↾ X ⊆ v ∧ v -1 ∈ U ∧ ∃ w ∈ U w ∘ w ⊆ v ↔ I ↾ X ⊆ V ∧ V -1 ∈ U ∧ ∃ w ∈ U w ∘ w ⊆ V
18 8 11 17 3anbi123d ⊢ v = V → ∀ w ∈ 𝒫 X × X v ⊆ w → w ∈ U ∧ ∀ w ∈ U v ∩ w ∈ U ∧ I ↾ X ⊆ v ∧ v -1 ∈ U ∧ ∃ w ∈ U w ∘ w ⊆ v ↔ ∀ w ∈ 𝒫 X × X V ⊆ w → w ∈ U ∧ ∀ w ∈ U V ∩ w ∈ U ∧ I ↾ X ⊆ V ∧ V -1 ∈ U ∧ ∃ w ∈ U w ∘ w ⊆ V
19 18 rspcv ⊢ V ∈ U → ∀ v ∈ U ∀ w ∈ 𝒫 X × X v ⊆ w → w ∈ U ∧ ∀ w ∈ U v ∩ w ∈ U ∧ I ↾ X ⊆ v ∧ v -1 ∈ U ∧ ∃ w ∈ U w ∘ w ⊆ v → ∀ w ∈ 𝒫 X × X V ⊆ w → w ∈ U ∧ ∀ w ∈ U V ∩ w ∈ U ∧ I ↾ X ⊆ V ∧ V -1 ∈ U ∧ ∃ w ∈ U w ∘ w ⊆ V
20 5 19 mpan9 ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U → ∀ w ∈ 𝒫 X × X V ⊆ w → w ∈ U ∧ ∀ w ∈ U V ∩ w ∈ U ∧ I ↾ X ⊆ V ∧ V -1 ∈ U ∧ ∃ w ∈ U w ∘ w ⊆ V
21 20 simp3d ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U → I ↾ X ⊆ V ∧ V -1 ∈ U ∧ ∃ w ∈ U w ∘ w ⊆ V
22 21 simp3d ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U → ∃ w ∈ U w ∘ w ⊆ V