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 𝐴 )