Metamath Proof Explorer

Theorem tususp

Description: A constructed uniform space is an uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017)

Ref Expression
Hypothesis tuslem.k ⊢ K = toUnifSp ⁡ U
Assertion tususp ⊢ U ∈ UnifOn ⁡ X → K ∈ UnifSp

Proof

Step Hyp Ref Expression
1 tuslem.k ⊢ K = toUnifSp ⁡ U
2 id ⊢ U ∈ UnifOn ⁡ X → U ∈ UnifOn ⁡ X
3 1 tususs ⊢ U ∈ UnifOn ⁡ X → U = UnifSt ⁡ K
4 1 tusbas ⊢ U ∈ UnifOn ⁡ X → X = Base K
5 4 fveq2d ⊢ U ∈ UnifOn ⁡ X → UnifOn ⁡ X = UnifOn ⁡ Base K
6 2 3 5 3eltr3d ⊢ U ∈ UnifOn ⁡ X → UnifSt ⁡ K ∈ UnifOn ⁡ Base K
7 1 tusunif ⊢ U ∈ UnifOn ⁡ X → U = UnifSet ⁡ K
8 7 fveq2d ⊢ U ∈ UnifOn ⁡ X → unifTop ⁡ U = unifTop ⁡ UnifSet ⁡ K
9 1 tuslem ⊢ U ∈ UnifOn ⁡ X → X = Base K ∧ U = UnifSet ⁡ K ∧ unifTop ⁡ U = TopOpen ⁡ K
10 9 simp3d ⊢ U ∈ UnifOn ⁡ X → unifTop ⁡ U = TopOpen ⁡ K
11 7 3 eqtr3d ⊢ U ∈ UnifOn ⁡ X → UnifSet ⁡ K = UnifSt ⁡ K
12 11 fveq2d ⊢ U ∈ UnifOn ⁡ X → unifTop ⁡ UnifSet ⁡ K = unifTop ⁡ UnifSt ⁡ K
13 8 10 12 3eqtr3d ⊢ U ∈ UnifOn ⁡ X → TopOpen ⁡ K = unifTop ⁡ UnifSt ⁡ K
14 eqid ⊢ Base K = Base K
15 eqid ⊢ UnifSt ⁡ K = UnifSt ⁡ K
16 eqid ⊢ TopOpen ⁡ K = TopOpen ⁡ K
17 14 15 16 isusp ⊢ K ∈ UnifSp ↔ UnifSt ⁡ K ∈ UnifOn ⁡ Base K ∧ TopOpen ⁡ K = unifTop ⁡ UnifSt ⁡ K
18 6 13 17 sylanbrc ⊢ U ∈ UnifOn ⁡ X → K ∈ UnifSp