Metamath Proof Explorer

Theorem ustssxp

Description: Entourages are subsets of the Cartesian product of the base set. (Contributed by Thierry Arnoux, 19-Nov-2017)

Ref Expression
Assertion ustssxp ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U → V ⊆ X × X

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 simp1d ⊢ U ∈ UnifOn ⁡ X → U ⊆ 𝒫 X × X
6 5 sselda ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U → V ∈ 𝒫 X × X
7 6 elpwid ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U → V ⊆ X × X