Metamath Proof Explorer

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 ${⊢}\mathrm{Lim}{A}$
Assertion limenpsi ${⊢}{A}\in {V}\to {A}\approx \left({A}\setminus \left\{\varnothing \right\}\right)$

Proof

Step Hyp Ref Expression
1 limenpsi.1 ${⊢}\mathrm{Lim}{A}$
2 difexg ${⊢}{A}\in {V}\to {A}\setminus \left\{\varnothing \right\}\in \mathrm{V}$
3 limsuc ${⊢}\mathrm{Lim}{A}\to \left({x}\in {A}↔\mathrm{suc}{x}\in {A}\right)$
4 1 3 ax-mp ${⊢}{x}\in {A}↔\mathrm{suc}{x}\in {A}$
5 4 biimpi ${⊢}{x}\in {A}\to \mathrm{suc}{x}\in {A}$
6 nsuceq0 ${⊢}\mathrm{suc}{x}\ne \varnothing$
7 eldifsn ${⊢}\mathrm{suc}{x}\in \left({A}\setminus \left\{\varnothing \right\}\right)↔\left(\mathrm{suc}{x}\in {A}\wedge \mathrm{suc}{x}\ne \varnothing \right)$
8 5 6 7 sylanblrc ${⊢}{x}\in {A}\to \mathrm{suc}{x}\in \left({A}\setminus \left\{\varnothing \right\}\right)$
9 limord ${⊢}\mathrm{Lim}{A}\to \mathrm{Ord}{A}$
10 1 9 ax-mp ${⊢}\mathrm{Ord}{A}$
11 ordelon ${⊢}\left(\mathrm{Ord}{A}\wedge {x}\in {A}\right)\to {x}\in \mathrm{On}$
12 10 11 mpan ${⊢}{x}\in {A}\to {x}\in \mathrm{On}$
13 ordelon ${⊢}\left(\mathrm{Ord}{A}\wedge {y}\in {A}\right)\to {y}\in \mathrm{On}$
14 10 13 mpan ${⊢}{y}\in {A}\to {y}\in \mathrm{On}$
15 suc11 ${⊢}\left({x}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\to \left(\mathrm{suc}{x}=\mathrm{suc}{y}↔{x}={y}\right)$
16 12 14 15 syl2an ${⊢}\left({x}\in {A}\wedge {y}\in {A}\right)\to \left(\mathrm{suc}{x}=\mathrm{suc}{y}↔{x}={y}\right)$
17 8 16 dom3 ${⊢}\left({A}\in {V}\wedge {A}\setminus \left\{\varnothing \right\}\in \mathrm{V}\right)\to {A}\preccurlyeq \left({A}\setminus \left\{\varnothing \right\}\right)$
18 2 17 mpdan ${⊢}{A}\in {V}\to {A}\preccurlyeq \left({A}\setminus \left\{\varnothing \right\}\right)$
19 difss ${⊢}{A}\setminus \left\{\varnothing \right\}\subseteq {A}$
20 ssdomg ${⊢}{A}\in {V}\to \left({A}\setminus \left\{\varnothing \right\}\subseteq {A}\to \left({A}\setminus \left\{\varnothing \right\}\right)\preccurlyeq {A}\right)$
21 19 20 mpi ${⊢}{A}\in {V}\to \left({A}\setminus \left\{\varnothing \right\}\right)\preccurlyeq {A}$
22 sbth ${⊢}\left({A}\preccurlyeq \left({A}\setminus \left\{\varnothing \right\}\right)\wedge \left({A}\setminus \left\{\varnothing \right\}\right)\preccurlyeq {A}\right)\to {A}\approx \left({A}\setminus \left\{\varnothing \right\}\right)$
23 18 21 22 syl2anc ${⊢}{A}\in {V}\to {A}\approx \left({A}\setminus \left\{\varnothing \right\}\right)$