Theorem isfxp

Description: Property of being a fixed point. (Contributed by Thierry Arnoux, 18-Nov-2025)

	Ref	Expression
Hypotheses	fxpgaval.s	⊢ 𝑈 = ( Base ‘ 𝐺 )
	fxpgaval.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐺 GrpAct 𝐶 ) )
	isfxp.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐶 )
Assertion	isfxp	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐶 FixPts 𝐴 ) ↔ ∀ 𝑝 ∈ 𝑈 ( 𝑝 𝐴 𝑋 ) = 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		fxpgaval.s	⊢ 𝑈 = ( Base ‘ 𝐺 )
2		fxpgaval.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐺 GrpAct 𝐶 ) )
3		isfxp.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐶 )
4	1 2	fxpgaval	⊢ ( 𝜑 → ( 𝐶 FixPts 𝐴 ) = { 𝑥 ∈ 𝐶 ∣ ∀ 𝑝 ∈ 𝑈 ( 𝑝 𝐴 𝑥 ) = 𝑥 } )
5	4	eleq2d	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐶 FixPts 𝐴 ) ↔ 𝑋 ∈ { 𝑥 ∈ 𝐶 ∣ ∀ 𝑝 ∈ 𝑈 ( 𝑝 𝐴 𝑥 ) = 𝑥 } ) )
6		oveq2	⊢ ( 𝑥 = 𝑋 → ( 𝑝 𝐴 𝑥 ) = ( 𝑝 𝐴 𝑋 ) )
7		id	⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
8	6 7	eqeq12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑝 𝐴 𝑥 ) = 𝑥 ↔ ( 𝑝 𝐴 𝑋 ) = 𝑋 ) )
9	8	ralbidv	⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑝 ∈ 𝑈 ( 𝑝 𝐴 𝑥 ) = 𝑥 ↔ ∀ 𝑝 ∈ 𝑈 ( 𝑝 𝐴 𝑋 ) = 𝑋 ) )
10	9	elrab	⊢ ( 𝑋 ∈ { 𝑥 ∈ 𝐶 ∣ ∀ 𝑝 ∈ 𝑈 ( 𝑝 𝐴 𝑥 ) = 𝑥 } ↔ ( 𝑋 ∈ 𝐶 ∧ ∀ 𝑝 ∈ 𝑈 ( 𝑝 𝐴 𝑋 ) = 𝑋 ) )
11	5 10	bitrdi	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐶 FixPts 𝐴 ) ↔ ( 𝑋 ∈ 𝐶 ∧ ∀ 𝑝 ∈ 𝑈 ( 𝑝 𝐴 𝑋 ) = 𝑋 ) ) )
12	3 11	mpbirand	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐶 FixPts 𝐴 ) ↔ ∀ 𝑝 ∈ 𝑈 ( 𝑝 𝐴 𝑋 ) = 𝑋 ) )