Description: A class is an ordinal number if and only if its successor is an ordinal number. Biconditional form of onsuc . (Contributed by NM, 9-Sep-2003)
Ref | Expression | ||
---|---|---|---|
Assertion | onsucb | |- ( A e. On <-> suc A e. On ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ordsuc | |- ( Ord A <-> Ord suc A ) |
|
2 | sucexb | |- ( A e. _V <-> suc A e. _V ) |
|
3 | 1 2 | anbi12i | |- ( ( Ord A /\ A e. _V ) <-> ( Ord suc A /\ suc A e. _V ) ) |
4 | elon2 | |- ( A e. On <-> ( Ord A /\ A e. _V ) ) |
|
5 | elon2 | |- ( suc A e. On <-> ( Ord suc A /\ suc A e. _V ) ) |
|
6 | 3 4 5 | 3bitr4i | |- ( A e. On <-> suc A e. On ) |