Step |
Hyp |
Ref |
Expression |
1 |
|
symgval.1 |
⊢ 𝐺 = ( SymGrp ‘ 𝐴 ) |
2 |
|
symgval.2 |
⊢ 𝐵 = { 𝑥 ∣ 𝑥 : 𝐴 –1-1-onto→ 𝐴 } |
3 |
|
df-symg |
⊢ SymGrp = ( 𝑥 ∈ V ↦ ( ( EndoFMnd ‘ 𝑥 ) ↾s { ℎ ∣ ℎ : 𝑥 –1-1-onto→ 𝑥 } ) ) |
4 |
3
|
a1i |
⊢ ( 𝐴 ∈ V → SymGrp = ( 𝑥 ∈ V ↦ ( ( EndoFMnd ‘ 𝑥 ) ↾s { ℎ ∣ ℎ : 𝑥 –1-1-onto→ 𝑥 } ) ) ) |
5 |
|
fveq2 |
⊢ ( 𝑥 = 𝐴 → ( EndoFMnd ‘ 𝑥 ) = ( EndoFMnd ‘ 𝐴 ) ) |
6 |
|
eqidd |
⊢ ( 𝑥 = 𝐴 → ℎ = ℎ ) |
7 |
|
id |
⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 ) |
8 |
6 7 7
|
f1oeq123d |
⊢ ( 𝑥 = 𝐴 → ( ℎ : 𝑥 –1-1-onto→ 𝑥 ↔ ℎ : 𝐴 –1-1-onto→ 𝐴 ) ) |
9 |
8
|
abbidv |
⊢ ( 𝑥 = 𝐴 → { ℎ ∣ ℎ : 𝑥 –1-1-onto→ 𝑥 } = { ℎ ∣ ℎ : 𝐴 –1-1-onto→ 𝐴 } ) |
10 |
|
f1oeq1 |
⊢ ( ℎ = 𝑥 → ( ℎ : 𝐴 –1-1-onto→ 𝐴 ↔ 𝑥 : 𝐴 –1-1-onto→ 𝐴 ) ) |
11 |
10
|
cbvabv |
⊢ { ℎ ∣ ℎ : 𝐴 –1-1-onto→ 𝐴 } = { 𝑥 ∣ 𝑥 : 𝐴 –1-1-onto→ 𝐴 } |
12 |
9 11
|
eqtrdi |
⊢ ( 𝑥 = 𝐴 → { ℎ ∣ ℎ : 𝑥 –1-1-onto→ 𝑥 } = { 𝑥 ∣ 𝑥 : 𝐴 –1-1-onto→ 𝐴 } ) |
13 |
12 2
|
eqtr4di |
⊢ ( 𝑥 = 𝐴 → { ℎ ∣ ℎ : 𝑥 –1-1-onto→ 𝑥 } = 𝐵 ) |
14 |
5 13
|
oveq12d |
⊢ ( 𝑥 = 𝐴 → ( ( EndoFMnd ‘ 𝑥 ) ↾s { ℎ ∣ ℎ : 𝑥 –1-1-onto→ 𝑥 } ) = ( ( EndoFMnd ‘ 𝐴 ) ↾s 𝐵 ) ) |
15 |
14
|
adantl |
⊢ ( ( 𝐴 ∈ V ∧ 𝑥 = 𝐴 ) → ( ( EndoFMnd ‘ 𝑥 ) ↾s { ℎ ∣ ℎ : 𝑥 –1-1-onto→ 𝑥 } ) = ( ( EndoFMnd ‘ 𝐴 ) ↾s 𝐵 ) ) |
16 |
|
id |
⊢ ( 𝐴 ∈ V → 𝐴 ∈ V ) |
17 |
|
ovexd |
⊢ ( 𝐴 ∈ V → ( ( EndoFMnd ‘ 𝐴 ) ↾s 𝐵 ) ∈ V ) |
18 |
|
nfv |
⊢ Ⅎ 𝑥 𝐴 ∈ V |
19 |
|
nfcv |
⊢ Ⅎ 𝑥 𝐴 |
20 |
|
nfcv |
⊢ Ⅎ 𝑥 ( EndoFMnd ‘ 𝐴 ) |
21 |
|
nfcv |
⊢ Ⅎ 𝑥 ↾s |
22 |
|
nfab1 |
⊢ Ⅎ 𝑥 { 𝑥 ∣ 𝑥 : 𝐴 –1-1-onto→ 𝐴 } |
23 |
2 22
|
nfcxfr |
⊢ Ⅎ 𝑥 𝐵 |
24 |
20 21 23
|
nfov |
⊢ Ⅎ 𝑥 ( ( EndoFMnd ‘ 𝐴 ) ↾s 𝐵 ) |
25 |
4 15 16 17 18 19 24
|
fvmptdf |
⊢ ( 𝐴 ∈ V → ( SymGrp ‘ 𝐴 ) = ( ( EndoFMnd ‘ 𝐴 ) ↾s 𝐵 ) ) |
26 |
|
ress0 |
⊢ ( ∅ ↾s 𝐵 ) = ∅ |
27 |
26
|
a1i |
⊢ ( ¬ 𝐴 ∈ V → ( ∅ ↾s 𝐵 ) = ∅ ) |
28 |
|
fvprc |
⊢ ( ¬ 𝐴 ∈ V → ( EndoFMnd ‘ 𝐴 ) = ∅ ) |
29 |
28
|
oveq1d |
⊢ ( ¬ 𝐴 ∈ V → ( ( EndoFMnd ‘ 𝐴 ) ↾s 𝐵 ) = ( ∅ ↾s 𝐵 ) ) |
30 |
|
fvprc |
⊢ ( ¬ 𝐴 ∈ V → ( SymGrp ‘ 𝐴 ) = ∅ ) |
31 |
27 29 30
|
3eqtr4rd |
⊢ ( ¬ 𝐴 ∈ V → ( SymGrp ‘ 𝐴 ) = ( ( EndoFMnd ‘ 𝐴 ) ↾s 𝐵 ) ) |
32 |
25 31
|
pm2.61i |
⊢ ( SymGrp ‘ 𝐴 ) = ( ( EndoFMnd ‘ 𝐴 ) ↾s 𝐵 ) |
33 |
1 32
|
eqtri |
⊢ 𝐺 = ( ( EndoFMnd ‘ 𝐴 ) ↾s 𝐵 ) |