Step |
Hyp |
Ref |
Expression |
1 |
|
efmndbas.g |
⊢ 𝐺 = ( EndoFMnd ‘ 𝐴 ) |
2 |
|
efmndbas.b |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
3 |
|
ovex |
⊢ ( 𝐴 ↑m 𝐴 ) ∈ V |
4 |
|
eqid |
⊢ { 〈 ( Base ‘ ndx ) , ( 𝐴 ↑m 𝐴 ) 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝐴 ↑m 𝐴 ) , 𝑔 ∈ ( 𝐴 ↑m 𝐴 ) ↦ ( 𝑓 ∘ 𝑔 ) ) 〉 , 〈 ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) 〉 } = { 〈 ( Base ‘ ndx ) , ( 𝐴 ↑m 𝐴 ) 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝐴 ↑m 𝐴 ) , 𝑔 ∈ ( 𝐴 ↑m 𝐴 ) ↦ ( 𝑓 ∘ 𝑔 ) ) 〉 , 〈 ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) 〉 } |
5 |
4
|
topgrpbas |
⊢ ( ( 𝐴 ↑m 𝐴 ) ∈ V → ( 𝐴 ↑m 𝐴 ) = ( Base ‘ { 〈 ( Base ‘ ndx ) , ( 𝐴 ↑m 𝐴 ) 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝐴 ↑m 𝐴 ) , 𝑔 ∈ ( 𝐴 ↑m 𝐴 ) ↦ ( 𝑓 ∘ 𝑔 ) ) 〉 , 〈 ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) 〉 } ) ) |
6 |
3 5
|
mp1i |
⊢ ( 𝐴 ∈ V → ( 𝐴 ↑m 𝐴 ) = ( Base ‘ { 〈 ( Base ‘ ndx ) , ( 𝐴 ↑m 𝐴 ) 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝐴 ↑m 𝐴 ) , 𝑔 ∈ ( 𝐴 ↑m 𝐴 ) ↦ ( 𝑓 ∘ 𝑔 ) ) 〉 , 〈 ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) 〉 } ) ) |
7 |
|
eqid |
⊢ ( 𝐴 ↑m 𝐴 ) = ( 𝐴 ↑m 𝐴 ) |
8 |
|
eqid |
⊢ ( 𝑓 ∈ ( 𝐴 ↑m 𝐴 ) , 𝑔 ∈ ( 𝐴 ↑m 𝐴 ) ↦ ( 𝑓 ∘ 𝑔 ) ) = ( 𝑓 ∈ ( 𝐴 ↑m 𝐴 ) , 𝑔 ∈ ( 𝐴 ↑m 𝐴 ) ↦ ( 𝑓 ∘ 𝑔 ) ) |
9 |
|
eqid |
⊢ ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) = ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) |
10 |
1 7 8 9
|
efmnd |
⊢ ( 𝐴 ∈ V → 𝐺 = { 〈 ( Base ‘ ndx ) , ( 𝐴 ↑m 𝐴 ) 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝐴 ↑m 𝐴 ) , 𝑔 ∈ ( 𝐴 ↑m 𝐴 ) ↦ ( 𝑓 ∘ 𝑔 ) ) 〉 , 〈 ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) 〉 } ) |
11 |
10
|
fveq2d |
⊢ ( 𝐴 ∈ V → ( Base ‘ 𝐺 ) = ( Base ‘ { 〈 ( Base ‘ ndx ) , ( 𝐴 ↑m 𝐴 ) 〉 , 〈 ( +g ‘ ndx ) , ( 𝑓 ∈ ( 𝐴 ↑m 𝐴 ) , 𝑔 ∈ ( 𝐴 ↑m 𝐴 ) ↦ ( 𝑓 ∘ 𝑔 ) ) 〉 , 〈 ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) 〉 } ) ) |
12 |
6 11
|
eqtr4d |
⊢ ( 𝐴 ∈ V → ( 𝐴 ↑m 𝐴 ) = ( Base ‘ 𝐺 ) ) |
13 |
|
base0 |
⊢ ∅ = ( Base ‘ ∅ ) |
14 |
|
reldmmap |
⊢ Rel dom ↑m |
15 |
14
|
ovprc1 |
⊢ ( ¬ 𝐴 ∈ V → ( 𝐴 ↑m 𝐴 ) = ∅ ) |
16 |
|
fvprc |
⊢ ( ¬ 𝐴 ∈ V → ( EndoFMnd ‘ 𝐴 ) = ∅ ) |
17 |
1 16
|
eqtrid |
⊢ ( ¬ 𝐴 ∈ V → 𝐺 = ∅ ) |
18 |
17
|
fveq2d |
⊢ ( ¬ 𝐴 ∈ V → ( Base ‘ 𝐺 ) = ( Base ‘ ∅ ) ) |
19 |
13 15 18
|
3eqtr4a |
⊢ ( ¬ 𝐴 ∈ V → ( 𝐴 ↑m 𝐴 ) = ( Base ‘ 𝐺 ) ) |
20 |
12 19
|
pm2.61i |
⊢ ( 𝐴 ↑m 𝐴 ) = ( Base ‘ 𝐺 ) |
21 |
2 20
|
eqtr4i |
⊢ 𝐵 = ( 𝐴 ↑m 𝐴 ) |