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 |-