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

Metamath Proof Explorer

Theorem presucmap

Description: pre is really a predecessor (when it should be). This correctness theorem for pre makes it usable in proofs without unfolding iota . This theorem gives one witness; preuniqval gives it is the only one. (Contributed by Peter Mazsa, 12-Jan-2026)

Ref Expression
Assertion presucmap ( 𝑁 ∈ ran SucMap → pre 𝑁 SucMap 𝑁 )

Proof

Step Hyp Ref Expression
1 dfpre2 ⊢ ( 𝑁 ∈ ran SucMap → pre 𝑁 = ( ℩ 𝑚 𝑚 SucMap 𝑁 ) )
2 1 eqcomd ⊢ ( 𝑁 ∈ ran SucMap → ( ℩ 𝑚 𝑚 SucMap 𝑁 ) = pre 𝑁 )
3 preex ⊢ pre 𝑁 ∈ V
4 eupre2 ⊢ ( 𝑁 ∈ ran SucMap → ( 𝑁 ∈ ran SucMap ↔ ∃! 𝑚 𝑚 SucMap 𝑁 ) )
5 4 ibi ⊢ ( 𝑁 ∈ ran SucMap → ∃! 𝑚 𝑚 SucMap 𝑁 )
6 breq1 ⊢ ( 𝑚 = pre 𝑁 → ( 𝑚 SucMap 𝑁 ↔ pre 𝑁 SucMap 𝑁 ) )
7 6 iota2 ⊢ ( ( pre 𝑁 ∈ V ∧ ∃! 𝑚 𝑚 SucMap 𝑁 ) → ( pre 𝑁 SucMap 𝑁 ↔ ( ℩ 𝑚 𝑚 SucMap 𝑁 ) = pre 𝑁 ) )
8 3 5 7 sylancr ⊢ ( 𝑁 ∈ ran SucMap → ( pre 𝑁 SucMap 𝑁 ↔ ( ℩ 𝑚 𝑚 SucMap 𝑁 ) = pre 𝑁 ) )
9 2 8 mpbird ⊢ ( 𝑁 ∈ ran SucMap → pre 𝑁 SucMap 𝑁 )