nnecl

Description: Closure of exponentiation of natural numbers. Proposition 8.17 of TakeutiZaring p. 63. Theorem 2.20 of Schloeder p. 6. (Contributed by NM, 24-Mar-2007) (Proof shortened by Andrew Salmon, 22-Oct-2011)

		Ref	Expression
	Assertion	nnecl	$⊢ (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		nnon	$⊢ A \in ω \to A \in On$
11		oe0	$⊢ A \in On \to A ↑_{𝑜} \emptyset = 1_{𝑜}$
12	10 11	syl	$⊢ A \in ω \to A ↑_{𝑜} \emptyset = 1_{𝑜}$
13		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
14		peano1	$⊢ \emptyset \in ω$
15		peano2	$⊢ \emptyset \in ω \to suc \emptyset \in ω$
16	14 15	ax-mp	$⊢ suc \emptyset \in ω$
17	13 16	eqeltri	$⊢ 1_{𝑜} \in ω$
18	12 17	eqeltrdi	$⊢ A \in ω \to A ↑_{𝑜} \emptyset \in ω$
19		nnmcl	$⊢ (A ↑_{𝑜} y \in ω \land A \in ω) \to (A ↑_{𝑜} y) \cdot_{𝑜} A \in ω$
20	19	expcom	$⊢ A \in ω \to (A ↑_{𝑜} y \in ω \to (A ↑_{𝑜} y) \cdot_{𝑜} A \in ω)$
21	20	adantr	$⊢ (A \in ω \land y \in ω) \to (A ↑_{𝑜} y \in ω \to (A ↑_{𝑜} y) \cdot_{𝑜} A \in ω)$
22		nnesuc	$⊢ (A \in ω \land y \in ω) \to A ↑_{𝑜} suc y = (A ↑_{𝑜} y) \cdot_{𝑜} A$
23	22	eleq1d	$⊢ (A \in ω \land y \in ω) \to (A ↑_{𝑜} suc y \in ω \leftrightarrow (A ↑_{𝑜} y) \cdot_{𝑜} A \in ω)$
24	21 23	sylibrd	$⊢ (A \in ω \land y \in ω) \to (A ↑_{𝑜} y \in ω \to A ↑_{𝑜} suc y \in ω)$
25	24	expcom	$⊢ y \in ω \to (A \in ω \to (A ↑_{𝑜} y \in ω \to A ↑_{𝑜} suc y \in ω))$
26	5 7 9 18 25	finds2	$⊢ x \in ω \to (A \in ω \to A ↑_{𝑜} x \in ω)$
27	3 26	vtoclga	$⊢ B \in ω \to (A \in ω \to A ↑_{𝑜} B \in ω)$
28	27	impcom	$⊢ (A \in ω \land B \in ω) \to A ↑_{𝑜} B \in ω$

Metamath Proof Explorer

Theorem nnecl

Proof