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