Theorem preel

Description: Predecessor is a subset of its successor. (Contributed by Peter Mazsa, 12-Jan-2026)

	Ref	Expression
Assertion	preel	Could not format assertion : No typesetting found for |- ( N e. Suc -> pre N e. N ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		preex	Could not format pre N e. _V : No typesetting found for |- pre N e. _V with typecode |-
2	1	sucid	Could not format pre N e. suc pre N : No typesetting found for |- pre N e. suc pre N with typecode |-
3		sucpre	Could not format ( N e. Suc -> suc pre N = N ) : No typesetting found for |- ( N e. Suc -> suc pre N = N ) with typecode |-
4	2 3	eleqtrid	Could not format ( N e. Suc -> pre N e. N ) : No typesetting found for |- ( N e. Suc -> pre N e. N ) with typecode |-