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	Could not format assertion : No typesetting found for |- FixPts = ( b e. _V , a e. _V |-> { x e. b | A. p e. dom dom a ( p a x ) = x } ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfxp	Could not format FixPts : No typesetting found for class FixPts with typecode class
1		vb	$$setvarb$$
2		cvv	$$class\mathrm{V}$$
3		va	$$setvara$$
4		vx	$$setvarx$$
5	1	cv	$$setvarb$$
6		vp	$$setvarp$$
7	3	cv	$$setvara$$
8	7	cdm	$$class\mathrm{dom}a$$
9	8	cdm	$$class\mathrm{dom}\mathrm{dom}a$$
10	6	cv	$$setvarp$$
11	4	cv	$$setvarx$$
12	10 11 7	co	$$class\left(pax\right)$$
13	12 11	wceq	$$wffpax=x$$
14	13 6 9	wral	$$wff\forall p\in \mathrm{dom}\mathrm{dom}apax=x$$
15	14 4 5	crab	$$class\left\{x\in b|\forall p\in \mathrm{dom}\mathrm{dom}apax=x\right\}$$
16	1 3 2 2 15	cmpo	$$class\left(b\in \mathrm{V},a\in \mathrm{V}⟼\left\{x\in b|\forall p\in \mathrm{dom}\mathrm{dom}apax=x\right\}\right)$$
17	0 16	wceq	Could not format FixPts = ( b e. _V , a e. _V |-> { x e. b | A. p e. dom dom a ( p a x ) = x } ) : No typesetting found for wff FixPts = ( b e. _V , a e. _V |-> { x e. b | A. p e. dom dom a ( p a x ) = x } ) with typecode wff