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	⊢ 𝑋 = suc 𝑌
	sucneqoni.2	⊢ 𝑌 ∈ On
Assertion	sucneqoni	⊢ 𝑋 ≠ 𝑌

Proof

Step	Hyp	Ref	Expression
1		sucneqoni.1	⊢ 𝑋 = suc 𝑌
2		sucneqoni.2	⊢ 𝑌 ∈ On
3	1	a1i	⊢ ( ⊤ → 𝑋 = suc 𝑌 )
4	2	a1i	⊢ ( ⊤ → 𝑌 ∈ On )
5	3 4	sucneqond	⊢ ( ⊤ → 𝑋 ≠ 𝑌 )
6	5	mptru	⊢ 𝑋 ≠ 𝑌