Metamath Proof Explorer


Theorem omsucne

Description: A natural number is not the successor of itself. (Contributed by AV, 17-Oct-2023)

Ref Expression
Assertion omsucne
|- ( A e. _om -> A =/= suc A )

Proof

Step Hyp Ref Expression
1 nnord
 |-  ( A e. _om -> Ord A )
2 orddisj
 |-  ( Ord A -> ( A i^i { A } ) = (/) )
3 1 2 syl
 |-  ( A e. _om -> ( A i^i { A } ) = (/) )
4 snnzg
 |-  ( A e. _om -> { A } =/= (/) )
5 disjpss
 |-  ( ( ( A i^i { A } ) = (/) /\ { A } =/= (/) ) -> A C. ( A u. { A } ) )
6 3 4 5 syl2anc
 |-  ( A e. _om -> A C. ( A u. { A } ) )
7 6 pssned
 |-  ( A e. _om -> A =/= ( A u. { A } ) )
8 df-suc
 |-  suc A = ( A u. { A } )
9 8 neeq2i
 |-  ( A =/= suc A <-> A =/= ( A u. { A } ) )
10 7 9 sylibr
 |-  ( A e. _om -> A =/= suc A )