Theorem preex

Description: The successor-predecessor exists. (Contributed by Peter Mazsa, 12-Jan-2026)

	Ref	Expression
Assertion	preex	Could not format assertion : No typesetting found for |- pre N e. _V with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-pre	Could not format pre N = ( iota m m e. Pred ( SucMap , dom SucMap , N ) ) : No typesetting found for |- pre N = ( iota m m e. Pred ( SucMap , dom SucMap , N ) ) with typecode |-
2		iotaex	Could not format ( iota m m e. Pred ( SucMap , dom SucMap , N ) ) e. _V : No typesetting found for |- ( iota m m e. Pred ( SucMap , dom SucMap , N ) ) e. _V with typecode |-
3	1 2	eqeltri	Could not format pre N e. _V : No typesetting found for |- pre N e. _V with typecode |-