Definition df-fxp 33129

Description: Define the set of fixed points left unchanged by a group action. (Contributed by Thierry Arnoux, 18-Nov-2025.)

Assertion

Ref	Expression
df-fxp	⊢ FixPts = (𝑏 ∈ V, 𝑎 ∈ V ↦ {𝑥 ∈ 𝑏 ∣ ∀𝑝 ∈ dom dom 𝑎(𝑝𝑎𝑥) = 𝑥})

Distinct variable group:   𝑎,𝑏,𝑥,𝑝

Detailed syntax breakdown of Definition df-fxp

Step	Hyp	Ref	Expression
1		cfxp 33128	. 2 class FixPts
2		vb	. . 3 setvar 𝑏
3		va	. . 3 setvar 𝑎
4		cvv 3455	. . 3 class V
5		vp	. . . . . . . 8 setvar 𝑝
6	5	cv 1539	. . . . . . 7 class 𝑝
7		vx	. . . . . . . 8 setvar 𝑥
8	7	cv 1539	. . . . . . 7 class 𝑥
9	3	cv 1539	. . . . . . 7 class 𝑎
10	6, 8, 9	co 7394	. . . . . 6 class (𝑝𝑎𝑥)
11	10, 8	wceq 1540	. . . . 5 wff (𝑝𝑎𝑥) = 𝑥
12	9	cdm 5646	. . . . . 6 class dom 𝑎
13	12	cdm 5646	. . . . 5 class dom dom 𝑎
14	11, 5, 13	wral 3046	. . . 4 wff ∀𝑝 ∈ dom dom 𝑎(𝑝𝑎𝑥) = 𝑥
15	2	cv 1539	. . . 4 class 𝑏
16	14, 7, 15	crab 3411	. . 3 class {𝑥 ∈ 𝑏 ∣ ∀𝑝 ∈ dom dom 𝑎(𝑝𝑎𝑥) = 𝑥}
17	2, 3, 4, 4, 16	cmpo 7396	. 2 class (𝑏 ∈ V, 𝑎 ∈ V ↦ {𝑥 ∈ 𝑏 ∣ ∀𝑝 ∈ dom dom 𝑎(𝑝𝑎𝑥) = 𝑥})
18	1, 17	wceq 1540	1 wff FixPts = (𝑏 ∈ V, 𝑎 ∈ V ↦ {𝑥 ∈ 𝑏 ∣ ∀𝑝 ∈ dom dom 𝑎(𝑝𝑎𝑥) = 𝑥})

This definition is referenced by:  fxpval  33130