Metamath Proof Explorer

Theorem press

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

Ref Expression
Assertion press 
|- ( N e. Suc -> pre N C_ N )

Proof

Step Hyp Ref Expression
1 sssucid 
 |-  pre N C_ suc pre N
2 sucpre 
 |-  ( N e. Suc -> suc pre N = N )
3 1 2 sseqtrid 
 |-  ( N e. Suc -> pre N C_ N )