nnacl

Description: Closure of addition of natural numbers. Proposition 8.9 of TakeutiZaring p. 59. Theorem 2.20 of Schloeder p. 6. (Contributed by NM, 20-Sep-1995) (Proof shortened by Andrew Salmon, 22-Oct-2011)

		Ref	Expression
	Assertion	nnacl	$⊢ (A \in ω \land B \in ω) \to A +_{𝑜} B \in ω$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ x = B \to A +_{𝑜} x = A +_{𝑜} B$
2	1	eleq1d	$⊢ x = B \to (A +_{𝑜} x \in ω \leftrightarrow A +_{𝑜} B \in ω)$
3	2	imbi2d	$⊢ x = B \to ((A \in ω \to A +_{𝑜} x \in ω) \leftrightarrow (A \in ω \to A +_{𝑜} B \in ω))$
4		oveq2	$⊢ x = \emptyset \to A +_{𝑜} x = A +_{𝑜} \emptyset$
5	4	eleq1d	$⊢ x = \emptyset \to (A +_{𝑜} x \in ω \leftrightarrow A +_{𝑜} \emptyset \in ω)$
6		oveq2	$⊢ x = y \to A +_{𝑜} x = A +_{𝑜} y$
7	6	eleq1d	$⊢ x = y \to (A +_{𝑜} x \in ω \leftrightarrow A +_{𝑜} y \in ω)$
8		oveq2	$⊢ x = suc y \to A +_{𝑜} x = A +_{𝑜} suc y$
9	8	eleq1d	$⊢ x = suc y \to (A +_{𝑜} x \in ω \leftrightarrow A +_{𝑜} suc y \in ω)$
10		nna0	$⊢ A \in ω \to A +_{𝑜} \emptyset = A$
11	10	eleq1d	$⊢ A \in ω \to (A +_{𝑜} \emptyset \in ω \leftrightarrow A \in ω)$
12	11	ibir	$⊢ A \in ω \to A +_{𝑜} \emptyset \in ω$
13		peano2	$⊢ A +_{𝑜} y \in ω \to suc (A +_{𝑜} y) \in ω$
14		nnasuc	$⊢ (A \in ω \land y \in ω) \to A +_{𝑜} suc y = suc (A +_{𝑜} y)$
15	14	eleq1d	$⊢ (A \in ω \land y \in ω) \to (A +_{𝑜} suc y \in ω \leftrightarrow suc (A +_{𝑜} y) \in ω)$
16	13 15	imbitrrid	$⊢ (A \in ω \land y \in ω) \to (A +_{𝑜} y \in ω \to A +_{𝑜} suc y \in ω)$
17	16	expcom	$⊢ y \in ω \to (A \in ω \to (A +_{𝑜} y \in ω \to A +_{𝑜} suc y \in ω))$
18	5 7 9 12 17	finds2	$⊢ x \in ω \to (A \in ω \to A +_{𝑜} x \in ω)$
19	3 18	vtoclga	$⊢ B \in ω \to (A \in ω \to A +_{𝑜} B \in ω)$
20	19	impcom	$⊢ (A \in ω \land B \in ω) \to A +_{𝑜} B \in ω$

Metamath Proof Explorer

Theorem nnacl

Proof