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	⊢ ( 𝜑 → 𝑋 = suc 𝑌 )
	sucneqond.2	⊢ ( 𝜑 → 𝑌 ∈ On )
Assertion	sucneqond	⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		sucneqond.1	⊢ ( 𝜑 → 𝑋 = suc 𝑌 )
2		sucneqond.2	⊢ ( 𝜑 → 𝑌 ∈ On )
3		sucidg	⊢ ( 𝑌 ∈ On → 𝑌 ∈ suc 𝑌 )
4	2 3	syl	⊢ ( 𝜑 → 𝑌 ∈ suc 𝑌 )
5	4 1	eleqtrrd	⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
6		suceloni	⊢ ( 𝑌 ∈ On → suc 𝑌 ∈ On )
7	2 6	syl	⊢ ( 𝜑 → suc 𝑌 ∈ On )
8	1 7	eqeltrd	⊢ ( 𝜑 → 𝑋 ∈ On )
9		eloni	⊢ ( 𝑋 ∈ On → Ord 𝑋 )
10	8 9	syl	⊢ ( 𝜑 → Ord 𝑋 )
11		ordirr	⊢ ( Ord 𝑋 → ¬ 𝑋 ∈ 𝑋 )
12	10 11	syl	⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑋 )
13		eleq1	⊢ ( 𝑋 = 𝑌 → ( 𝑋 ∈ 𝑋 ↔ 𝑌 ∈ 𝑋 ) )
14	13	biimprd	⊢ ( 𝑋 = 𝑌 → ( 𝑌 ∈ 𝑋 → 𝑋 ∈ 𝑋 ) )
15	14	con3d	⊢ ( 𝑋 = 𝑌 → ( ¬ 𝑋 ∈ 𝑋 → ¬ 𝑌 ∈ 𝑋 ) )
16	12 15	syl5com	⊢ ( 𝜑 → ( 𝑋 = 𝑌 → ¬ 𝑌 ∈ 𝑋 ) )
17	5 16	mt2d	⊢ ( 𝜑 → ¬ 𝑋 = 𝑌 )
18	17	neqned	⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )