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 A
Assertion limensuci 
|- ( A e. V -> A ~~ suc A )

Proof

Step Hyp Ref Expression
1 limensuci.1 
 |-  Lim A
2 1 limenpsi 
 |-  ( A e. V -> A ~~ ( A \ { (/) } ) )
3 2 ensymd 
 |-  ( A e. V -> ( A \ { (/) } ) ~~ A )
4 0ex 
 |-  (/) e. _V
5 en2sn 
 |-  ( ( (/) e. _V /\ A e. V ) -> { (/) } ~~ { A } )
6 4 5 mpan 
 |-  ( A e. V -> { (/) } ~~ { A } )
7 disjdifr 
 |-  ( ( A \ { (/) } ) i^i { (/) } ) = (/)
8 limord 
 |-  ( Lim A -> Ord A )
9 1 8 ax-mp 
 |-  Ord A
10 ordirr 
 |-  ( Ord A -> -. A e. A )
11 9 10 ax-mp 
 |-  -. A e. A
12 disjsn 
 |-  ( ( A i^i { A } ) = (/) <-> -. A e. A )
13 11 12 mpbir 
 |-  ( A i^i { A } ) = (/)
14 unen 
 |-  ( ( ( ( A \ { (/) } ) ~~ A /\ { (/) } ~~ { A } ) /\ ( ( ( A \ { (/) } ) i^i { (/) } ) = (/) /\ ( A i^i { A } ) = (/) ) ) -> ( ( A \ { (/) } ) u. { (/) } ) ~~ ( A u. { A } ) )
15 7 13 14 mpanr12 
 |-  ( ( ( A \ { (/) } ) ~~ A /\ { (/) } ~~ { A } ) -> ( ( A \ { (/) } ) u. { (/) } ) ~~ ( A u. { A } ) )
16 3 6 15 syl2anc 
 |-  ( A e. V -> ( ( A \ { (/) } ) u. { (/) } ) ~~ ( A u. { A } ) )
17 0ellim 
 |-  ( Lim A -> (/) e. A )
18 1 17 ax-mp 
 |-  (/) e. A
19 4 snss 
 |-  ( (/) e. A <-> { (/) } C_ A )
20 18 19 mpbi 
 |-  { (/) } C_ A
21 undif 
 |-  ( { (/) } C_ A <-> ( { (/) } u. ( A \ { (/) } ) ) = A )
22 20 21 mpbi 
 |-  ( { (/) } u. ( A \ { (/) } ) ) = A
23 uncom 
 |-  ( { (/) } u. ( A \ { (/) } ) ) = ( ( A \ { (/) } ) u. { (/) } )
24 22 23 eqtr3i 
 |-  A = ( ( A \ { (/) } ) u. { (/) } )
25 df-suc 
 |-  suc A = ( A u. { A } )
26 16 24 25 3brtr4g 
 |-  ( A e. V -> A ~~ suc A )