Theorem fxpval

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

	Ref	Expression
Hypotheses	fxpval.1	$$⊢\phi \to B\in V$$
	fxpval.2	$$⊢\phi \to A\in W$$
Assertion	fxpval	Could not format assertion : No typesetting found for |- ( ph -> ( B FixPts A ) = { x e. B | A. p e. dom dom A ( p A x ) = x } ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		fxpval.1	$$⊢\phi \to B\in V$$
2		fxpval.2	$$⊢\phi \to A\in W$$
3		df-fxp	Could not format FixPts = ( b e. _V , a e. _V |-> { x e. b | A. p e. dom dom a ( p a x ) = x } ) : No typesetting found for |- FixPts = ( b e. _V , a e. _V |-> { x e. b | A. p e. dom dom a ( p a x ) = x } ) with typecode |-
4	3	a1i	Could not format ( ph -> FixPts = ( b e. _V , a e. _V |-> { x e. b | A. p e. dom dom a ( p a x ) = x } ) ) : No typesetting found for |- ( ph -> FixPts = ( b e. _V , a e. _V |-> { x e. b | A. p e. dom dom a ( p a x ) = x } ) ) with typecode |-
5		simpl	$$⊢\left(b=B\wedge a=A\right)\to b=B$$
6		dmeq	$$⊢a=A\to \mathrm{dom}a=\mathrm{dom}A$$
7	6	dmeqd	$$⊢a=A\to \mathrm{dom}\mathrm{dom}a=\mathrm{dom}\mathrm{dom}A$$
8		oveq	$$⊢a=A\to pax=pAx$$
9	8	eqeq1d	$$⊢a=A\to \left(pax=x\leftrightarrow pAx=x\right)$$
10	7 9	raleqbidv	$$⊢a=A\to \left(\forall p\in \mathrm{dom}\mathrm{dom}apax=x\leftrightarrow \forall p\in \mathrm{dom}\mathrm{dom}ApAx=x\right)$$
11	10	adantl	$$⊢\left(b=B\wedge a=A\right)\to \left(\forall p\in \mathrm{dom}\mathrm{dom}apax=x\leftrightarrow \forall p\in \mathrm{dom}\mathrm{dom}ApAx=x\right)$$
12	5 11	rabeqbidv	$$⊢\left(b=B\wedge a=A\right)\to \left\{x\in b|\forall p\in \mathrm{dom}\mathrm{dom}apax=x\right\}=\left\{x\in B|\forall p\in \mathrm{dom}\mathrm{dom}ApAx=x\right\}$$
13	12	adantl	$$⊢\left(\phi \wedge \left(b=B\wedge a=A\right)\right)\to \left\{x\in b|\forall p\in \mathrm{dom}\mathrm{dom}apax=x\right\}=\left\{x\in B|\forall p\in \mathrm{dom}\mathrm{dom}ApAx=x\right\}$$
14	1	elexd	$$⊢\phi \to B\in \mathrm{V}$$
15	2	elexd	$$⊢\phi \to A\in \mathrm{V}$$
16		eqid	$$⊢\left\{x\in B|\forall p\in \mathrm{dom}\mathrm{dom}ApAx=x\right\}=\left\{x\in B|\forall p\in \mathrm{dom}\mathrm{dom}ApAx=x\right\}$$
17	16 1	rabexd	$$⊢\phi \to \left\{x\in B|\forall p\in \mathrm{dom}\mathrm{dom}ApAx=x\right\}\in \mathrm{V}$$
18	4 13 14 15 17	ovmpod	Could not format ( ph -> ( B FixPts A ) = { x e. B | A. p e. dom dom A ( p A x ) = x } ) : No typesetting found for |- ( ph -> ( B FixPts A ) = { x e. B | A. p e. dom dom A ( p A x ) = x } ) with typecode |-