Step |
Hyp |
Ref |
Expression |
1 |
|
utopustuq.1 |
⊢ 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) ) |
2 |
|
fveq2 |
⊢ ( 𝑝 = 𝑟 → ( 𝑁 ‘ 𝑝 ) = ( 𝑁 ‘ 𝑟 ) ) |
3 |
2
|
eleq2d |
⊢ ( 𝑝 = 𝑟 → ( 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ↔ 𝑐 ∈ ( 𝑁 ‘ 𝑟 ) ) ) |
4 |
3
|
cbvralvw |
⊢ ( ∀ 𝑝 ∈ 𝑐 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ↔ ∀ 𝑟 ∈ 𝑐 𝑐 ∈ ( 𝑁 ‘ 𝑟 ) ) |
5 |
|
eleq1w |
⊢ ( 𝑐 = 𝑎 → ( 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ↔ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ) |
6 |
5
|
raleqbi1dv |
⊢ ( 𝑐 = 𝑎 → ( ∀ 𝑝 ∈ 𝑐 𝑐 ∈ ( 𝑁 ‘ 𝑝 ) ↔ ∀ 𝑝 ∈ 𝑎 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ) |
7 |
4 6
|
bitr3id |
⊢ ( 𝑐 = 𝑎 → ( ∀ 𝑟 ∈ 𝑐 𝑐 ∈ ( 𝑁 ‘ 𝑟 ) ↔ ∀ 𝑝 ∈ 𝑎 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) ) |
8 |
7
|
cbvrabv |
⊢ { 𝑐 ∈ 𝒫 𝑋 ∣ ∀ 𝑟 ∈ 𝑐 𝑐 ∈ ( 𝑁 ‘ 𝑟 ) } = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑝 ∈ 𝑎 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) } |
9 |
1
|
ustuqtop0 |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑁 : 𝑋 ⟶ 𝒫 𝒫 𝑋 ) |
10 |
1
|
ustuqtop1 |
⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ) |
11 |
1
|
ustuqtop2 |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) → ( fi ‘ ( 𝑁 ‘ 𝑝 ) ) ⊆ ( 𝑁 ‘ 𝑝 ) ) |
12 |
1
|
ustuqtop3 |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → 𝑝 ∈ 𝑎 ) |
13 |
1
|
ustuqtop4 |
⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ∀ 𝑥 ∈ 𝑏 𝑎 ∈ ( 𝑁 ‘ 𝑥 ) ) |
14 |
1
|
ustuqtop5 |
⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) → 𝑋 ∈ ( 𝑁 ‘ 𝑝 ) ) |
15 |
8 9 10 11 12 13 14
|
neiptopreu |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∃! 𝑗 ∈ ( TopOn ‘ 𝑋 ) 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ) |
16 |
9
|
feqmptd |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( 𝑁 ‘ 𝑝 ) ) ) |
17 |
16
|
eqeq1d |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ↔ ( 𝑝 ∈ 𝑋 ↦ ( 𝑁 ‘ 𝑝 ) ) = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ) ) |
18 |
|
fvex |
⊢ ( 𝑁 ‘ 𝑝 ) ∈ V |
19 |
18
|
rgenw |
⊢ ∀ 𝑝 ∈ 𝑋 ( 𝑁 ‘ 𝑝 ) ∈ V |
20 |
|
mpteqb |
⊢ ( ∀ 𝑝 ∈ 𝑋 ( 𝑁 ‘ 𝑝 ) ∈ V → ( ( 𝑝 ∈ 𝑋 ↦ ( 𝑁 ‘ 𝑝 ) ) = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ↔ ∀ 𝑝 ∈ 𝑋 ( 𝑁 ‘ 𝑝 ) = ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ) |
21 |
19 20
|
ax-mp |
⊢ ( ( 𝑝 ∈ 𝑋 ↦ ( 𝑁 ‘ 𝑝 ) ) = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ↔ ∀ 𝑝 ∈ 𝑋 ( 𝑁 ‘ 𝑝 ) = ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) |
22 |
17 21
|
bitrdi |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ↔ ∀ 𝑝 ∈ 𝑋 ( 𝑁 ‘ 𝑝 ) = ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ) |
23 |
22
|
reubidv |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( ∃! 𝑗 ∈ ( TopOn ‘ 𝑋 ) 𝑁 = ( 𝑝 ∈ 𝑋 ↦ ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ↔ ∃! 𝑗 ∈ ( TopOn ‘ 𝑋 ) ∀ 𝑝 ∈ 𝑋 ( 𝑁 ‘ 𝑝 ) = ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) ) |
24 |
15 23
|
mpbid |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∃! 𝑗 ∈ ( TopOn ‘ 𝑋 ) ∀ 𝑝 ∈ 𝑋 ( 𝑁 ‘ 𝑝 ) = ( ( nei ‘ 𝑗 ) ‘ { 𝑝 } ) ) |