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