Theorem ordsssuc2

Description: An ordinal subset of an ordinal number belongs to its successor. (Contributed by NM, 1-Feb-2005) (Proof shortened by Andrew Salmon, 12-Aug-2011)

	Ref	Expression
Assertion	ordsssuc2	|- ( ( Ord A /\ B e. On ) -> ( A C_ B <-> A e. suc B ) )

Proof

Step	Hyp	Ref	Expression
1		elong	|- ( A e. _V -> ( A e. On <-> Ord A ) )
2	1	biimprd	|- ( A e. _V -> ( Ord A -> A e. On ) )
3	2	anim1d	|- ( A e. _V -> ( ( Ord A /\ B e. On ) -> ( A e. On /\ B e. On ) ) )
4		onsssuc	|- ( ( A e. On /\ B e. On ) -> ( A C_ B <-> A e. suc B ) )
5	3 4	syl6	|- ( A e. _V -> ( ( Ord A /\ B e. On ) -> ( A C_ B <-> A e. suc B ) ) )
6		annim	|- ( ( B e. On /\ -. A e. _V ) <-> -. ( B e. On -> A e. _V ) )
7		ssexg	|- ( ( A C_ B /\ B e. On ) -> A e. _V )
8	7	ex	|- ( A C_ B -> ( B e. On -> A e. _V ) )
9		elex	|- ( A e. suc B -> A e. _V )
10	9	a1d	|- ( A e. suc B -> ( B e. On -> A e. _V ) )
11	8 10	pm5.21ni	|- ( -. ( B e. On -> A e. _V ) -> ( A C_ B <-> A e. suc B ) )
12	6 11	sylbi	|- ( ( B e. On /\ -. A e. _V ) -> ( A C_ B <-> A e. suc B ) )
13	12	expcom	|- ( -. A e. _V -> ( B e. On -> ( A C_ B <-> A e. suc B ) ) )
14	13	adantld	|- ( -. A e. _V -> ( ( Ord A /\ B e. On ) -> ( A C_ B <-> A e. suc B ) ) )
15	5 14	pm2.61i	|- ( ( Ord A /\ B e. On ) -> ( A C_ B <-> A e. suc B ) )