Theorem preel

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

	Ref	Expression
Assertion	preel	⊢ ( 𝑁 ∈ Suc → pre 𝑁 ∈ 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		preex	⊢ pre 𝑁 ∈ V
2	1	sucid	⊢ pre 𝑁 ∈ suc pre 𝑁
3		sucpre	⊢ ( 𝑁 ∈ Suc → suc pre 𝑁 = 𝑁 )
4	2 3	eleqtrid	⊢ ( 𝑁 ∈ Suc → pre 𝑁 ∈ 𝑁 )