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

Metamath Proof Explorer

Theorem limensuci

Description: A limit ordinal is equinumerous to its successor. (Contributed by NM, 30-Oct-2003)

Ref Expression
Hypothesis limensuci.1 ⊢ Lim 𝐴
Assertion limensuci ( 𝐴 ∈ 𝑉 → 𝐴 ≈ suc 𝐴 )

Proof

Step Hyp Ref Expression
1 limensuci.1 ⊢ Lim 𝐴
2 1 limenpsi ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ≈ ( 𝐴 ∖ { ∅ } ) )
3 2 ensymd ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∖ { ∅ } ) ≈ 𝐴 )
4 0ex ⊢ ∅ ∈ V
5 en2sn ⊢ ( ( ∅ ∈ V ∧ 𝐴 ∈ 𝑉 ) → { ∅ } ≈ { 𝐴 } )
6 4 5 mpan ⊢ ( 𝐴 ∈ 𝑉 → { ∅ } ≈ { 𝐴 } )
7 disjdifr ⊢ ( ( 𝐴 ∖ { ∅ } ) ∩ { ∅ } ) = ∅
8 limord ⊢ ( Lim 𝐴 → Ord 𝐴 )
9 1 8 ax-mp ⊢ Ord 𝐴
10 ordirr ⊢ ( Ord 𝐴 → ¬ 𝐴 ∈ 𝐴 )
11 9 10 ax-mp ⊢ ¬ 𝐴 ∈ 𝐴
12 disjsn ⊢ ( ( 𝐴 ∩ { 𝐴 } ) = ∅ ↔ ¬ 𝐴 ∈ 𝐴 )
13 11 12 mpbir ⊢ ( 𝐴 ∩ { 𝐴 } ) = ∅
14 unen ⊢ ( ( ( ( 𝐴 ∖ { ∅ } ) ≈ 𝐴 ∧ { ∅ } ≈ { 𝐴 } ) ∧ ( ( ( 𝐴 ∖ { ∅ } ) ∩ { ∅ } ) = ∅ ∧ ( 𝐴 ∩ { 𝐴 } ) = ∅ ) ) → ( ( 𝐴 ∖ { ∅ } ) ∪ { ∅ } ) ≈ ( 𝐴 ∪ { 𝐴 } ) )
15 7 13 14 mpanr12 ⊢ ( ( ( 𝐴 ∖ { ∅ } ) ≈ 𝐴 ∧ { ∅ } ≈ { 𝐴 } ) → ( ( 𝐴 ∖ { ∅ } ) ∪ { ∅ } ) ≈ ( 𝐴 ∪ { 𝐴 } ) )
16 3 6 15 syl2anc ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ∖ { ∅ } ) ∪ { ∅ } ) ≈ ( 𝐴 ∪ { 𝐴 } ) )
17 0ellim ⊢ ( Lim 𝐴 → ∅ ∈ 𝐴 )
18 1 17 ax-mp ⊢ ∅ ∈ 𝐴
19 4 snss ⊢ ( ∅ ∈ 𝐴 ↔ { ∅ } ⊆ 𝐴 )
20 18 19 mpbi ⊢ { ∅ } ⊆ 𝐴
21 undif ⊢ ( { ∅ } ⊆ 𝐴 ↔ ( { ∅ } ∪ ( 𝐴 ∖ { ∅ } ) ) = 𝐴 )
22 20 21 mpbi ⊢ ( { ∅ } ∪ ( 𝐴 ∖ { ∅ } ) ) = 𝐴
23 uncom ⊢ ( { ∅ } ∪ ( 𝐴 ∖ { ∅ } ) ) = ( ( 𝐴 ∖ { ∅ } ) ∪ { ∅ } )
24 22 23 eqtr3i ⊢ 𝐴 = ( ( 𝐴 ∖ { ∅ } ) ∪ { ∅ } )
25 df-suc ⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } )
26 16 24 25 3brtr4g ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ≈ suc 𝐴 )