Theorem sucneqond

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	sucneqond.1	$$⊢\phi \to X=\mathrm{suc}Y$$
	sucneqond.2	$$⊢\phi \to Y\in \mathrm{On}$$
Assertion	sucneqond	$$⊢\phi \to X\ne Y$$

Proof

Step	Hyp	Ref	Expression
1		sucneqond.1	$$⊢\phi \to X=\mathrm{suc}Y$$
2		sucneqond.2	$$⊢\phi \to Y\in \mathrm{On}$$
3		sucidg	$$⊢Y\in \mathrm{On}\to Y\in \mathrm{suc}Y$$
4	2 3	syl	$$⊢\phi \to Y\in \mathrm{suc}Y$$
5	4 1	eleqtrrd	$$⊢\phi \to Y\in X$$
6		onsuc	$$⊢Y\in \mathrm{On}\to \mathrm{suc}Y\in \mathrm{On}$$
7	2 6	syl	$$⊢\phi \to \mathrm{suc}Y\in \mathrm{On}$$
8	1 7	eqeltrd	$$⊢\phi \to X\in \mathrm{On}$$
9		eloni	$$⊢X\in \mathrm{On}\to \mathrm{Ord}X$$
10	8 9	syl	$$⊢\phi \to \mathrm{Ord}X$$
11		ordirr	$$⊢\mathrm{Ord}X\to \neg X\in X$$
12	10 11	syl	$$⊢\phi \to \neg X\in X$$
13		eleq1	$$⊢X=Y\to \left(X\in X\leftrightarrow Y\in X\right)$$
14	13	biimprd	$$⊢X=Y\to \left(Y\in X\to X\in X\right)$$
15	14	con3d	$$⊢X=Y\to \left(\neg X\in X\to \neg Y\in X\right)$$
16	12 15	syl5com	$$⊢\phi \to \left(X=Y\to \neg Y\in X\right)$$
17	5 16	mt2d	$$⊢\phi \to \neg X=Y$$
18	17	neqned	$$⊢\phi \to X\ne Y$$