This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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