Step |
Hyp |
Ref |
Expression |
1 |
|
df-tus |
⊢ toUnifSp = ( 𝑢 ∈ ∪ ran UnifOn ↦ ( { 〈 ( Base ‘ ndx ) , dom ∪ 𝑢 〉 , 〈 ( UnifSet ‘ ndx ) , 𝑢 〉 } sSet 〈 ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑢 ) 〉 ) ) |
2 |
|
simpr |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → 𝑢 = 𝑈 ) |
3 |
2
|
unieqd |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → ∪ 𝑢 = ∪ 𝑈 ) |
4 |
3
|
dmeqd |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → dom ∪ 𝑢 = dom ∪ 𝑈 ) |
5 |
4
|
opeq2d |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → 〈 ( Base ‘ ndx ) , dom ∪ 𝑢 〉 = 〈 ( Base ‘ ndx ) , dom ∪ 𝑈 〉 ) |
6 |
2
|
opeq2d |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → 〈 ( UnifSet ‘ ndx ) , 𝑢 〉 = 〈 ( UnifSet ‘ ndx ) , 𝑈 〉 ) |
7 |
5 6
|
preq12d |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → { 〈 ( Base ‘ ndx ) , dom ∪ 𝑢 〉 , 〈 ( UnifSet ‘ ndx ) , 𝑢 〉 } = { 〈 ( Base ‘ ndx ) , dom ∪ 𝑈 〉 , 〈 ( UnifSet ‘ ndx ) , 𝑈 〉 } ) |
8 |
2
|
fveq2d |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → ( unifTop ‘ 𝑢 ) = ( unifTop ‘ 𝑈 ) ) |
9 |
8
|
opeq2d |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → 〈 ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑢 ) 〉 = 〈 ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑈 ) 〉 ) |
10 |
7 9
|
oveq12d |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → ( { 〈 ( Base ‘ ndx ) , dom ∪ 𝑢 〉 , 〈 ( UnifSet ‘ ndx ) , 𝑢 〉 } sSet 〈 ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑢 ) 〉 ) = ( { 〈 ( Base ‘ ndx ) , dom ∪ 𝑈 〉 , 〈 ( UnifSet ‘ ndx ) , 𝑈 〉 } sSet 〈 ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑈 ) 〉 ) ) |
11 |
|
elrnust |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑈 ∈ ∪ ran UnifOn ) |
12 |
|
ovexd |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( { 〈 ( Base ‘ ndx ) , dom ∪ 𝑈 〉 , 〈 ( UnifSet ‘ ndx ) , 𝑈 〉 } sSet 〈 ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑈 ) 〉 ) ∈ V ) |
13 |
1 10 11 12
|
fvmptd2 |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( toUnifSp ‘ 𝑈 ) = ( { 〈 ( Base ‘ ndx ) , dom ∪ 𝑈 〉 , 〈 ( UnifSet ‘ ndx ) , 𝑈 〉 } sSet 〈 ( TopSet ‘ ndx ) , ( unifTop ‘ 𝑈 ) 〉 ) ) |