Theorem sucneqoni

Description: Inequality of an ordinal set with its successor. Does not use the axiom of regularity. (Contributed by ML, 18-Oct-2020)

	Ref	Expression
Hypotheses	sucneqoni.1	$$⊢X=\mathrm{suc}Y$$
	sucneqoni.2	$$⊢Y\in \mathrm{On}$$
Assertion	sucneqoni	$$⊢X\ne Y$$

Proof

Step	Hyp	Ref	Expression
1		sucneqoni.1	$$⊢X=\mathrm{suc}Y$$
2		sucneqoni.2	$$⊢Y\in \mathrm{On}$$
3	1	a1i	$$⊢\top \to X=\mathrm{suc}Y$$
4	2	a1i	$$⊢\top \to Y\in \mathrm{On}$$
5	3 4	sucneqond	$$⊢\top \to X\ne Y$$
6	5	mptru	$$⊢X\ne Y$$