Theorem press

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

	Ref	Expression
Assertion	press	⊢ ( 𝑁 ∈ Suc → pre 𝑁 ⊆ 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		sssucid	⊢ pre 𝑁 ⊆ suc pre 𝑁
2		sucpre	⊢ ( 𝑁 ∈ Suc → suc pre 𝑁 = 𝑁 )
3	1 2	sseqtrid	⊢ ( 𝑁 ∈ Suc → pre 𝑁 ⊆ 𝑁 )