Metamath Proof Explorer

Theorem ressust

Description: The uniform structure of a restricted space. (Contributed by Thierry Arnoux, 22-Jan-2018)

Ref Expression
Hypotheses ressust.x ⊢ 𝑋 = ( Base ‘ 𝑊 )
ressust.t ⊢ 𝑇 = ( UnifSt ‘ ( 𝑊 ↾s 𝐴 ) )
Assertion ressust ( ( 𝑊 ∈ UnifSp ∧ 𝐴 ⊆ 𝑋 ) → 𝑇 ∈ ( UnifOn ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ressust.x ⊢ 𝑋 = ( Base ‘ 𝑊 )
2 ressust.t ⊢ 𝑇 = ( UnifSt ‘ ( 𝑊 ↾s 𝐴 ) )
3 1 fvexi ⊢ 𝑋 ∈ V
4 3 ssex ⊢ ( 𝐴 ⊆ 𝑋 → 𝐴 ∈ V )
5 4 adantl ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ∈ V )
6 ressuss ⊢ ( 𝐴 ∈ V → ( UnifSt ‘ ( 𝑊 ↾s 𝐴 ) ) = ( ( UnifSt ‘ 𝑊 ) ↾t ( 𝐴 × 𝐴 ) ) )
7 5 6 syl ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝐴 ⊆ 𝑋 ) → ( UnifSt ‘ ( 𝑊 ↾s 𝐴 ) ) = ( ( UnifSt ‘ 𝑊 ) ↾t ( 𝐴 × 𝐴 ) ) )
8 2 7 syl5eq ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝐴 ⊆ 𝑋 ) → 𝑇 = ( ( UnifSt ‘ 𝑊 ) ↾t ( 𝐴 × 𝐴 ) ) )
9 eqid ⊢ ( UnifSt ‘ 𝑊 ) = ( UnifSt ‘ 𝑊 )
10 eqid ⊢ ( TopOpen ‘ 𝑊 ) = ( TopOpen ‘ 𝑊 )
11 1 9 10 isusp ⊢ ( 𝑊 ∈ UnifSp ↔ ( ( UnifSt ‘ 𝑊 ) ∈ ( UnifOn ‘ 𝑋 ) ∧ ( TopOpen ‘ 𝑊 ) = ( unifTop ‘ ( UnifSt ‘ 𝑊 ) ) ) )
12 11 simplbi ⊢ ( 𝑊 ∈ UnifSp → ( UnifSt ‘ 𝑊 ) ∈ ( UnifOn ‘ 𝑋 ) )
13 trust ⊢ ( ( ( UnifSt ‘ 𝑊 ) ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( UnifSt ‘ 𝑊 ) ↾t ( 𝐴 × 𝐴 ) ) ∈ ( UnifOn ‘ 𝐴 ) )
14 12 13 sylan ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝐴 ⊆ 𝑋 ) → ( ( UnifSt ‘ 𝑊 ) ↾t ( 𝐴 × 𝐴 ) ) ∈ ( UnifOn ‘ 𝐴 ) )
15 8 14 eqeltrd ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝐴 ⊆ 𝑋 ) → 𝑇 ∈ ( UnifOn ‘ 𝐴 ) )