oacl

Description: Closure law for ordinal addition. Proposition 8.2 of TakeutiZaring p. 57. Remark 2.8 of Schloeder p. 5. (Contributed by NM, 5-May-1995)

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

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ x = \emptyset \to A +_{𝑜} x = A +_{𝑜} \emptyset$
2	1	eleq1d	$⊢ x = \emptyset \to (A +_{𝑜} x \in On \leftrightarrow A +_{𝑜} \emptyset \in On)$
3		oveq2	$⊢ x = y \to A +_{𝑜} x = A +_{𝑜} y$
4	3	eleq1d	$⊢ x = y \to (A +_{𝑜} x \in On \leftrightarrow A +_{𝑜} y \in On)$
5		oveq2	$⊢ x = suc y \to A +_{𝑜} x = A +_{𝑜} suc y$
6	5	eleq1d	$⊢ x = suc y \to (A +_{𝑜} x \in On \leftrightarrow A +_{𝑜} suc y \in On)$
7		oveq2	$⊢ x = B \to A +_{𝑜} x = A +_{𝑜} B$
8	7	eleq1d	$⊢ x = B \to (A +_{𝑜} x \in On \leftrightarrow A +_{𝑜} B \in On)$
9		oa0	$⊢ A \in On \to A +_{𝑜} \emptyset = A$
10	9	eleq1d	$⊢ A \in On \to (A +_{𝑜} \emptyset \in On \leftrightarrow A \in On)$
11	10	ibir	$⊢ A \in On \to A +_{𝑜} \emptyset \in On$
12		onsuc	$⊢ A +_{𝑜} y \in On \to suc (A +_{𝑜} y) \in On$
13		oasuc	$⊢ (A \in On \land y \in On) \to A +_{𝑜} suc y = suc (A +_{𝑜} y)$
14	13	eleq1d	$⊢ (A \in On \land y \in On) \to (A +_{𝑜} suc y \in On \leftrightarrow suc (A +_{𝑜} y) \in On)$
15	12 14	imbitrrid	$⊢ (A \in On \land y \in On) \to (A +_{𝑜} y \in On \to A +_{𝑜} suc y \in On)$
16	15	expcom	$⊢ y \in On \to (A \in On \to (A +_{𝑜} y \in On \to A +_{𝑜} suc y \in On))$
17		vex	$⊢ x \in V$
18		iunon	$⊢ (x \in V \land \forall y \in x A +_{𝑜} y \in On) \to ⋃_{y \in x} (A +_{𝑜} y) \in On$
19	17 18	mpan	$⊢ \forall y \in x A +_{𝑜} y \in On \to ⋃_{y \in x} (A +_{𝑜} y) \in On$
20		oalim	$⊢ (A \in On \land (x \in V \land Lim x)) \to A +_{𝑜} x = ⋃_{y \in x} (A +_{𝑜} y)$
21	17 20	mpanr1	$⊢ (A \in On \land Lim x) \to A +_{𝑜} x = ⋃_{y \in x} (A +_{𝑜} y)$
22	21	eleq1d	$⊢ (A \in On \land Lim x) \to (A +_{𝑜} x \in On \leftrightarrow ⋃_{y \in x} (A +_{𝑜} y) \in On)$
23	19 22	imbitrrid	$⊢ (A \in On \land Lim x) \to (\forall y \in x A +_{𝑜} y \in On \to A +_{𝑜} x \in On)$
24	23	expcom	$⊢ Lim x \to (A \in On \to (\forall y \in x A +_{𝑜} y \in On \to A +_{𝑜} x \in On))$
25	2 4 6 8 11 16 24	tfinds3	$⊢ B \in On \to (A \in On \to A +_{𝑜} B \in On)$
26	25	impcom	$⊢ (A \in On \land B \in On) \to A +_{𝑜} B \in On$

Metamath Proof Explorer

Theorem oacl

Proof