Step |
Hyp |
Ref |
Expression |
1 |
|
symggrp.1 |
⊢ 𝐺 = ( SymGrp ‘ 𝐴 ) |
2 |
|
eqid |
⊢ ( EndoFMnd ‘ 𝐴 ) = ( EndoFMnd ‘ 𝐴 ) |
3 |
2
|
efmndtset |
⊢ ( 𝐴 ∈ 𝑉 → ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) = ( TopSet ‘ ( EndoFMnd ‘ 𝐴 ) ) ) |
4 |
|
eqid |
⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) |
5 |
1 4
|
symgbas |
⊢ ( Base ‘ 𝐺 ) = { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } |
6 |
|
fvexd |
⊢ ( 𝐴 ∈ 𝑉 → ( Base ‘ 𝐺 ) ∈ V ) |
7 |
5 6
|
eqeltrrid |
⊢ ( 𝐴 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } ∈ V ) |
8 |
|
eqid |
⊢ ( ( EndoFMnd ‘ 𝐴 ) ↾s { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } ) = ( ( EndoFMnd ‘ 𝐴 ) ↾s { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } ) |
9 |
|
eqid |
⊢ ( TopSet ‘ ( EndoFMnd ‘ 𝐴 ) ) = ( TopSet ‘ ( EndoFMnd ‘ 𝐴 ) ) |
10 |
8 9
|
resstset |
⊢ ( { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } ∈ V → ( TopSet ‘ ( EndoFMnd ‘ 𝐴 ) ) = ( TopSet ‘ ( ( EndoFMnd ‘ 𝐴 ) ↾s { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } ) ) ) |
11 |
7 10
|
syl |
⊢ ( 𝐴 ∈ 𝑉 → ( TopSet ‘ ( EndoFMnd ‘ 𝐴 ) ) = ( TopSet ‘ ( ( EndoFMnd ‘ 𝐴 ) ↾s { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } ) ) ) |
12 |
|
eqid |
⊢ { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } = { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } |
13 |
1 12
|
symgval |
⊢ 𝐺 = ( ( EndoFMnd ‘ 𝐴 ) ↾s { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } ) |
14 |
13
|
eqcomi |
⊢ ( ( EndoFMnd ‘ 𝐴 ) ↾s { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } ) = 𝐺 |
15 |
14
|
fveq2i |
⊢ ( TopSet ‘ ( ( EndoFMnd ‘ 𝐴 ) ↾s { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } ) ) = ( TopSet ‘ 𝐺 ) |
16 |
15
|
a1i |
⊢ ( 𝐴 ∈ 𝑉 → ( TopSet ‘ ( ( EndoFMnd ‘ 𝐴 ) ↾s { 𝑓 ∣ 𝑓 : 𝐴 –1-1-onto→ 𝐴 } ) ) = ( TopSet ‘ 𝐺 ) ) |
17 |
3 11 16
|
3eqtrd |
⊢ ( 𝐴 ∈ 𝑉 → ( ∏t ‘ ( 𝐴 × { 𝒫 𝐴 } ) ) = ( TopSet ‘ 𝐺 ) ) |