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	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
	fxpval.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑊 )
Assertion	fxpss	⊢ ( 𝜑 → ( 𝐵 FixPts 𝐴 ) ⊆ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fxpval.1	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
2		fxpval.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑊 )
3	1 2	fxpval	⊢ ( 𝜑 → ( 𝐵 FixPts 𝐴 ) = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑝 ∈ dom dom 𝐴 ( 𝑝 𝐴 𝑥 ) = 𝑥 } )
4		ssrab2	⊢ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑝 ∈ dom dom 𝐴 ( 𝑝 𝐴 𝑥 ) = 𝑥 } ⊆ 𝐵
5	3 4	eqsstrdi	⊢ ( 𝜑 → ( 𝐵 FixPts 𝐴 ) ⊆ 𝐵 )