Theorem isfxp

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

	Ref	Expression
Hypotheses	fxpgaval.s	$$⊢U={\mathrm{Base}}_G$$
	fxpgaval.a	$$⊢\phi \to A\in \left(G\mathrm{GrpAct}C\right)$$
	isfxp.x	$$⊢\phi \to X\in C$$
Assertion	isfxp	Could not format assertion : No typesetting found for |- ( ph -> ( X e. ( C FixPts A ) <-> A. p e. U ( p A X ) = X ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		fxpgaval.s	$$⊢U={\mathrm{Base}}_G$$
2		fxpgaval.a	$$⊢\phi \to A\in \left(G\mathrm{GrpAct}C\right)$$
3		isfxp.x	$$⊢\phi \to X\in C$$
4	1 2	fxpgaval	Could not format ( ph -> ( C FixPts A ) = { x e. C | A. p e. U ( p A x ) = x } ) : No typesetting found for |- ( ph -> ( C FixPts A ) = { x e. C | A. p e. U ( p A x ) = x } ) with typecode |-
5	4	eleq2d	Could not format ( ph -> ( X e. ( C FixPts A ) <-> X e. { x e. C | A. p e. U ( p A x ) = x } ) ) : No typesetting found for |- ( ph -> ( X e. ( C FixPts A ) <-> X e. { x e. C | A. p e. U ( p A x ) = x } ) ) with typecode |-
6		oveq2	$$⊢x=X\to pAx=pAX$$
7		id	$$⊢x=X\to x=X$$
8	6 7	eqeq12d	$$⊢x=X\to \left(pAx=x\leftrightarrow pAX=X\right)$$
9	8	ralbidv	$$⊢x=X\to \left(\forall p\in UpAx=x\leftrightarrow \forall p\in UpAX=X\right)$$
10	9	elrab	$$⊢X\in \left\{x\in C|\forall p\in UpAx=x\right\}\leftrightarrow \left(X\in C\wedge \forall p\in UpAX=X\right)$$
11	5 10	bitrdi	Could not format ( ph -> ( X e. ( C FixPts A ) <-> ( X e. C /\ A. p e. U ( p A X ) = X ) ) ) : No typesetting found for |- ( ph -> ( X e. ( C FixPts A ) <-> ( X e. C /\ A. p e. U ( p A X ) = X ) ) ) with typecode |-
12	3 11	mpbirand	Could not format ( ph -> ( X e. ( C FixPts A ) <-> A. p e. U ( p A X ) = X ) ) : No typesetting found for |- ( ph -> ( X e. ( C FixPts A ) <-> A. p e. U ( p A X ) = X ) ) with typecode |-