Theorem ordelsuc

Description: A set belongs to an ordinal iff its successor is a subset of the ordinal. Exercise 8 of TakeutiZaring p. 42 and its converse. (Contributed by NM, 29-Nov-2003)

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

Proof

Step	Hyp	Ref	Expression
1		ordsucss	|- ( Ord B -> ( A e. B -> suc A C_ B ) )
2	1	adantl	|- ( ( A e. C /\ Ord B ) -> ( A e. B -> suc A C_ B ) )
3		sucssel	|- ( A e. C -> ( suc A C_ B -> A e. B ) )
4	3	adantr	|- ( ( A e. C /\ Ord B ) -> ( suc A C_ B -> A e. B ) )
5	2 4	impbid	|- ( ( A e. C /\ Ord B ) -> ( A e. B <-> suc A C_ B ) )