This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ φ → B ∈ V
fxpval.2 ⊢ φ → A ∈ 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 ⊢ φ → B ∈ V
2 fxpval.2 ⊢ φ → A ∈ 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 ⊢ x ∈ B | ∀ p ∈ dom ⁡ dom ⁡ A p A x = x ⊆ 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 |-