Theorem onepsuc

Description: Every ordinal is less than its successor, relationship version. Lemma 1.7 of Schloeder p. 1. (Contributed by RP, 15-Jan-2025)

	Ref	Expression
Assertion	onepsuc	⊢ ( 𝐴 ∈ On → 𝐴 E suc 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		sucidg	⊢ ( 𝐴 ∈ On → 𝐴 ∈ suc 𝐴 )
2		onsuc	⊢ ( 𝐴 ∈ On → suc 𝐴 ∈ On )
3		epelg	⊢ ( suc 𝐴 ∈ On → ( 𝐴 E suc 𝐴 ↔ 𝐴 ∈ suc 𝐴 ) )
4	2 3	syl	⊢ ( 𝐴 ∈ On → ( 𝐴 E suc 𝐴 ↔ 𝐴 ∈ suc 𝐴 ) )
5	1 4	mpbird	⊢ ( 𝐴 ∈ On → 𝐴 E suc 𝐴 )