This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oaord1

Description: An ordinal is less than its sum with a nonzero ordinal. Theorem 18 of Suppes p. 209 and its converse. (Contributed by NM, 6-Dec-2004)

Ref Expression
Assertion oaord1 
|- ( ( A e. On /\ B e. On ) -> ( (/) e. B <-> A e. ( A +o B ) ) )

Proof

Step Hyp Ref Expression
1 0elon 
 |-  (/) e. On
2 oaord 
 |-  ( ( (/) e. On /\ B e. On /\ A e. On ) -> ( (/) e. B <-> ( A +o (/) ) e. ( A +o B ) ) )
3 1 2 mp3an1 
 |-  ( ( B e. On /\ A e. On ) -> ( (/) e. B <-> ( A +o (/) ) e. ( A +o B ) ) )
4 oa0 
 |-  ( A e. On -> ( A +o (/) ) = A )
5 4 adantl 
 |-  ( ( B e. On /\ A e. On ) -> ( A +o (/) ) = A )
6 5 eleq1d 
 |-  ( ( B e. On /\ A e. On ) -> ( ( A +o (/) ) e. ( A +o B ) <-> A e. ( A +o B ) ) )
7 3 6 bitrd 
 |-  ( ( B e. On /\ A e. On ) -> ( (/) e. B <-> A e. ( A +o B ) ) )
8 7 ancoms 
 |-  ( ( A e. On /\ B e. On ) -> ( (/) e. B <-> A e. ( A +o B ) ) )