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∈Uw∘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×Xv⊆w→w∈U∧∀w∈Uv∩w∈U∧I↾X⊆v∧v-1∈U∧∃w∈Uw∘w⊆v
3 1 2 syl ⊢U∈UnifOn⁡X→U∈UnifOn⁡X↔U⊆𝒫X×X∧X×X∈U∧∀v∈U∀w∈𝒫X×Xv⊆w→w∈U∧∀w∈Uv∩w∈U∧I↾X⊆v∧v-1∈U∧∃w∈Uw∘w⊆v
4 3 ibi ⊢U∈UnifOn⁡X→U⊆𝒫X×X∧X×X∈U∧∀v∈U∀w∈𝒫X×Xv⊆w→w∈U∧∀w∈Uv∩w∈U∧I↾X⊆v∧v-1∈U∧∃w∈Uw∘w⊆v
5 4 simp3d ⊢U∈UnifOn⁡X→∀v∈U∀w∈𝒫X×Xv⊆w→w∈U∧∀w∈Uv∩w∈U∧I↾X⊆v∧v-1∈U∧∃w∈Uw∘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×Xv⊆w→w∈U↔∀w∈𝒫X×XV⊆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∈Uv∩w∈U↔∀w∈UV∩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∈Uw∘w⊆v↔∃w∈Uw∘w⊆V
17 12 14 16 3anbi123d ⊢v=V→I↾X⊆v∧v-1∈U∧∃w∈Uw∘w⊆v↔I↾X⊆V∧V-1∈U∧∃w∈Uw∘w⊆V
18 8 11 17 3anbi123d ⊢v=V→∀w∈𝒫X×Xv⊆w→w∈U∧∀w∈Uv∩w∈U∧I↾X⊆v∧v-1∈U∧∃w∈Uw∘w⊆v↔∀w∈𝒫X×XV⊆w→w∈U∧∀w∈UV∩w∈U∧I↾X⊆V∧V-1∈U∧∃w∈Uw∘w⊆V
19 18 rspcv ⊢V∈U→∀v∈U∀w∈𝒫X×Xv⊆w→w∈U∧∀w∈Uv∩w∈U∧I↾X⊆v∧v-1∈U∧∃w∈Uw∘w⊆v→∀w∈𝒫X×XV⊆w→w∈U∧∀w∈UV∩w∈U∧I↾X⊆V∧V-1∈U∧∃w∈Uw∘w⊆V
20 5 19 mpan9 ⊢U∈UnifOn⁡X∧V∈U→∀w∈𝒫X×XV⊆w→w∈U∧∀w∈UV∩w∈U∧I↾X⊆V∧V-1∈U∧∃w∈Uw∘w⊆V
21 20 simp3d ⊢U∈UnifOn⁡X∧V∈U→I↾X⊆V∧V-1∈U∧∃w∈Uw∘w⊆V
22 21 simp3d ⊢U∈UnifOn⁡X∧V∈U→∃w∈Uw∘w⊆V