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 ( 𝐴 ∈ ω → 𝐴 ≠ suc 𝐴 )

Proof

Step Hyp Ref Expression
1 nnord ( 𝐴 ∈ ω → Ord 𝐴 )
2 orddisj ( Ord 𝐴 → ( 𝐴 ∩ { 𝐴 } ) = ∅ )
3 1 2 syl ( 𝐴 ∈ ω → ( 𝐴 ∩ { 𝐴 } ) = ∅ )
4 snnzg ( 𝐴 ∈ ω → { 𝐴 } ≠ ∅ )
5 disjpss ( ( ( 𝐴 ∩ { 𝐴 } ) = ∅ ∧ { 𝐴 } ≠ ∅ ) → 𝐴 ⊊ ( 𝐴 ∪ { 𝐴 } ) )
6 3 4 5 syl2anc ( 𝐴 ∈ ω → 𝐴 ⊊ ( 𝐴 ∪ { 𝐴 } ) )
7 6 pssned ( 𝐴 ∈ ω → 𝐴 ≠ ( 𝐴 ∪ { 𝐴 } ) )
8 df-suc suc 𝐴 = ( 𝐴 ∪ { 𝐴 } )
9 8 neeq2i ( 𝐴 ≠ suc 𝐴𝐴 ≠ ( 𝐴 ∪ { 𝐴 } ) )
10 7 9 sylibr ( 𝐴 ∈ ω → 𝐴 ≠ suc 𝐴 )