Definition df-fxp

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

	Ref	Expression
Assertion	df-fxp	|- FixPts = ( b e. _V , a e. _V |-> { x e. b | A. p e. dom dom a ( p a x ) = x } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfxp	|- FixPts
1		vb	|- b
2		cvv	|- _V
3		va	|- a
4		vx	|- x
5	1	cv	|- b
6		vp	|- p
7	3	cv	|- a
8	7	cdm	|- dom a
9	8	cdm	|- dom dom a
10	6	cv	|- p
11	4	cv	|- x
12	10 11 7	co	|- ( p a x )
13	12 11	wceq	|- ( p a x ) = x
14	13 6 9	wral	|- A. p e. dom dom a ( p a x ) = x
15	14 4 5	crab	|- { x e. b | A. p e. dom dom a ( p a x ) = x }
16	1 3 2 2 15	cmpo	|- ( b e. _V , a e. _V |-> { x e. b | A. p e. dom dom a ( p a x ) = x } )
17	0 16	wceq	|- FixPts = ( b e. _V , a e. _V |-> { x e. b | A. p e. dom dom a ( p a x ) = x } )