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

Metamath Proof Explorer

Theorem limsssuc

Description: A class includes a limit ordinal iff the successor of the class includes it. (Contributed by NM, 30-Oct-2003)

Ref Expression
Assertion limsssuc 
|- ( Lim A -> ( A C_ B <-> A C_ suc B ) )

Proof

Step Hyp Ref Expression
1 sssucid 
 |-  B C_ suc B
2 sstr2 
 |-  ( A C_ B -> ( B C_ suc B -> A C_ suc B ) )
3 1 2 mpi 
 |-  ( A C_ B -> A C_ suc B )
4 eleq1 
 |-  ( x = B -> ( x e. A <-> B e. A ) )
5 4 biimpcd 
 |-  ( x e. A -> ( x = B -> B e. A ) )
6 limsuc 
 |-  ( Lim A -> ( B e. A <-> suc B e. A ) )
7 6 biimpa 
 |-  ( ( Lim A /\ B e. A ) -> suc B e. A )
8 limord 
 |-  ( Lim A -> Ord A )
9 ordelord 
 |-  ( ( Ord A /\ B e. A ) -> Ord B )
10 8 9 sylan 
 |-  ( ( Lim A /\ B e. A ) -> Ord B )
11 ordsuc 
 |-  ( Ord B <-> Ord suc B )
12 10 11 sylib 
 |-  ( ( Lim A /\ B e. A ) -> Ord suc B )
13 ordtri1 
 |-  ( ( Ord A /\ Ord suc B ) -> ( A C_ suc B <-> -. suc B e. A ) )
14 8 12 13 syl2an2r 
 |-  ( ( Lim A /\ B e. A ) -> ( A C_ suc B <-> -. suc B e. A ) )
15 14 con2bid 
 |-  ( ( Lim A /\ B e. A ) -> ( suc B e. A <-> -. A C_ suc B ) )
16 7 15 mpbid 
 |-  ( ( Lim A /\ B e. A ) -> -. A C_ suc B )
17 16 ex 
 |-  ( Lim A -> ( B e. A -> -. A C_ suc B ) )
18 5 17 sylan9r 
 |-  ( ( Lim A /\ x e. A ) -> ( x = B -> -. A C_ suc B ) )
19 18 con2d 
 |-  ( ( Lim A /\ x e. A ) -> ( A C_ suc B -> -. x = B ) )
20 19 ex 
 |-  ( Lim A -> ( x e. A -> ( A C_ suc B -> -. x = B ) ) )
21 20 com23 
 |-  ( Lim A -> ( A C_ suc B -> ( x e. A -> -. x = B ) ) )
22 21 imp31 
 |-  ( ( ( Lim A /\ A C_ suc B ) /\ x e. A ) -> -. x = B )
23 ssel2 
 |-  ( ( A C_ suc B /\ x e. A ) -> x e. suc B )
24 vex 
 |-  x e. _V
25 24 elsuc 
 |-  ( x e. suc B <-> ( x e. B \/ x = B ) )
26 23 25 sylib 
 |-  ( ( A C_ suc B /\ x e. A ) -> ( x e. B \/ x = B ) )
27 26 ord 
 |-  ( ( A C_ suc B /\ x e. A ) -> ( -. x e. B -> x = B ) )
28 27 con1d 
 |-  ( ( A C_ suc B /\ x e. A ) -> ( -. x = B -> x e. B ) )
29 28 adantll 
 |-  ( ( ( Lim A /\ A C_ suc B ) /\ x e. A ) -> ( -. x = B -> x e. B ) )
30 22 29 mpd 
 |-  ( ( ( Lim A /\ A C_ suc B ) /\ x e. A ) -> x e. B )
31 30 ex 
 |-  ( ( Lim A /\ A C_ suc B ) -> ( x e. A -> x e. B ) )
32 31 ssrdv 
 |-  ( ( Lim A /\ A C_ suc B ) -> A C_ B )
33 32 ex 
 |-  ( Lim A -> ( A C_ suc B -> A C_ B ) )
34 3 33 impbid2 
 |-  ( Lim A -> ( A C_ B <-> A C_ suc B ) )