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 𝐴 )