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 ) ) )