Metamath Proof Explorer

Theorem omlim

Description: Ordinal multiplication with a limit ordinal. Definition 8.15 of TakeutiZaring p. 62. Definition 2.5 of Schloeder p. 4. (Contributed by NM, 3-Aug-2004) (Revised by Mario Carneiro, 8-Sep-2013)

		Ref	Expression
	Assertion	omlim	$⊢ (A \in On \land (B \in C \land Lim B)) \to A \cdot_{𝑜} B = ⋃_{x \in B} (A \cdot_{𝑜} 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 ⟼ y +_{𝑜} A), \emptyset) (B) = ⋃_{x \in B} rec ((y \in V ⟼ y +_{𝑜} A), \emptyset) (x)$
5	4	adantl	$⊢ (A \in On \land (B \in On \land Lim B)) \to rec ((y \in V ⟼ y +_{𝑜} A), \emptyset) (B) = ⋃_{x \in B} rec ((y \in V ⟼ y +_{𝑜} A), \emptyset) (x)$
6		omv	$⊢ (A \in On \land B \in On) \to A \cdot_{𝑜} B = rec ((y \in V ⟼ y +_{𝑜} A), \emptyset) (B)$
7		onelon	$⊢ (B \in On \land x \in B) \to x \in On$
8		omv	$⊢ (A \in On \land x \in On) \to A \cdot_{𝑜} x = rec ((y \in V ⟼ y +_{𝑜} A), \emptyset) (x)$
9	7 8	sylan2	$⊢ (A \in On \land (B \in On \land x \in B)) \to A \cdot_{𝑜} x = rec ((y \in V ⟼ y +_{𝑜} A), \emptyset) (x)$
10	9	anassrs	$⊢ ((A \in On \land B \in On) \land x \in B) \to A \cdot_{𝑜} x = rec ((y \in V ⟼ y +_{𝑜} A), \emptyset) (x)$
11	10	iuneq2dv	$⊢ (A \in On \land B \in On) \to ⋃_{x \in B} (A \cdot_{𝑜} x) = ⋃_{x \in B} rec ((y \in V ⟼ y +_{𝑜} A), \emptyset) (x)$
12	6 11	eqeq12d	$⊢ (A \in On \land B \in On) \to (A \cdot_{𝑜} B = ⋃_{x \in B} (A \cdot_{𝑜} x) \leftrightarrow rec ((y \in V ⟼ y +_{𝑜} A), \emptyset) (B) = ⋃_{x \in B} rec ((y \in V ⟼ y +_{𝑜} A), \emptyset) (x))$
13	12	adantrr	$⊢ (A \in On \land (B \in On \land Lim B)) \to (A \cdot_{𝑜} B = ⋃_{x \in B} (A \cdot_{𝑜} x) \leftrightarrow rec ((y \in V ⟼ y +_{𝑜} A), \emptyset) (B) = ⋃_{x \in B} rec ((y \in V ⟼ y +_{𝑜} A), \emptyset) (x))$
14	5 13	mpbird	$⊢ (A \in On \land (B \in On \land Lim B)) \to A \cdot_{𝑜} B = ⋃_{x \in B} (A \cdot_{𝑜} x)$
15	3 14	sylan2	$⊢ (A \in On \land (B \in C \land Lim B)) \to A \cdot_{𝑜} B = ⋃_{x \in B} (A \cdot_{𝑜} x)$