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 𝐴
Assertion	limenpsi	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ≈ ( 𝐴 ∖ { ∅ } ) )

Proof

Step	Hyp	Ref	Expression
1		limenpsi.1	⊢ Lim 𝐴
2		difexg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∖ { ∅ } ) ∈ V )
3		limsuc	⊢ ( Lim 𝐴 → ( 𝑥 ∈ 𝐴 ↔ suc 𝑥 ∈ 𝐴 ) )
4	1 3	ax-mp	⊢ ( 𝑥 ∈ 𝐴 ↔ suc 𝑥 ∈ 𝐴 )
5	4	biimpi	⊢ ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 )
6		nsuceq0	⊢ suc 𝑥 ≠ ∅
7		eldifsn	⊢ ( suc 𝑥 ∈ ( 𝐴 ∖ { ∅ } ) ↔ ( suc 𝑥 ∈ 𝐴 ∧ suc 𝑥 ≠ ∅ ) )
8	5 6 7	sylanblrc	⊢ ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ ( 𝐴 ∖ { ∅ } ) )
9		limord	⊢ ( Lim 𝐴 → Ord 𝐴 )
10	1 9	ax-mp	⊢ Ord 𝐴
11		ordelon	⊢ ( ( Ord 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ On )
12	10 11	mpan	⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ On )
13		ordelon	⊢ ( ( Ord 𝐴 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ On )
14	10 13	mpan	⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ∈ On )
15		suc11	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( suc 𝑥 = suc 𝑦 ↔ 𝑥 = 𝑦 ) )
16	12 14 15	syl2an	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( suc 𝑥 = suc 𝑦 ↔ 𝑥 = 𝑦 ) )
17	8 16	dom3	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐴 ∖ { ∅ } ) ∈ V ) → 𝐴 ≼ ( 𝐴 ∖ { ∅ } ) )
18	2 17	mpdan	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ≼ ( 𝐴 ∖ { ∅ } ) )
19		difss	⊢ ( 𝐴 ∖ { ∅ } ) ⊆ 𝐴
20		ssdomg	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ∖ { ∅ } ) ⊆ 𝐴 → ( 𝐴 ∖ { ∅ } ) ≼ 𝐴 ) )
21	19 20	mpi	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∖ { ∅ } ) ≼ 𝐴 )
22		sbth	⊢ ( ( 𝐴 ≼ ( 𝐴 ∖ { ∅ } ) ∧ ( 𝐴 ∖ { ∅ } ) ≼ 𝐴 ) → 𝐴 ≈ ( 𝐴 ∖ { ∅ } ) )
23	18 21 22	syl2anc	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ≈ ( 𝐴 ∖ { ∅ } ) )