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 ⊢ φ → B ∈ V
fxpval.2 ⊢ φ → A ∈ W
Assertion fxpval Could not format assertion : No typesetting found for |- ( ph -> ( B FixPts A ) = { x e. B | A. p e. dom dom A ( p A x ) = x } ) with typecode |-

Proof

Step Hyp Ref Expression
1 fxpval.1 ⊢ φ → B ∈ V
2 fxpval.2 ⊢ φ → A ∈ W
3 df-fxp Could not format FixPts = ( b e. _V , a e. _V |-> { x e. b | A. p e. dom dom a ( p a x ) = x } ) : No typesetting found for |- FixPts = ( b e. _V , a e. _V |-> { x e. b | A. p e. dom dom a ( p a x ) = x } ) with typecode |-
4 3 a1i Could not format ( ph -> FixPts = ( b e. _V , a e. _V |-> { x e. b | A. p e. dom dom a ( p a x ) = x } ) ) : No typesetting found for |- ( ph -> FixPts = ( b e. _V , a e. _V |-> { x e. b | A. p e. dom dom a ( p a x ) = x } ) ) with typecode |-
5 simpl ⊢ b = B ∧ a = A → b = B
6 dmeq ⊢ a = A → dom ⁡ a = dom ⁡ A
7 6 dmeqd ⊢ a = A → dom ⁡ dom ⁡ a = dom ⁡ dom ⁡ A
8 oveq ⊢ a = A → p a x = p A x
9 8 eqeq1d ⊢ a = A → p a x = x ↔ p A x = x
10 7 9 raleqbidv ⊢ a = A → ∀ p ∈ dom ⁡ dom ⁡ a p a x = x ↔ ∀ p ∈ dom ⁡ dom ⁡ A p A x = x
11 10 adantl ⊢ b = B ∧ a = A → ∀ p ∈ dom ⁡ dom ⁡ a p a x = x ↔ ∀ p ∈ dom ⁡ dom ⁡ A p A x = x
12 5 11 rabeqbidv ⊢ b = B ∧ a = A → x ∈ b | ∀ p ∈ dom ⁡ dom ⁡ a p a x = x = x ∈ B | ∀ p ∈ dom ⁡ dom ⁡ A p A x = x
13 12 adantl ⊢ φ ∧ b = B ∧ a = A → x ∈ b | ∀ p ∈ dom ⁡ dom ⁡ a p a x = x = x ∈ B | ∀ p ∈ dom ⁡ dom ⁡ A p A x = x
14 1 elexd ⊢ φ → B ∈ V
15 2 elexd ⊢ φ → A ∈ V
16 eqid ⊢ x ∈ B | ∀ p ∈ dom ⁡ dom ⁡ A p A x = x = x ∈ B | ∀ p ∈ dom ⁡ dom ⁡ A p A x = x
17 16 1 rabexd ⊢ φ → x ∈ B | ∀ p ∈ dom ⁡ dom ⁡ A p A x = x ∈ V
18 4 13 14 15 17 ovmpod Could not format ( ph -> ( B FixPts A ) = { x e. B | A. p e. dom dom A ( p A x ) = x } ) : No typesetting found for |- ( ph -> ( B FixPts A ) = { x e. B | A. p e. dom dom A ( p A x ) = x } ) with typecode |-