Metamath Proof Explorer

Theorem ordsucOLD

Description: Obsolete version of ordsuc as of 6-Jan-2025. (Contributed by NM, 3-Apr-1995) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	ordsucOLD	$⊢ Ord A \leftrightarrow Ord suc A$

Proof

Step	Hyp	Ref	Expression
1		elong	$⊢ A \in V \to (A \in On \leftrightarrow Ord A)$
2		onsuc	$⊢ A \in On \to suc A \in On$
3		eloni	$⊢ suc A \in On \to Ord suc A$
4	2 3	syl	$⊢ A \in On \to Ord suc A$
5	1 4	syl6bir	$⊢ A \in V \to (Ord A \to Ord suc A)$
6		sucidg	$⊢ A \in V \to A \in suc A$
7		ordelord	$⊢ (Ord suc A \land A \in suc A) \to Ord A$
8	7	ex	$⊢ Ord suc A \to (A \in suc A \to Ord A)$
9	6 8	syl5com	$⊢ A \in V \to (Ord suc A \to Ord A)$
10	5 9	impbid	$⊢ A \in V \to (Ord A \leftrightarrow Ord suc A)$
11		sucprc	$⊢ \neg A \in V \to suc A = A$
12	11	eqcomd	$⊢ \neg A \in V \to A = suc A$
13		ordeq	$⊢ A = suc A \to (Ord A \leftrightarrow Ord suc A)$
14	12 13	syl	$⊢ \neg A \in V \to (Ord A \leftrightarrow Ord suc A)$
15	10 14	pm2.61i	$⊢ Ord A \leftrightarrow Ord suc A$