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

Metamath Proof Explorer

Theorem fxpval

Description: Value of the set of fixed points. (Contributed by Thierry Arnoux, 18-Nov-2025)

Ref Expression
Hypotheses fxpval.1 
|- ( ph -> B e. V )
fxpval.2 
|- ( ph -> A e. W )
Assertion fxpval 
|- ( ph -> ( B FixPts A ) = { x e. B | A. p e. dom dom A ( p A x ) = x } )

Proof

Step Hyp Ref Expression
1 fxpval.1 
 |-  ( ph -> B e. V )
2 fxpval.2 
 |-  ( ph -> A e. W )
3 df-fxp 
 |-  FixPts = ( b e. _V , a e. _V |-> { x e. b | A. p e. dom dom a ( p a x ) = x } )
4 3 a1i 
 |-  ( ph -> FixPts = ( b e. _V , a e. _V |-> { x e. b | A. p e. dom dom a ( p a x ) = x } ) )
5 simpl 
 |-  ( ( b = B /\ a = A ) -> b = B )
6 dmeq 
 |-  ( a = A -> dom a = dom A )
7 6 dmeqd 
 |-  ( a = A -> dom dom a = dom dom A )
8 oveq 
 |-  ( a = A -> ( p a x ) = ( p A x ) )
9 8 eqeq1d 
 |-  ( a = A -> ( ( p a x ) = x <-> ( p A x ) = x ) )
10 7 9 raleqbidv 
 |-  ( a = A -> ( A. p e. dom dom a ( p a x ) = x <-> A. p e. dom dom A ( p A x ) = x ) )
11 10 adantl 
 |-  ( ( b = B /\ a = A ) -> ( A. p e. dom dom a ( p a x ) = x <-> A. p e. dom dom A ( p A x ) = x ) )
12 5 11 rabeqbidv 
 |-  ( ( b = B /\ a = A ) -> { x e. b | A. p e. dom dom a ( p a x ) = x } = { x e. B | A. p e. dom dom A ( p A x ) = x } )
13 12 adantl 
 |-  ( ( ph /\ ( b = B /\ a = A ) ) -> { x e. b | A. p e. dom dom a ( p a x ) = x } = { x e. B | A. p e. dom dom A ( p A x ) = x } )
14 1 elexd 
 |-  ( ph -> B e. _V )
15 2 elexd 
 |-  ( ph -> A e. _V )
16 eqid 
 |-  { x e. B | A. p e. dom dom A ( p A x ) = x } = { x e. B | A. p e. dom dom A ( p A x ) = x }
17 16 1 rabexd 
 |-  ( ph -> { x e. B | A. p e. dom dom A ( p A x ) = x } e. _V )
18 4 13 14 15 17 ovmpod 
 |-  ( ph -> ( B FixPts A ) = { x e. B | A. p e. dom dom A ( p A x ) = x } )