Theorem omsucne

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

	Ref	Expression
Assertion	omsucne	$$⊢A\in \mathrm{\omega }\to A\ne \mathrm{suc}A$$

Proof

Step	Hyp	Ref	Expression
1		nnord	$$⊢A\in \mathrm{\omega }\to \mathrm{Ord}A$$
2		orddisj	$$⊢\mathrm{Ord}A\to A\cap \left\{A\right\}=\varnothing$$
3	1 2	syl	$$⊢A\in \mathrm{\omega }\to A\cap \left\{A\right\}=\varnothing$$
4		snnzg	$$⊢A\in \mathrm{\omega }\to \left\{A\right\}\ne \varnothing$$
5		disjpss	$$⊢\left(A\cap \left\{A\right\}=\varnothing \wedge \left\{A\right\}\ne \varnothing \right)\to A\subset A\cup \left\{A\right\}$$
6	3 4 5	syl2anc	$$⊢A\in \mathrm{\omega }\to A\subset A\cup \left\{A\right\}$$
7	6	pssned	$$⊢A\in \mathrm{\omega }\to A\ne A\cup \left\{A\right\}$$
8		df-suc	$$⊢\mathrm{suc}A=A\cup \left\{A\right\}$$
9	8	neeq2i	$$⊢A\ne \mathrm{suc}A\leftrightarrow A\ne A\cup \left\{A\right\}$$
10	7 9	sylibr	$$⊢A\in \mathrm{\omega }\to A\ne \mathrm{suc}A$$