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	⊢ FixPts = ( 𝑏 ∈ V , 𝑎 ∈ V ↦ { 𝑥 ∈ 𝑏 ∣ ∀ 𝑝 ∈ dom dom 𝑎 ( 𝑝 𝑎 𝑥 ) = 𝑥 } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfxp	⊢ FixPts
1		vb	⊢ 𝑏
2		cvv	⊢ V
3		va	⊢ 𝑎
4		vx	⊢ 𝑥
5	1	cv	⊢ 𝑏
6		vp	⊢ 𝑝
7	3	cv	⊢ 𝑎
8	7	cdm	⊢ dom 𝑎
9	8	cdm	⊢ dom dom 𝑎
10	6	cv	⊢ 𝑝
11	4	cv	⊢ 𝑥
12	10 11 7	co	⊢ ( 𝑝 𝑎 𝑥 )
13	12 11	wceq	⊢ ( 𝑝 𝑎 𝑥 ) = 𝑥
14	13 6 9	wral	⊢ ∀ 𝑝 ∈ dom dom 𝑎 ( 𝑝 𝑎 𝑥 ) = 𝑥
15	14 4 5	crab	⊢ { 𝑥 ∈ 𝑏 ∣ ∀ 𝑝 ∈ dom dom 𝑎 ( 𝑝 𝑎 𝑥 ) = 𝑥 }
16	1 3 2 2 15	cmpo	⊢ ( 𝑏 ∈ V , 𝑎 ∈ V ↦ { 𝑥 ∈ 𝑏 ∣ ∀ 𝑝 ∈ dom dom 𝑎 ( 𝑝 𝑎 𝑥 ) = 𝑥 } )
17	0 16	wceq	⊢ FixPts = ( 𝑏 ∈ V , 𝑎 ∈ V ↦ { 𝑥 ∈ 𝑏 ∣ ∀ 𝑝 ∈ dom dom 𝑎 ( 𝑝 𝑎 𝑥 ) = 𝑥 } )