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 = suc Y
	sucneqoni.2	|- Y e. On
Assertion	sucneqoni	|- X =/= Y

Proof

Step	Hyp	Ref	Expression
1		sucneqoni.1	|- X = suc Y
2		sucneqoni.2	|- Y e. On
3	1	a1i	|- ( T. -> X = suc Y )
4	2	a1i	|- ( T. -> Y e. On )
5	3 4	sucneqond	|- ( T. -> X =/= Y )
6	5	mptru	|- X =/= Y