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 A \leftrightarrow Ord suc A$

Proof

Step	Hyp	Ref	Expression
1		ordsuci	$⊢ Ord A \to Ord suc A$
2		sucidg	$⊢ A \in V \to A \in suc A$
3		ordelord	$⊢ (Ord suc A \land A \in suc A) \to Ord A$
4	3	ex	$⊢ Ord suc A \to (A \in suc A \to Ord A)$
5	2 4	syl5com	$⊢ A \in V \to (Ord suc A \to Ord A)$
6		sucprc	$⊢ \neg A \in V \to suc A = A$
7	6	eqcomd	$⊢ \neg A \in V \to A = suc A$
8		ordeq	$⊢ A = suc A \to (Ord A \leftrightarrow Ord suc A)$
9	7 8	syl	$⊢ \neg A \in V \to (Ord A \leftrightarrow Ord suc A)$
10	9	biimprd	$⊢ \neg A \in V \to (Ord suc A \to Ord A)$
11	5 10	pm2.61i	$⊢ Ord suc A \to Ord A$
12	1 11	impbii	$⊢ Ord A \leftrightarrow Ord suc A$