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

Metamath Proof Explorer

Theorem nnarcl

Description: Reverse closure law for addition of natural numbers. Exercise 1 of TakeutiZaring p. 62 and its converse. (Contributed by NM, 12-Dec-2004)

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

Proof

Step Hyp Ref Expression
1 oaword1 
 |-  ( ( A e. On /\ B e. On ) -> A C_ ( A +o B ) )
2 eloni 
 |-  ( A e. On -> Ord A )
3 ordom 
 |-  Ord _om
4 ordtr2 
 |-  ( ( Ord A /\ Ord _om ) -> ( ( A C_ ( A +o B ) /\ ( A +o B ) e. _om ) -> A e. _om ) )
5 2 3 4 sylancl 
 |-  ( A e. On -> ( ( A C_ ( A +o B ) /\ ( A +o B ) e. _om ) -> A e. _om ) )
6 5 expd 
 |-  ( A e. On -> ( A C_ ( A +o B ) -> ( ( A +o B ) e. _om -> A e. _om ) ) )
7 6 adantr 
 |-  ( ( A e. On /\ B e. On ) -> ( A C_ ( A +o B ) -> ( ( A +o B ) e. _om -> A e. _om ) ) )
8 1 7 mpd 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A +o B ) e. _om -> A e. _om ) )
9 oaword2 
 |-  ( ( B e. On /\ A e. On ) -> B C_ ( A +o B ) )
10 9 ancoms 
 |-  ( ( A e. On /\ B e. On ) -> B C_ ( A +o B ) )
11 eloni 
 |-  ( B e. On -> Ord B )
12 ordtr2 
 |-  ( ( Ord B /\ Ord _om ) -> ( ( B C_ ( A +o B ) /\ ( A +o B ) e. _om ) -> B e. _om ) )
13 11 3 12 sylancl 
 |-  ( B e. On -> ( ( B C_ ( A +o B ) /\ ( A +o B ) e. _om ) -> B e. _om ) )
14 13 expd 
 |-  ( B e. On -> ( B C_ ( A +o B ) -> ( ( A +o B ) e. _om -> B e. _om ) ) )
15 14 adantl 
 |-  ( ( A e. On /\ B e. On ) -> ( B C_ ( A +o B ) -> ( ( A +o B ) e. _om -> B e. _om ) ) )
16 10 15 mpd 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A +o B ) e. _om -> B e. _om ) )
17 8 16 jcad 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A +o B ) e. _om -> ( A e. _om /\ B e. _om ) ) )
18 nnacl 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A +o B ) e. _om )
19 17 18 impbid1 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A +o B ) e. _om <-> ( A e. _om /\ B e. _om ) ) )