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

Metamath Proof Explorer

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 𝐴 ) ↔ ∀ 𝑝 ∈ 𝑈 ( 𝑝 𝐴 𝑋 ) = 𝑋 ) )