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

Metamath Proof Explorer

Definition df-fxp

Description: Define the set of fixed points left unchanged by a group action. (Contributed by Thierry Arnoux, 18-Nov-2025)

Ref Expression
Assertion df-fxp Could not format assertion : 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 |-

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfxp Could not format FixPts : No typesetting found for class FixPts with typecode class
1 vb setvar b
2 cvv class V
3 va setvar a
4 vx setvar x
5 1 cv setvar b
6 vp setvar p
7 3 cv setvar a
8 7 cdm class dom ⁡ a
9 8 cdm class dom ⁡ dom ⁡ a
10 6 cv setvar p
11 4 cv setvar x
12 10 11 7 co class p a x
13 12 11 wceq wff p a x = x
14 13 6 9 wral wff ∀ p ∈ dom ⁡ dom ⁡ a p a x = x
15 14 4 5 crab class x ∈ b | ∀ p ∈ dom ⁡ dom ⁡ a p a x = x
16 1 3 2 2 15 cmpo class b ∈ V , a ∈ V ⟼ x ∈ b | ∀ p ∈ dom ⁡ dom ⁡ a p a x = x
17 0 16 wceq 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 wff FixPts = ( b e. _V , a e. _V |-> { x e. b | A. p e. dom dom a ( p a x ) = x } ) with typecode wff