nlimsucg

Description: A successor is not a limit ordinal. (Contributed by NM, 25-Mar-1995) (Proof shortened by Andrew Salmon, 27-Aug-2011)

		Ref	Expression
	Assertion	nlimsucg	$⊢ A \in V \to \neg Lim suc A$

Step	Hyp	Ref	Expression
1		limord	$⊢ Lim suc A \to Ord suc A$
2		ordsuc	$⊢ Ord A \leftrightarrow Ord suc A$
3	1 2	sylibr	$⊢ Lim suc A \to Ord A$
4		limuni	$⊢ Lim suc A \to suc A = ⋃ suc A$
5		ordunisuc	$⊢ Ord A \to ⋃ suc A = A$
6	5	eqeq2d	$⊢ Ord A \to (suc A = ⋃ suc A \leftrightarrow suc A = A)$
7		ordirr	$⊢ Ord A \to \neg A \in A$
8		eleq2	$⊢ suc A = A \to (A \in suc A \leftrightarrow A \in A)$
9	8	notbid	$⊢ suc A = A \to (\neg A \in suc A \leftrightarrow \neg A \in A)$
10	7 9	syl5ibrcom	$⊢ Ord A \to (suc A = A \to \neg A \in suc A)$
11		sucidg	$⊢ A \in V \to A \in suc A$
12	11	con3i	$⊢ \neg A \in suc A \to \neg A \in V$
13	10 12	syl6	$⊢ Ord A \to (suc A = A \to \neg A \in V)$
14	6 13	sylbid	$⊢ Ord A \to (suc A = ⋃ suc A \to \neg A \in V)$
15	3 4 14	sylc	$⊢ Lim suc A \to \neg A \in V$
16	15	con2i	$⊢ A \in V \to \neg Lim suc A$

Metamath Proof Explorer