Theorem fxpss

Description: The set of fixed points is a subset of the set acted upon. (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	fxpss	Could not format assertion : No typesetting found for |- ( ph -> ( B FixPts A ) C_ B ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		fxpval.1	$$⊢\phi \to B\in V$$
2		fxpval.2	$$⊢\phi \to A\in W$$
3	1 2	fxpval	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 |-
4		ssrab2	$$⊢\left\{x\in B|\forall p\in \mathrm{dom}\mathrm{dom}ApAx=x\right\}\subseteq B$$
5	3 4	eqsstrdi	Could not format ( ph -> ( B FixPts A ) C_ B ) : No typesetting found for |- ( ph -> ( B FixPts A ) C_ B ) with typecode |-