Step |
Hyp |
Ref |
Expression |
1 |
|
efmndtset.g |
⊢ 𝐺 = ( EndoFMnd ‘ 𝐴 ) |
2 |
|
fvex |
⊢ ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ∈ V |
3 |
|
eqid |
⊢ { 〈 ( Base ‘ ndx ) , ( 𝐴 ↑m 𝐴 ) 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝐴 ↑m 𝐴 ) , 𝑔 ∈ ( 𝐴 ↑m 𝐴 ) ↦ ( 𝑓 ∘ 𝑔 ) ) 〉 , 〈 ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) 〉 } = { 〈 ( Base ‘ ndx ) , ( 𝐴 ↑m 𝐴 ) 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝐴 ↑m 𝐴 ) , 𝑔 ∈ ( 𝐴 ↑m 𝐴 ) ↦ ( 𝑓 ∘ 𝑔 ) ) 〉 , 〈 ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) 〉 } |
4 |
3
|
topgrptset |
⊢ ( ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) ∈ V → ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) = ( TopSet ‘ { 〈 ( Base ‘ ndx ) , ( 𝐴 ↑m 𝐴 ) 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝐴 ↑m 𝐴 ) , 𝑔 ∈ ( 𝐴 ↑m 𝐴 ) ↦ ( 𝑓 ∘ 𝑔 ) ) 〉 , 〈 ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) 〉 } ) ) |
5 |
2 4
|
ax-mp |
⊢ ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) = ( TopSet ‘ { 〈 ( Base ‘ ndx ) , ( 𝐴 ↑m 𝐴 ) 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝐴 ↑m 𝐴 ) , 𝑔 ∈ ( 𝐴 ↑m 𝐴 ) ↦ ( 𝑓 ∘ 𝑔 ) ) 〉 , 〈 ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) 〉 } ) |
6 |
|
eqid |
⊢ ( 𝐴 ↑m 𝐴 ) = ( 𝐴 ↑m 𝐴 ) |
7 |
|
eqid |
⊢ ( 𝑓 ∈ ( 𝐴 ↑m 𝐴 ) , 𝑔 ∈ ( 𝐴 ↑m 𝐴 ) ↦ ( 𝑓 ∘ 𝑔 ) ) = ( 𝑓 ∈ ( 𝐴 ↑m 𝐴 ) , 𝑔 ∈ ( 𝐴 ↑m 𝐴 ) ↦ ( 𝑓 ∘ 𝑔 ) ) |
8 |
|
eqid |
⊢ ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) = ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) |
9 |
1 6 7 8
|
efmnd |
⊢ ( 𝐴 ∈ 𝑉 → 𝐺 = { 〈 ( Base ‘ ndx ) , ( 𝐴 ↑m 𝐴 ) 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝐴 ↑m 𝐴 ) , 𝑔 ∈ ( 𝐴 ↑m 𝐴 ) ↦ ( 𝑓 ∘ 𝑔 ) ) 〉 , 〈 ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) 〉 } ) |
10 |
9
|
fveq2d |
⊢ ( 𝐴 ∈ 𝑉 → ( TopSet ‘ 𝐺 ) = ( TopSet ‘ { 〈 ( Base ‘ ndx ) , ( 𝐴 ↑m 𝐴 ) 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝐴 ↑m 𝐴 ) , 𝑔 ∈ ( 𝐴 ↑m 𝐴 ) ↦ ( 𝑓 ∘ 𝑔 ) ) 〉 , 〈 ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) 〉 } ) ) |
11 |
5 10
|
eqtr4id |
⊢ ( 𝐴 ∈ 𝑉 → ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) = ( TopSet ‘ 𝐺 ) ) |