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 \in V \to A \approx (A ∖ \{\emptyset\})$

Proof

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

Metamath Proof Explorer

Theorem limenpsi

Proof