Metamath Proof Explorer


Theorem ordsssuc

Description: An ordinal is a subset of another ordinal if and only if it belongs to its successor. (Contributed by NM, 28-Nov-2003)

Ref Expression
Assertion ordsssuc AOnOrdBABAsucB

Proof

Step Hyp Ref Expression
1 eloni AOnOrdA
2 ordsseleq OrdAOrdBABABA=B
3 1 2 sylan AOnOrdBABABA=B
4 elsucg AOnAsucBABA=B
5 4 adantr AOnOrdBAsucBABA=B
6 3 5 bitr4d AOnOrdBABAsucB