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	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 +o 𝐵 ) ∈ ω ↔ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) )

Proof

Step	Hyp	Ref	Expression
1		oaword1	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐴 ⊆ ( 𝐴 +o 𝐵 ) )
2		eloni	⊢ ( 𝐴 ∈ On → Ord 𝐴 )
3		ordom	⊢ Ord ω
4		ordtr2	⊢ ( ( Ord 𝐴 ∧ Ord ω ) → ( ( 𝐴 ⊆ ( 𝐴 +o 𝐵 ) ∧ ( 𝐴 +o 𝐵 ) ∈ ω ) → 𝐴 ∈ ω ) )
5	2 3 4	sylancl	⊢ ( 𝐴 ∈ On → ( ( 𝐴 ⊆ ( 𝐴 +o 𝐵 ) ∧ ( 𝐴 +o 𝐵 ) ∈ ω ) → 𝐴 ∈ ω ) )
6	5	expd	⊢ ( 𝐴 ∈ On → ( 𝐴 ⊆ ( 𝐴 +o 𝐵 ) → ( ( 𝐴 +o 𝐵 ) ∈ ω → 𝐴 ∈ ω ) ) )
7	6	adantr	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ ( 𝐴 +o 𝐵 ) → ( ( 𝐴 +o 𝐵 ) ∈ ω → 𝐴 ∈ ω ) ) )
8	1 7	mpd	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 +o 𝐵 ) ∈ ω → 𝐴 ∈ ω ) )
9		oaword2	⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → 𝐵 ⊆ ( 𝐴 +o 𝐵 ) )
10	9	ancoms	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐵 ⊆ ( 𝐴 +o 𝐵 ) )
11		eloni	⊢ ( 𝐵 ∈ On → Ord 𝐵 )
12		ordtr2	⊢ ( ( Ord 𝐵 ∧ Ord ω ) → ( ( 𝐵 ⊆ ( 𝐴 +o 𝐵 ) ∧ ( 𝐴 +o 𝐵 ) ∈ ω ) → 𝐵 ∈ ω ) )
13	11 3 12	sylancl	⊢ ( 𝐵 ∈ On → ( ( 𝐵 ⊆ ( 𝐴 +o 𝐵 ) ∧ ( 𝐴 +o 𝐵 ) ∈ ω ) → 𝐵 ∈ ω ) )
14	13	expd	⊢ ( 𝐵 ∈ On → ( 𝐵 ⊆ ( 𝐴 +o 𝐵 ) → ( ( 𝐴 +o 𝐵 ) ∈ ω → 𝐵 ∈ ω ) ) )
15	14	adantl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐵 ⊆ ( 𝐴 +o 𝐵 ) → ( ( 𝐴 +o 𝐵 ) ∈ ω → 𝐵 ∈ ω ) ) )
16	10 15	mpd	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 +o 𝐵 ) ∈ ω → 𝐵 ∈ ω ) )
17	8 16	jcad	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 +o 𝐵 ) ∈ ω → ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) )
18		nnacl	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 +o 𝐵 ) ∈ ω )
19	17 18	impbid1	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 +o 𝐵 ) ∈ ω ↔ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) )