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 ∈ On ∧ B ∈ On → A + 𝑜 B ∈ ω ↔ A ∈ ω ∧ B ∈ ω

Proof

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