Metamath Proof Explorer

Theorem ustssco

Description: In an uniform structure, any entourage V is a subset of its composition with itself. (Contributed by Thierry Arnoux, 5-Jan-2018)

Ref Expression
Assertion ustssco ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) → 𝑉 ⊆ ( 𝑉 ∘ 𝑉 ) )

Proof

Step Hyp Ref Expression
1 ssun1 ⊢ 𝑉 ⊆ ( 𝑉 ∪ ( 𝑉 ∘ 𝑉 ) )
2 coires1 ⊢ ( 𝑉 ∘ ( I ↾ 𝑋 ) ) = ( 𝑉 ↾ 𝑋 )
3 ustrel ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) → Rel 𝑉 )
4 ustssxp ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) → 𝑉 ⊆ ( 𝑋 × 𝑋 ) )
5 dmss ⊢ ( 𝑉 ⊆ ( 𝑋 × 𝑋 ) → dom 𝑉 ⊆ dom ( 𝑋 × 𝑋 ) )
6 4 5 syl ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) → dom 𝑉 ⊆ dom ( 𝑋 × 𝑋 ) )
7 dmxpid ⊢ dom ( 𝑋 × 𝑋 ) = 𝑋
8 6 7 sseqtrdi ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) → dom 𝑉 ⊆ 𝑋 )
9 relssres ⊢ ( ( Rel 𝑉 ∧ dom 𝑉 ⊆ 𝑋 ) → ( 𝑉 ↾ 𝑋 ) = 𝑉 )
10 3 8 9 syl2anc ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) → ( 𝑉 ↾ 𝑋 ) = 𝑉 )
11 2 10 syl5eq ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) → ( 𝑉 ∘ ( I ↾ 𝑋 ) ) = 𝑉 )
12 11 uneq1d ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) → ( ( 𝑉 ∘ ( I ↾ 𝑋 ) ) ∪ ( 𝑉 ∘ 𝑉 ) ) = ( 𝑉 ∪ ( 𝑉 ∘ 𝑉 ) ) )
13 1 12 sseqtrrid ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) → 𝑉 ⊆ ( ( 𝑉 ∘ ( I ↾ 𝑋 ) ) ∪ ( 𝑉 ∘ 𝑉 ) ) )
14 coundi ⊢ ( 𝑉 ∘ ( ( I ↾ 𝑋 ) ∪ 𝑉 ) ) = ( ( 𝑉 ∘ ( I ↾ 𝑋 ) ) ∪ ( 𝑉 ∘ 𝑉 ) )
15 13 14 sseqtrrdi ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) → 𝑉 ⊆ ( 𝑉 ∘ ( ( I ↾ 𝑋 ) ∪ 𝑉 ) ) )
16 ustdiag ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) → ( I ↾ 𝑋 ) ⊆ 𝑉 )
17 ssequn1 ⊢ ( ( I ↾ 𝑋 ) ⊆ 𝑉 ↔ ( ( I ↾ 𝑋 ) ∪ 𝑉 ) = 𝑉 )
18 16 17 sylib ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) → ( ( I ↾ 𝑋 ) ∪ 𝑉 ) = 𝑉 )
19 18 coeq2d ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) → ( 𝑉 ∘ ( ( I ↾ 𝑋 ) ∪ 𝑉 ) ) = ( 𝑉 ∘ 𝑉 ) )
20 15 19 sseqtrd ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) → 𝑉 ⊆ ( 𝑉 ∘ 𝑉 ) )