Theorem isfxp

Description: Property of being a fixed point. (Contributed by Thierry Arnoux, 18-Nov-2025)

	Ref	Expression
Hypotheses	fxpgaval.s	|- U = ( Base ` G )
	fxpgaval.a	|- ( ph -> A e. ( G GrpAct C ) )
	isfxp.x	|- ( ph -> X e. C )
Assertion	isfxp	|- ( ph -> ( X e. ( C FixPts A ) <-> A. p e. U ( p A X ) = X ) )

Proof

Step	Hyp	Ref	Expression
1		fxpgaval.s	|- U = ( Base ` G )
2		fxpgaval.a	|- ( ph -> A e. ( G GrpAct C ) )
3		isfxp.x	|- ( ph -> X e. C )
4	1 2	fxpgaval	|- ( ph -> ( C FixPts A ) = { x e. C | A. p e. U ( p A x ) = x } )
5	4	eleq2d	|- ( ph -> ( X e. ( C FixPts A ) <-> X e. { x e. C | A. p e. U ( p A x ) = x } ) )
6		oveq2	|- ( x = X -> ( p A x ) = ( p A X ) )
7		id	|- ( x = X -> x = X )
8	6 7	eqeq12d	|- ( x = X -> ( ( p A x ) = x <-> ( p A X ) = X ) )
9	8	ralbidv	|- ( x = X -> ( A. p e. U ( p A x ) = x <-> A. p e. U ( p A X ) = X ) )
10	9	elrab	|- ( X e. { x e. C | A. p e. U ( p A x ) = x } <-> ( X e. C /\ A. p e. U ( p A X ) = X ) )
11	5 10	bitrdi	|- ( ph -> ( X e. ( C FixPts A ) <-> ( X e. C /\ A. p e. U ( p A X ) = X ) ) )
12	3 11	mpbirand	|- ( ph -> ( X e. ( C FixPts A ) <-> A. p e. U ( p A X ) = X ) )