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