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

Metamath Proof Explorer

Theorem dfpre

Description: Alternate definition of the successor-predecessor. (Contributed by Peter Mazsa, 27-Jan-2026)

Ref Expression
Assertion dfpre pre 𝑁 = ( ℩ 𝑚 𝑚 ∈ Pred ( SucMap , V , 𝑁 ) )

Proof

Step Hyp Ref Expression
1 df-pre ⊢ pre 𝑁 = ( ℩ 𝑚 𝑚 ∈ Pred ( SucMap , dom SucMap , 𝑁 ) )
2 dmsucmap ⊢ dom SucMap = V
3 predeq2 ⊢ ( dom SucMap = V → Pred ( SucMap , dom SucMap , 𝑁 ) = Pred ( SucMap , V , 𝑁 ) )
4 2 3 ax-mp ⊢ Pred ( SucMap , dom SucMap , 𝑁 ) = Pred ( SucMap , V , 𝑁 )
5 4 eleq2i ⊢ ( 𝑚 ∈ Pred ( SucMap , dom SucMap , 𝑁 ) ↔ 𝑚 ∈ Pred ( SucMap , V , 𝑁 ) )
6 5 iotabii ⊢ ( ℩ 𝑚 𝑚 ∈ Pred ( SucMap , dom SucMap , 𝑁 ) ) = ( ℩ 𝑚 𝑚 ∈ Pred ( SucMap , V , 𝑁 ) )
7 1 6 eqtri ⊢ pre 𝑁 = ( ℩ 𝑚 𝑚 ∈ Pred ( SucMap , V , 𝑁 ) )