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 \in On \land B \in On) \to (A +_{𝑜} B \in ω \leftrightarrow (A \in ω \land B \in ω))$

Proof

Step	Hyp	Ref	Expression
1		oaword1	$⊢ (A \in On \land B \in On) \to A \subseteq A +_{𝑜} B$
2		eloni	$⊢ A \in On \to Ord A$
3		ordom	$⊢ Ord ω$
4		ordtr2	$⊢ (Ord A \land Ord ω) \to ((A \subseteq A +_{𝑜} B \land A +_{𝑜} B \in ω) \to A \in ω)$
5	2 3 4	sylancl	$⊢ A \in On \to ((A \subseteq A +_{𝑜} B \land A +_{𝑜} B \in ω) \to A \in ω)$
6	5	expd	$⊢ A \in On \to (A \subseteq A +_{𝑜} B \to (A +_{𝑜} B \in ω \to A \in ω))$
7	6	adantr	$⊢ (A \in On \land B \in On) \to (A \subseteq A +_{𝑜} B \to (A +_{𝑜} B \in ω \to A \in ω))$
8	1 7	mpd	$⊢ (A \in On \land B \in On) \to (A +_{𝑜} B \in ω \to A \in ω)$
9		oaword2	$⊢ (B \in On \land A \in On) \to B \subseteq A +_{𝑜} B$
10	9	ancoms	$⊢ (A \in On \land B \in On) \to B \subseteq A +_{𝑜} B$
11		eloni	$⊢ B \in On \to Ord B$
12		ordtr2	$⊢ (Ord B \land Ord ω) \to ((B \subseteq A +_{𝑜} B \land A +_{𝑜} B \in ω) \to B \in ω)$
13	11 3 12	sylancl	$⊢ B \in On \to ((B \subseteq A +_{𝑜} B \land A +_{𝑜} B \in ω) \to B \in ω)$
14	13	expd	$⊢ B \in On \to (B \subseteq A +_{𝑜} B \to (A +_{𝑜} B \in ω \to B \in ω))$
15	14	adantl	$⊢ (A \in On \land B \in On) \to (B \subseteq A +_{𝑜} B \to (A +_{𝑜} B \in ω \to B \in ω))$
16	10 15	mpd	$⊢ (A \in On \land B \in On) \to (A +_{𝑜} B \in ω \to B \in ω)$
17	8 16	jcad	$⊢ (A \in On \land B \in On) \to (A +_{𝑜} B \in ω \to (A \in ω \land B \in ω))$
18		nnacl	$⊢ (A \in ω \land B \in ω) \to A +_{𝑜} B \in ω$
19	17 18	impbid1	$⊢ (A \in On \land B \in On) \to (A +_{𝑜} B \in ω \leftrightarrow (A \in ω \land B \in ω))$