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 ( ( 𝐴 ∈ 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 𝐵 ) ∈ ω ↔ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) )