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 ⊢ X = Base W
ressust.t ⊢ T = UnifSt ⁡ W ↾ 𝑠 A
Assertion ressust ⊢ W ∈ UnifSp ∧ A ⊆ X → T ∈ UnifOn ⁡ A

Proof

Step Hyp Ref Expression
1 ressust.x ⊢ X = Base W
2 ressust.t ⊢ T = UnifSt ⁡ W ↾ 𝑠 A
3 1 fvexi ⊢ X ∈ V
4 3 ssex ⊢ A ⊆ X → A ∈ V
5 4 adantl ⊢ W ∈ UnifSp ∧ A ⊆ X → A ∈ V
6 ressuss ⊢ A ∈ V → UnifSt ⁡ W ↾ 𝑠 A = UnifSt ⁡ W ↾ 𝑡 A × A
7 5 6 syl ⊢ W ∈ UnifSp ∧ A ⊆ X → UnifSt ⁡ W ↾ 𝑠 A = UnifSt ⁡ W ↾ 𝑡 A × A
8 2 7 syl5eq ⊢ W ∈ UnifSp ∧ A ⊆ X → T = UnifSt ⁡ W ↾ 𝑡 A × A
9 eqid ⊢ UnifSt ⁡ W = UnifSt ⁡ W
10 eqid ⊢ TopOpen ⁡ W = TopOpen ⁡ W
11 1 9 10 isusp ⊢ W ∈ UnifSp ↔ UnifSt ⁡ W ∈ UnifOn ⁡ X ∧ TopOpen ⁡ W = unifTop ⁡ UnifSt ⁡ W
12 11 simplbi ⊢ W ∈ UnifSp → UnifSt ⁡ W ∈ UnifOn ⁡ X
13 trust ⊢ UnifSt ⁡ W ∈ UnifOn ⁡ X ∧ A ⊆ X → UnifSt ⁡ W ↾ 𝑡 A × A ∈ UnifOn ⁡ A
14 12 13 sylan ⊢ W ∈ UnifSp ∧ A ⊆ X → UnifSt ⁡ W ↾ 𝑡 A × A ∈ UnifOn ⁡ A
15 8 14 eqeltrd ⊢ W ∈ UnifSp ∧ A ⊆ X → T ∈ UnifOn ⁡ A