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

Metamath Proof Explorer

Theorem limensuc

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

Ref Expression
Assertion limensuc ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) → 𝐴 ≈ suc 𝐴 )

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ ( 𝐴 = if ( Lim 𝐴 , 𝐴 , On ) → ( 𝐴 ∈ 𝑉 ↔ if ( Lim 𝐴 , 𝐴 , On ) ∈ 𝑉 ) )
2 id ⊢ ( 𝐴 = if ( Lim 𝐴 , 𝐴 , On ) → 𝐴 = if ( Lim 𝐴 , 𝐴 , On ) )
3 suceq ⊢ ( 𝐴 = if ( Lim 𝐴 , 𝐴 , On ) → suc 𝐴 = suc if ( Lim 𝐴 , 𝐴 , On ) )
4 2 3 breq12d ⊢ ( 𝐴 = if ( Lim 𝐴 , 𝐴 , On ) → ( 𝐴 ≈ suc 𝐴 ↔ if ( Lim 𝐴 , 𝐴 , On ) ≈ suc if ( Lim 𝐴 , 𝐴 , On ) ) )
5 1 4 imbi12d ⊢ ( 𝐴 = if ( Lim 𝐴 , 𝐴 , On ) → ( ( 𝐴 ∈ 𝑉 → 𝐴 ≈ suc 𝐴 ) ↔ ( if ( Lim 𝐴 , 𝐴 , On ) ∈ 𝑉 → if ( Lim 𝐴 , 𝐴 , On ) ≈ suc if ( Lim 𝐴 , 𝐴 , On ) ) ) )
6 limeq ⊢ ( 𝐴 = if ( Lim 𝐴 , 𝐴 , On ) → ( Lim 𝐴 ↔ Lim if ( Lim 𝐴 , 𝐴 , On ) ) )
7 limeq ⊢ ( On = if ( Lim 𝐴 , 𝐴 , On ) → ( Lim On ↔ Lim if ( Lim 𝐴 , 𝐴 , On ) ) )
8 limon ⊢ Lim On
9 6 7 8 elimhyp ⊢ Lim if ( Lim 𝐴 , 𝐴 , On )
10 9 limensuci ⊢ ( if ( Lim 𝐴 , 𝐴 , On ) ∈ 𝑉 → if ( Lim 𝐴 , 𝐴 , On ) ≈ suc if ( Lim 𝐴 , 𝐴 , On ) )
11 5 10 dedth ⊢ ( Lim 𝐴 → ( 𝐴 ∈ 𝑉 → 𝐴 ≈ suc 𝐴 ) )
12 11 impcom ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Lim 𝐴 ) → 𝐴 ≈ suc 𝐴 )