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	|- ( ph -> B e. V )
	fxpval.2	|- ( ph -> A e. W )
Assertion	fxpss	|- ( ph -> ( B FixPts A ) C_ B )

Proof

Step	Hyp	Ref	Expression
1		fxpval.1	|- ( ph -> B e. V )
2		fxpval.2	|- ( ph -> A e. W )
3	1 2	fxpval	|- ( ph -> ( B FixPts A ) = { x e. B | A. p e. dom dom A ( p A x ) = x } )
4		ssrab2	|- { x e. B | A. p e. dom dom A ( p A x ) = x } C_ B
5	3 4	eqsstrdi	|- ( ph -> ( B FixPts A ) C_ B )