This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
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 𝑉 ) |