Theorem ustrel

Description: The elements of uniform structures, called entourages, are relations. (Contributed by Thierry Arnoux, 15-Nov-2017)

	Ref	Expression
Assertion	ustrel	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) → Rel 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		ustssxp	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) → 𝑉 ⊆ ( 𝑋 × 𝑋 ) )
2		xpss	⊢ ( 𝑋 × 𝑋 ) ⊆ ( V × V )
3	1 2	sstrdi	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) → 𝑉 ⊆ ( V × V ) )
4		df-rel	⊢ ( Rel 𝑉 ↔ 𝑉 ⊆ ( V × V ) )
5	3 4	sylibr	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) → Rel 𝑉 )