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