Metamath Proof Explorer

Theorem oelim

Description: Ordinal exponentiation with a limit exponent and nonzero base. Definition 8.30 of TakeutiZaring p. 67. (Contributed by NM, 1-Jan-2005) (Revised by Mario Carneiro, 8-Sep-2013)

		Ref	Expression
	Assertion	oelim	$⊢ ((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \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 ⟼ y \cdot_{𝑜} A), 1_{𝑜}) (B) = ⋃_{x \in B} rec ((y \in V ⟼ y \cdot_{𝑜} A), 1_{𝑜}) (x)$
5	4	ad2antlr	$⊢ ((A \in On \land (B \in On \land Lim B)) \land \emptyset \in A) \to rec ((y \in V ⟼ y \cdot_{𝑜} A), 1_{𝑜}) (B) = ⋃_{x \in B} rec ((y \in V ⟼ y \cdot_{𝑜} A), 1_{𝑜}) (x)$
6		oevn0	$⊢ ((A \in On \land B \in On) \land \emptyset \in A) \to A ↑_{𝑜} B = rec ((y \in V ⟼ y \cdot_{𝑜} A), 1_{𝑜}) (B)$
7		onelon	$⊢ (B \in On \land x \in B) \to x \in On$
8		oevn0	$⊢ ((A \in On \land x \in On) \land \emptyset \in A) \to A ↑_{𝑜} x = rec ((y \in V ⟼ y \cdot_{𝑜} A), 1_{𝑜}) (x)$
9	7 8	sylanl2	$⊢ ((A \in On \land (B \in On \land x \in B)) \land \emptyset \in A) \to A ↑_{𝑜} x = rec ((y \in V ⟼ y \cdot_{𝑜} A), 1_{𝑜}) (x)$
10	9	exp42	$⊢ A \in On \to (B \in On \to (x \in B \to (\emptyset \in A \to A ↑_{𝑜} x = rec ((y \in V ⟼ y \cdot_{𝑜} A), 1_{𝑜}) (x))))$
11	10	com34	$⊢ A \in On \to (B \in On \to (\emptyset \in A \to (x \in B \to A ↑_{𝑜} x = rec ((y \in V ⟼ y \cdot_{𝑜} A), 1_{𝑜}) (x))))$
12	11	imp41	$⊢ (((A \in On \land B \in On) \land \emptyset \in A) \land x \in B) \to A ↑_{𝑜} x = rec ((y \in V ⟼ y \cdot_{𝑜} A), 1_{𝑜}) (x)$
13	12	iuneq2dv	$⊢ ((A \in On \land B \in On) \land \emptyset \in A) \to ⋃_{x \in B} (A ↑_{𝑜} x) = ⋃_{x \in B} rec ((y \in V ⟼ y \cdot_{𝑜} A), 1_{𝑜}) (x)$
14	6 13	eqeq12d	$⊢ ((A \in On \land B \in On) \land \emptyset \in A) \to (A ↑_{𝑜} B = ⋃_{x \in B} (A ↑_{𝑜} x) \leftrightarrow rec ((y \in V ⟼ y \cdot_{𝑜} A), 1_{𝑜}) (B) = ⋃_{x \in B} rec ((y \in V ⟼ y \cdot_{𝑜} A), 1_{𝑜}) (x))$
15	14	adantlrr	$⊢ ((A \in On \land (B \in On \land Lim B)) \land \emptyset \in A) \to (A ↑_{𝑜} B = ⋃_{x \in B} (A ↑_{𝑜} x) \leftrightarrow rec ((y \in V ⟼ y \cdot_{𝑜} A), 1_{𝑜}) (B) = ⋃_{x \in B} rec ((y \in V ⟼ y \cdot_{𝑜} A), 1_{𝑜}) (x))$
16	5 15	mpbird	$⊢ ((A \in On \land (B \in On \land Lim B)) \land \emptyset \in A) \to A ↑_{𝑜} B = ⋃_{x \in B} (A ↑_{𝑜} x)$
17	3 16	sylanl2	$⊢ ((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \to A ↑_{𝑜} B = ⋃_{x \in B} (A ↑_{𝑜} x)$