Metamath Proof Explorer

Theorem oalim

Description: Ordinal addition with a limit ordinal. Definition 8.1 of TakeutiZaring p. 56. (Contributed by NM, 3-Aug-2004) (Revised by Mario Carneiro, 8-Sep-2013)

		Ref	Expression
	Assertion	oalim	$⊢ (A \in On \land (B \in C \land Lim B)) \to A +_{𝑜} B = ⋃_{x \in B} (A +_{𝑜} x)$

Proof

Step	Hyp	Ref	Expression
1		limelon	$⊢ (B \in C \land Lim B) \to B \in On$
2		simpr	$⊢ (B \in C \land Lim B) \to Lim B$
3	1 2	jca	$⊢ (B \in C \land Lim B) \to (B \in On \land Lim B)$
4		rdglim2a	$⊢ (B \in On \land Lim B) \to rec ((y \in V ⟼ suc y), A) (B) = ⋃_{x \in B} rec ((y \in V ⟼ suc y), A) (x)$
5	4	adantl	$⊢ (A \in On \land (B \in On \land Lim B)) \to rec ((y \in V ⟼ suc y), A) (B) = ⋃_{x \in B} rec ((y \in V ⟼ suc y), A) (x)$
6		oav	$⊢ (A \in On \land B \in On) \to A +_{𝑜} B = rec ((y \in V ⟼ suc y), A) (B)$
7		onelon	$⊢ (B \in On \land x \in B) \to x \in On$
8		oav	$⊢ (A \in On \land x \in On) \to A +_{𝑜} x = rec ((y \in V ⟼ suc y), A) (x)$
9	7 8	sylan2	$⊢ (A \in On \land (B \in On \land x \in B)) \to A +_{𝑜} x = rec ((y \in V ⟼ suc y), A) (x)$
10	9	anassrs	$⊢ ((A \in On \land B \in On) \land x \in B) \to A +_{𝑜} x = rec ((y \in V ⟼ suc y), A) (x)$
11	10	iuneq2dv	$⊢ (A \in On \land B \in On) \to ⋃_{x \in B} (A +_{𝑜} x) = ⋃_{x \in B} rec ((y \in V ⟼ suc y), A) (x)$
12	6 11	eqeq12d	$⊢ (A \in On \land B \in On) \to (A +_{𝑜} B = ⋃_{x \in B} (A +_{𝑜} x) \leftrightarrow rec ((y \in V ⟼ suc y), A) (B) = ⋃_{x \in B} rec ((y \in V ⟼ suc y), A) (x))$
13	12	adantrr	$⊢ (A \in On \land (B \in On \land Lim B)) \to (A +_{𝑜} B = ⋃_{x \in B} (A +_{𝑜} x) \leftrightarrow rec ((y \in V ⟼ suc y), A) (B) = ⋃_{x \in B} rec ((y \in V ⟼ suc y), A) (x))$
14	5 13	mpbird	$⊢ (A \in On \land (B \in On \land Lim B)) \to A +_{𝑜} B = ⋃_{x \in B} (A +_{𝑜} x)$
15	3 14	sylan2	$⊢ (A \in On \land (B \in C \land Lim B)) \to A +_{𝑜} B = ⋃_{x \in B} (A +_{𝑜} x)$