Metamath Proof Explorer

Theorem ustbasel

Description: The full set is always an entourage. Condition F_IIb of BourbakiTop1 p. I.36. (Contributed by Thierry Arnoux, 19-Nov-2017)

Ref Expression
Assertion ustbasel ⊢U∈UnifOn⁡X→X×X∈U

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 simp2d ⊢U∈UnifOn⁡X→X×X∈U