Detailed syntax breakdown of Definition df-psgn
Step | Hyp | Ref
| Expression |
1 | | cpsgn 18697 |
. 2
class
pmSgn |
2 | | vd |
. . 3
setvar 𝑑 |
3 | | cvv 3409 |
. . 3
class
V |
4 | | vx |
. . . 4
setvar 𝑥 |
5 | | vp |
. . . . . . . . 9
setvar 𝑝 |
6 | 5 | cv 1537 |
. . . . . . . 8
class 𝑝 |
7 | | cid 5433 |
. . . . . . . 8
class
I |
8 | 6, 7 | cdif 3857 |
. . . . . . 7
class (𝑝 ∖ I ) |
9 | 8 | cdm 5528 |
. . . . . 6
class dom
(𝑝 ∖ I
) |
10 | | cfn 8540 |
. . . . . 6
class
Fin |
11 | 9, 10 | wcel 2111 |
. . . . 5
wff dom (𝑝 ∖ I ) ∈
Fin |
12 | 2 | cv 1537 |
. . . . . . 7
class 𝑑 |
13 | | csymg 18575 |
. . . . . . 7
class
SymGrp |
14 | 12, 13 | cfv 6340 |
. . . . . 6
class
(SymGrp‘𝑑) |
15 | | cbs 16554 |
. . . . . 6
class
Base |
16 | 14, 15 | cfv 6340 |
. . . . 5
class
(Base‘(SymGrp‘𝑑)) |
17 | 11, 5, 16 | crab 3074 |
. . . 4
class {𝑝 ∈
(Base‘(SymGrp‘𝑑)) ∣ dom (𝑝 ∖ I ) ∈ Fin} |
18 | 4 | cv 1537 |
. . . . . . . 8
class 𝑥 |
19 | | vw |
. . . . . . . . . 10
setvar 𝑤 |
20 | 19 | cv 1537 |
. . . . . . . . 9
class 𝑤 |
21 | | cgsu 16785 |
. . . . . . . . 9
class
Σg |
22 | 14, 20, 21 | co 7156 |
. . . . . . . 8
class
((SymGrp‘𝑑)
Σg 𝑤) |
23 | 18, 22 | wceq 1538 |
. . . . . . 7
wff 𝑥 = ((SymGrp‘𝑑) Σg
𝑤) |
24 | | vs |
. . . . . . . . 9
setvar 𝑠 |
25 | 24 | cv 1537 |
. . . . . . . 8
class 𝑠 |
26 | | c1 10589 |
. . . . . . . . . 10
class
1 |
27 | 26 | cneg 10922 |
. . . . . . . . 9
class
-1 |
28 | | chash 13753 |
. . . . . . . . . 10
class
♯ |
29 | 20, 28 | cfv 6340 |
. . . . . . . . 9
class
(♯‘𝑤) |
30 | | cexp 13492 |
. . . . . . . . 9
class
↑ |
31 | 27, 29, 30 | co 7156 |
. . . . . . . 8
class
(-1↑(♯‘𝑤)) |
32 | 25, 31 | wceq 1538 |
. . . . . . 7
wff 𝑠 = (-1↑(♯‘𝑤)) |
33 | 23, 32 | wa 399 |
. . . . . 6
wff (𝑥 = ((SymGrp‘𝑑) Σg
𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤))) |
34 | | cpmtr 18649 |
. . . . . . . . 9
class
pmTrsp |
35 | 12, 34 | cfv 6340 |
. . . . . . . 8
class
(pmTrsp‘𝑑) |
36 | 35 | crn 5529 |
. . . . . . 7
class ran
(pmTrsp‘𝑑) |
37 | 36 | cword 13926 |
. . . . . 6
class Word ran
(pmTrsp‘𝑑) |
38 | 33, 19, 37 | wrex 3071 |
. . . . 5
wff
∃𝑤 ∈ Word
ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg
𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤))) |
39 | 38, 24 | cio 6297 |
. . . 4
class
(℩𝑠∃𝑤 ∈ Word ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤)))) |
40 | 4, 17, 39 | cmpt 5116 |
. . 3
class (𝑥 ∈ {𝑝 ∈ (Base‘(SymGrp‘𝑑)) ∣ dom (𝑝 ∖ I ) ∈ Fin} ↦
(℩𝑠∃𝑤 ∈ Word ran
(pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg
𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤))))) |
41 | 2, 3, 40 | cmpt 5116 |
. 2
class (𝑑 ∈ V ↦ (𝑥 ∈ {𝑝 ∈ (Base‘(SymGrp‘𝑑)) ∣ dom (𝑝 ∖ I ) ∈ Fin} ↦
(℩𝑠∃𝑤 ∈ Word ran
(pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg
𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤)))))) |
42 | 1, 41 | wceq 1538 |
1
wff pmSgn =
(𝑑 ∈ V ↦ (𝑥 ∈ {𝑝 ∈ (Base‘(SymGrp‘𝑑)) ∣ dom (𝑝 ∖ I ) ∈ Fin} ↦
(℩𝑠∃𝑤 ∈ Word ran
(pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg
𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤)))))) |