This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ordsuc

Description: A class is ordinal if and only if its successor is ordinal. (Contributed by NM, 3-Apr-1995) Avoid ax-un . (Revised by BTernaryTau, 6-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		ordsuci	⊢ ( Ord 𝐴 → Ord suc 𝐴 )
2		sucidg	⊢ ( 𝐴 ∈ V → 𝐴 ∈ suc 𝐴 )
3		ordelord	⊢ ( ( Ord suc 𝐴 ∧ 𝐴 ∈ suc 𝐴 ) → Ord 𝐴 )
4	3	ex	⊢ ( Ord suc 𝐴 → ( 𝐴 ∈ suc 𝐴 → Ord 𝐴 ) )
5	2 4	syl5com	⊢ ( 𝐴 ∈ V → ( Ord suc 𝐴 → Ord 𝐴 ) )
6		sucprc	⊢ ( ¬ 𝐴 ∈ V → suc 𝐴 = 𝐴 )
7	6	eqcomd	⊢ ( ¬ 𝐴 ∈ V → 𝐴 = suc 𝐴 )
8		ordeq	⊢ ( 𝐴 = suc 𝐴 → ( Ord 𝐴 ↔ Ord suc 𝐴 ) )
9	7 8	syl	⊢ ( ¬ 𝐴 ∈ V → ( Ord 𝐴 ↔ Ord suc 𝐴 ) )
10	9	biimprd	⊢ ( ¬ 𝐴 ∈ V → ( Ord suc 𝐴 → Ord 𝐴 ) )
11	5 10	pm2.61i	⊢ ( Ord suc 𝐴 → Ord 𝐴 )
12	1 11	impbii	⊢ ( Ord 𝐴 ↔ Ord suc 𝐴 )