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 )