Step | Hyp | Ref
| Expression |
1 | | symgval.1 |
. 2
⊢ 𝐺 = (SymGrp‘𝐴) |
2 | | df-symg 18498 |
. . . . 5
⊢ SymGrp =
(𝑥 ∈ V ↦
((EndoFMnd‘𝑥)
↾s {ℎ
∣ ℎ:𝑥–1-1-onto→𝑥})) |
3 | 2 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ V → SymGrp = (𝑥 ∈ V ↦
((EndoFMnd‘𝑥)
↾s {ℎ
∣ ℎ:𝑥–1-1-onto→𝑥}))) |
4 | | fveq2 6672 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (EndoFMnd‘𝑥) = (EndoFMnd‘𝐴)) |
5 | | eqidd 2824 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → ℎ = ℎ) |
6 | | id 22 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴) |
7 | 5, 6, 6 | f1oeq123d 6612 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → (ℎ:𝑥–1-1-onto→𝑥 ↔ ℎ:𝐴–1-1-onto→𝐴)) |
8 | 7 | abbidv 2887 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → {ℎ ∣ ℎ:𝑥–1-1-onto→𝑥} = {ℎ ∣ ℎ:𝐴–1-1-onto→𝐴}) |
9 | | f1oeq1 6606 |
. . . . . . . . 9
⊢ (ℎ = 𝑥 → (ℎ:𝐴–1-1-onto→𝐴 ↔ 𝑥:𝐴–1-1-onto→𝐴)) |
10 | 9 | cbvabv 2891 |
. . . . . . . 8
⊢ {ℎ ∣ ℎ:𝐴–1-1-onto→𝐴} = {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} |
11 | 8, 10 | syl6eq 2874 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → {ℎ ∣ ℎ:𝑥–1-1-onto→𝑥} = {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴}) |
12 | | symgval.2 |
. . . . . . 7
⊢ 𝐵 = {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} |
13 | 11, 12 | syl6eqr 2876 |
. . . . . 6
⊢ (𝑥 = 𝐴 → {ℎ ∣ ℎ:𝑥–1-1-onto→𝑥} = 𝐵) |
14 | 4, 13 | oveq12d 7176 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((EndoFMnd‘𝑥) ↾s {ℎ ∣ ℎ:𝑥–1-1-onto→𝑥}) = ((EndoFMnd‘𝐴) ↾s 𝐵)) |
15 | 14 | adantl 484 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝑥 = 𝐴) → ((EndoFMnd‘𝑥) ↾s {ℎ ∣ ℎ:𝑥–1-1-onto→𝑥}) = ((EndoFMnd‘𝐴) ↾s 𝐵)) |
16 | | id 22 |
. . . 4
⊢ (𝐴 ∈ V → 𝐴 ∈ V) |
17 | | ovexd 7193 |
. . . 4
⊢ (𝐴 ∈ V →
((EndoFMnd‘𝐴)
↾s 𝐵)
∈ V) |
18 | | nfv 1915 |
. . . 4
⊢
Ⅎ𝑥 𝐴 ∈ V |
19 | | nfcv 2979 |
. . . 4
⊢
Ⅎ𝑥𝐴 |
20 | | nfcv 2979 |
. . . . 5
⊢
Ⅎ𝑥(EndoFMnd‘𝐴) |
21 | | nfcv 2979 |
. . . . 5
⊢
Ⅎ𝑥
↾s |
22 | | nfab1 2981 |
. . . . . 6
⊢
Ⅎ𝑥{𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} |
23 | 12, 22 | nfcxfr 2977 |
. . . . 5
⊢
Ⅎ𝑥𝐵 |
24 | 20, 21, 23 | nfov 7188 |
. . . 4
⊢
Ⅎ𝑥((EndoFMnd‘𝐴) ↾s 𝐵) |
25 | 3, 15, 16, 17, 18, 19, 24 | fvmptdf 6776 |
. . 3
⊢ (𝐴 ∈ V →
(SymGrp‘𝐴) =
((EndoFMnd‘𝐴)
↾s 𝐵)) |
26 | | ress0 16560 |
. . . . 5
⊢ (∅
↾s 𝐵) =
∅ |
27 | 26 | a1i 11 |
. . . 4
⊢ (¬
𝐴 ∈ V → (∅
↾s 𝐵) =
∅) |
28 | | fvprc 6665 |
. . . . 5
⊢ (¬
𝐴 ∈ V →
(EndoFMnd‘𝐴) =
∅) |
29 | 28 | oveq1d 7173 |
. . . 4
⊢ (¬
𝐴 ∈ V →
((EndoFMnd‘𝐴)
↾s 𝐵) =
(∅ ↾s 𝐵)) |
30 | | fvprc 6665 |
. . . 4
⊢ (¬
𝐴 ∈ V →
(SymGrp‘𝐴) =
∅) |
31 | 27, 29, 30 | 3eqtr4rd 2869 |
. . 3
⊢ (¬
𝐴 ∈ V →
(SymGrp‘𝐴) =
((EndoFMnd‘𝐴)
↾s 𝐵)) |
32 | 25, 31 | pm2.61i 184 |
. 2
⊢
(SymGrp‘𝐴) =
((EndoFMnd‘𝐴)
↾s 𝐵) |
33 | 1, 32 | eqtri 2846 |
1
⊢ 𝐺 = ((EndoFMnd‘𝐴) ↾s 𝐵) |