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 𝐴 ( 𝑝 𝐴 𝑥 ) = 𝑥 } )