Theorem dfpre2

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

	Ref	Expression
Assertion	dfpre2	|- ( N e. V -> pre N = ( iota m m SucMap N ) )

Proof

Step	Hyp	Ref	Expression
1		dfpre	|- pre N = ( iota m m e. Pred ( SucMap , _V , N ) )
2		elpredg	|- ( ( N e. V /\ m e. _V ) -> ( m e. Pred ( SucMap , _V , N ) <-> m SucMap N ) )
3	2	elvd	|- ( N e. V -> ( m e. Pred ( SucMap , _V , N ) <-> m SucMap N ) )
4	3	iotabidv	|- ( N e. V -> ( iota m m e. Pred ( SucMap , _V , N ) ) = ( iota m m SucMap N ) )
5	1 4	eqtrid	|- ( N e. V -> pre N = ( iota m m SucMap N ) )