Theorem ordsuc

Description: The successor of an ordinal class is ordinal. (Contributed by NM, 3-Apr-1995)

	Ref	Expression
Assertion	ordsuc	⊢ ( Ord 𝐴 ↔ Ord suc 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		elong	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ On ↔ Ord 𝐴 ) )
2		suceloni	⊢ ( 𝐴 ∈ On → suc 𝐴 ∈ On )
3		eloni	⊢ ( suc 𝐴 ∈ On → Ord suc 𝐴 )
4	2 3	syl	⊢ ( 𝐴 ∈ On → Ord suc 𝐴 )
5	1 4	syl6bir	⊢ ( 𝐴 ∈ V → ( Ord 𝐴 → Ord suc 𝐴 ) )
6		sucidg	⊢ ( 𝐴 ∈ V → 𝐴 ∈ suc 𝐴 )
7		ordelord	⊢ ( ( Ord suc 𝐴 ∧ 𝐴 ∈ suc 𝐴 ) → Ord 𝐴 )
8	7	ex	⊢ ( Ord suc 𝐴 → ( 𝐴 ∈ suc 𝐴 → Ord 𝐴 ) )
9	6 8	syl5com	⊢ ( 𝐴 ∈ V → ( Ord suc 𝐴 → Ord 𝐴 ) )
10	5 9	impbid	⊢ ( 𝐴 ∈ V → ( Ord 𝐴 ↔ Ord suc 𝐴 ) )
11		sucprc	⊢ ( ¬ 𝐴 ∈ V → suc 𝐴 = 𝐴 )
12	11	eqcomd	⊢ ( ¬ 𝐴 ∈ V → 𝐴 = suc 𝐴 )
13		ordeq	⊢ ( 𝐴 = suc 𝐴 → ( Ord 𝐴 ↔ Ord suc 𝐴 ) )
14	12 13	syl	⊢ ( ¬ 𝐴 ∈ V → ( Ord 𝐴 ↔ Ord suc 𝐴 ) )
15	10 14	pm2.61i	⊢ ( Ord 𝐴 ↔ Ord suc 𝐴 )