Step |
Hyp |
Ref |
Expression |
1 |
|
om1bas.o |
⊢ 𝑂 = ( 𝐽 Ω1 𝑌 ) |
2 |
|
om1bas.j |
⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
3 |
|
om1bas.y |
⊢ ( 𝜑 → 𝑌 ∈ 𝑋 ) |
4 |
|
ovex |
⊢ ( 𝐽 ↑ko II ) ∈ V |
5 |
|
eqid |
⊢ { 〈 ( Base ‘ ndx ) , ( Base ‘ 𝑂 ) 〉 , 〈 ( +g ‘ ndx ) , ( *𝑝 ‘ 𝐽 ) 〉 , 〈 ( TopSet ‘ ndx ) , ( 𝐽 ↑ko II ) 〉 } = { 〈 ( Base ‘ ndx ) , ( Base ‘ 𝑂 ) 〉 , 〈 ( +g ‘ ndx ) , ( *𝑝 ‘ 𝐽 ) 〉 , 〈 ( TopSet ‘ ndx ) , ( 𝐽 ↑ko II ) 〉 } |
6 |
5
|
topgrptset |
⊢ ( ( 𝐽 ↑ko II ) ∈ V → ( 𝐽 ↑ko II ) = ( TopSet ‘ { 〈 ( Base ‘ ndx ) , ( Base ‘ 𝑂 ) 〉 , 〈 ( +g ‘ ndx ) , ( *𝑝 ‘ 𝐽 ) 〉 , 〈 ( TopSet ‘ ndx ) , ( 𝐽 ↑ko II ) 〉 } ) ) |
7 |
4 6
|
ax-mp |
⊢ ( 𝐽 ↑ko II ) = ( TopSet ‘ { 〈 ( Base ‘ ndx ) , ( Base ‘ 𝑂 ) 〉 , 〈 ( +g ‘ ndx ) , ( *𝑝 ‘ 𝐽 ) 〉 , 〈 ( TopSet ‘ ndx ) , ( 𝐽 ↑ko II ) 〉 } ) |
8 |
|
eqidd |
⊢ ( 𝜑 → ( Base ‘ 𝑂 ) = ( Base ‘ 𝑂 ) ) |
9 |
1 2 3 8
|
om1bas |
⊢ ( 𝜑 → ( Base ‘ 𝑂 ) = { 𝑓 ∈ ( II Cn 𝐽 ) ∣ ( ( 𝑓 ‘ 0 ) = 𝑌 ∧ ( 𝑓 ‘ 1 ) = 𝑌 ) } ) |
10 |
|
eqidd |
⊢ ( 𝜑 → ( *𝑝 ‘ 𝐽 ) = ( *𝑝 ‘ 𝐽 ) ) |
11 |
|
eqidd |
⊢ ( 𝜑 → ( 𝐽 ↑ko II ) = ( 𝐽 ↑ko II ) ) |
12 |
1 9 10 11 2 3
|
om1val |
⊢ ( 𝜑 → 𝑂 = { 〈 ( Base ‘ ndx ) , ( Base ‘ 𝑂 ) 〉 , 〈 ( +g ‘ ndx ) , ( *𝑝 ‘ 𝐽 ) 〉 , 〈 ( TopSet ‘ ndx ) , ( 𝐽 ↑ko II ) 〉 } ) |
13 |
12
|
fveq2d |
⊢ ( 𝜑 → ( TopSet ‘ 𝑂 ) = ( TopSet ‘ { 〈 ( Base ‘ ndx ) , ( Base ‘ 𝑂 ) 〉 , 〈 ( +g ‘ ndx ) , ( *𝑝 ‘ 𝐽 ) 〉 , 〈 ( TopSet ‘ ndx ) , ( 𝐽 ↑ko II ) 〉 } ) ) |
14 |
7 13
|
eqtr4id |
⊢ ( 𝜑 → ( 𝐽 ↑ko II ) = ( TopSet ‘ 𝑂 ) ) |