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

Metamath Proof Explorer

Theorem fxpval

Description: Value of the set of fixed points. (Contributed by Thierry Arnoux, 18-Nov-2025)

Ref Expression
Hypotheses fxpval.1 ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
fxpval.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑊 )
Assertion fxpval ( 𝜑 → ( 𝐵 FixPts 𝐴 ) = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑝 ∈ dom dom 𝐴 ( 𝑝 𝐴 𝑥 ) = 𝑥 } )

Proof

Step Hyp Ref Expression
1 fxpval.1 ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
2 fxpval.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑊 )
3 df-fxp ⊢ FixPts = ( 𝑏 ∈ V , 𝑎 ∈ V ↦ { 𝑥 ∈ 𝑏 ∣ ∀ 𝑝 ∈ dom dom 𝑎 ( 𝑝 𝑎 𝑥 ) = 𝑥 } )
4 3 a1i ⊢ ( 𝜑 → FixPts = ( 𝑏 ∈ V , 𝑎 ∈ V ↦ { 𝑥 ∈ 𝑏 ∣ ∀ 𝑝 ∈ dom dom 𝑎 ( 𝑝 𝑎 𝑥 ) = 𝑥 } ) )
5 simpl ⊢ ( ( 𝑏 = 𝐵 ∧ 𝑎 = 𝐴 ) → 𝑏 = 𝐵 )
6 dmeq ⊢ ( 𝑎 = 𝐴 → dom 𝑎 = dom 𝐴 )
7 6 dmeqd ⊢ ( 𝑎 = 𝐴 → dom dom 𝑎 = dom dom 𝐴 )
8 oveq ⊢ ( 𝑎 = 𝐴 → ( 𝑝 𝑎 𝑥 ) = ( 𝑝 𝐴 𝑥 ) )
9 8 eqeq1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑝 𝑎 𝑥 ) = 𝑥 ↔ ( 𝑝 𝐴 𝑥 ) = 𝑥 ) )
10 7 9 raleqbidv ⊢ ( 𝑎 = 𝐴 → ( ∀ 𝑝 ∈ dom dom 𝑎 ( 𝑝 𝑎 𝑥 ) = 𝑥 ↔ ∀ 𝑝 ∈ dom dom 𝐴 ( 𝑝 𝐴 𝑥 ) = 𝑥 ) )
11 10 adantl ⊢ ( ( 𝑏 = 𝐵 ∧ 𝑎 = 𝐴 ) → ( ∀ 𝑝 ∈ dom dom 𝑎 ( 𝑝 𝑎 𝑥 ) = 𝑥 ↔ ∀ 𝑝 ∈ dom dom 𝐴 ( 𝑝 𝐴 𝑥 ) = 𝑥 ) )
12 5 11 rabeqbidv ⊢ ( ( 𝑏 = 𝐵 ∧ 𝑎 = 𝐴 ) → { 𝑥 ∈ 𝑏 ∣ ∀ 𝑝 ∈ dom dom 𝑎 ( 𝑝 𝑎 𝑥 ) = 𝑥 } = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑝 ∈ dom dom 𝐴 ( 𝑝 𝐴 𝑥 ) = 𝑥 } )
13 12 adantl ⊢ ( ( 𝜑 ∧ ( 𝑏 = 𝐵 ∧ 𝑎 = 𝐴 ) ) → { 𝑥 ∈ 𝑏 ∣ ∀ 𝑝 ∈ dom dom 𝑎 ( 𝑝 𝑎 𝑥 ) = 𝑥 } = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑝 ∈ dom dom 𝐴 ( 𝑝 𝐴 𝑥 ) = 𝑥 } )
14 1 elexd ⊢ ( 𝜑 → 𝐵 ∈ V )
15 2 elexd ⊢ ( 𝜑 → 𝐴 ∈ V )
16 eqid ⊢ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑝 ∈ dom dom 𝐴 ( 𝑝 𝐴 𝑥 ) = 𝑥 } = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑝 ∈ dom dom 𝐴 ( 𝑝 𝐴 𝑥 ) = 𝑥 }
17 16 1 rabexd ⊢ ( 𝜑 → { 𝑥 ∈ 𝐵 ∣ ∀ 𝑝 ∈ dom dom 𝐴 ( 𝑝 𝐴 𝑥 ) = 𝑥 } ∈ V )
18 4 13 14 15 17 ovmpod ⊢ ( 𝜑 → ( 𝐵 FixPts 𝐴 ) = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑝 ∈ dom dom 𝐴 ( 𝑝 𝐴 𝑥 ) = 𝑥 } )