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	|- ( ph -> X = suc Y )
	sucneqond.2	|- ( ph -> Y e. On )
Assertion	sucneqond	|- ( ph -> X =/= Y )

Proof

Step	Hyp	Ref	Expression
1		sucneqond.1	|- ( ph -> X = suc Y )
2		sucneqond.2	|- ( ph -> Y e. On )
3		sucidg	|- ( Y e. On -> Y e. suc Y )
4	2 3	syl	|- ( ph -> Y e. suc Y )
5	4 1	eleqtrrd	|- ( ph -> Y e. X )
6		suceloni	|- ( Y e. On -> suc Y e. On )
7	2 6	syl	|- ( ph -> suc Y e. On )
8	1 7	eqeltrd	|- ( ph -> X e. On )
9		eloni	|- ( X e. On -> Ord X )
10	8 9	syl	|- ( ph -> Ord X )
11		ordirr	|- ( Ord X -> -. X e. X )
12	10 11	syl	|- ( ph -> -. X e. X )
13		eleq1	|- ( X = Y -> ( X e. X <-> Y e. X ) )
14	13	biimprd	|- ( X = Y -> ( Y e. X -> X e. X ) )
15	14	con3d	|- ( X = Y -> ( -. X e. X -> -. Y e. X ) )
16	12 15	syl5com	|- ( ph -> ( X = Y -> -. Y e. X ) )
17	5 16	mt2d	|- ( ph -> -. X = Y )
18	17	neqned	|- ( ph -> X =/= Y )