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	$⊢ φ \to A \in (G GrpAct C)$
	isfxp.x	$⊢ φ \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 \|-

Step	Hyp	Ref	Expression
1		fxpgaval.s	$⊢ U = {Base}_{G}$
2		fxpgaval.a	$⊢ φ \to A \in (G GrpAct C)$
3		isfxp.x	$⊢ φ \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 p A x = p A X$
7		id	$⊢ x = X \to x = X$
8	6 7	eqeq12d	$⊢ x = X \to (p A x = x \leftrightarrow p A X = X)$
9	8	ralbidv	$⊢ x = X \to (\forall p \in U p A x = x \leftrightarrow \forall p \in U p A X = X)$
10	9	elrab	$⊢ X \in \{x \in C \| \forall p \in U p A x = x\} \leftrightarrow (X \in C \land \forall p \in U p A X = X)$
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 \|-

Metamath Proof Explorer