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

Metamath Proof Explorer

Theorem dfpre2

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

Ref Expression
Assertion dfpre2 Could not format assertion : No typesetting found for |- ( N e. V -> pre N = ( iota m m SucMap N ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 dfpre Could not format pre N = ( iota m m e. Pred ( SucMap , _V , N ) ) : No typesetting found for |- pre N = ( iota m m e. Pred ( SucMap , _V , N ) ) with typecode |-
2 elpredg Could not format ( ( N e. V /\ m e. _V ) -> ( m e. Pred ( SucMap , _V , N ) <-> m SucMap N ) ) : No typesetting found for |- ( ( N e. V /\ m e. _V ) -> ( m e. Pred ( SucMap , _V , N ) <-> m SucMap N ) ) with typecode |-
3 2 elvd Could not format ( N e. V -> ( m e. Pred ( SucMap , _V , N ) <-> m SucMap N ) ) : No typesetting found for |- ( N e. V -> ( m e. Pred ( SucMap , _V , N ) <-> m SucMap N ) ) with typecode |-
4 3 iotabidv Could not format ( N e. V -> ( iota m m e. Pred ( SucMap , _V , N ) ) = ( iota m m SucMap N ) ) : No typesetting found for |- ( N e. V -> ( iota m m e. Pred ( SucMap , _V , N ) ) = ( iota m m SucMap N ) ) with typecode |-
5 1 4 eqtrid Could not format ( N e. V -> pre N = ( iota m m SucMap N ) ) : No typesetting found for |- ( N e. V -> pre N = ( iota m m SucMap N ) ) with typecode |-