This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )