Theorem limenpsi

Description: A limit ordinal is equinumerous to a proper subset of itself. (Contributed by NM, 30-Oct-2003) (Revised by Mario Carneiro, 16-Nov-2014)

	Ref	Expression
Hypothesis	limenpsi.1	|- Lim A
Assertion	limenpsi	|- ( A e. V -> A ~~ ( A \ { (/) } ) )

Proof

Step	Hyp	Ref	Expression
1		limenpsi.1	|- Lim A
2		difexg	|- ( A e. V -> ( A \ { (/) } ) e. _V )
3		limsuc	|- ( Lim A -> ( x e. A <-> suc x e. A ) )
4	1 3	ax-mp	|- ( x e. A <-> suc x e. A )
5	4	biimpi	|- ( x e. A -> suc x e. A )
6		nsuceq0	|- suc x =/= (/)
7		eldifsn	|- ( suc x e. ( A \ { (/) } ) <-> ( suc x e. A /\ suc x =/= (/) ) )
8	5 6 7	sylanblrc	|- ( x e. A -> suc x e. ( A \ { (/) } ) )
9		limord	|- ( Lim A -> Ord A )
10	1 9	ax-mp	|- Ord A
11		ordelon	|- ( ( Ord A /\ x e. A ) -> x e. On )
12	10 11	mpan	|- ( x e. A -> x e. On )
13		ordelon	|- ( ( Ord A /\ y e. A ) -> y e. On )
14	10 13	mpan	|- ( y e. A -> y e. On )
15		suc11	|- ( ( x e. On /\ y e. On ) -> ( suc x = suc y <-> x = y ) )
16	12 14 15	syl2an	|- ( ( x e. A /\ y e. A ) -> ( suc x = suc y <-> x = y ) )
17	8 16	dom3	|- ( ( A e. V /\ ( A \ { (/) } ) e. _V ) -> A ~<_ ( A \ { (/) } ) )
18	2 17	mpdan	|- ( A e. V -> A ~<_ ( A \ { (/) } ) )
19		difss	|- ( A \ { (/) } ) C_ A
20		ssdomg	|- ( A e. V -> ( ( A \ { (/) } ) C_ A -> ( A \ { (/) } ) ~<_ A ) )
21	19 20	mpi	|- ( A e. V -> ( A \ { (/) } ) ~<_ A )
22		sbth	|- ( ( A ~<_ ( A \ { (/) } ) /\ ( A \ { (/) } ) ~<_ A ) -> A ~~ ( A \ { (/) } ) )
23	18 21 22	syl2anc	|- ( A e. V -> A ~~ ( A \ { (/) } ) )