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	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) → 𝑉 ⊆ ( 𝑋 × 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		elfvex	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 ∈ V )
2		isust	⊢ ( 𝑋 ∈ V → ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ↔ ( 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ∈ 𝑈 ∧ ∀ 𝑣 ∈ 𝑈 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) ∧ ∀ 𝑤 ∈ 𝑈 ( 𝑣 ∩ 𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑈 ∧ ∃ 𝑤 ∈ 𝑈 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) ) )
3	1 2	syl	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ↔ ( 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ∈ 𝑈 ∧ ∀ 𝑣 ∈ 𝑈 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) ∧ ∀ 𝑤 ∈ 𝑈 ( 𝑣 ∩ 𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑈 ∧ ∃ 𝑤 ∈ 𝑈 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) ) )
4	3	ibi	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ∈ 𝑈 ∧ ∀ 𝑣 ∈ 𝑈 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) ∧ ∀ 𝑤 ∈ 𝑈 ( 𝑣 ∩ 𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑈 ∧ ∃ 𝑤 ∈ 𝑈 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) )
5	4	simp1d	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) )
6	5	sselda	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) → 𝑉 ∈ 𝒫 ( 𝑋 × 𝑋 ) )
7	6	elpwid	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) → 𝑉 ⊆ ( 𝑋 × 𝑋 ) )