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