df-oexp

Description: Define the ordinal exponentiation operation. (Contributed by NM, 30-Dec-2004)

		Ref	Expression
	Assertion	df-oexp	$⊢ ↑_{𝑜} = (x \in On, y \in On ⟼ if (x = \emptyset, 1_{𝑜} ∖ y, rec ((z \in V ⟼ z \cdot_{𝑜} x), 1_{𝑜}) (y)))$

Step	Hyp	Ref	Expression
0		coe	$class ↑_{𝑜}$
1		vx	$setvar x$
2		con0	$class On$
3		vy	$setvar y$
4	1	cv	$setvar x$
5		c0	$class \emptyset$
6	4 5	wceq	$wff x = \emptyset$
7		c1o	$class 1_{𝑜}$
8	3	cv	$setvar y$
9	7 8	cdif	$class (1_{𝑜} ∖ y)$
10		vz	$setvar z$
11		cvv	$class V$
12	10	cv	$setvar z$
13		comu	$class \cdot_{𝑜}$
14	12 4 13	co	$class (z \cdot_{𝑜} x)$
15	10 11 14	cmpt	$class (z \in V ⟼ z \cdot_{𝑜} x)$
16	15 7	crdg	$class rec ((z \in V ⟼ z \cdot_{𝑜} x), 1_{𝑜})$
17	8 16	cfv	$class rec ((z \in V ⟼ z \cdot_{𝑜} x), 1_{𝑜}) (y)$
18	6 9 17	cif	$class if (x = \emptyset, 1_{𝑜} ∖ y, rec ((z \in V ⟼ z \cdot_{𝑜} x), 1_{𝑜}) (y))$
19	1 3 2 2 18	cmpo	$class (x \in On, y \in On ⟼ if (x = \emptyset, 1_{𝑜} ∖ y, rec ((z \in V ⟼ z \cdot_{𝑜} x), 1_{𝑜}) (y)))$
20	0 19	wceq	$wff ↑_{𝑜} = (x \in On, y \in On ⟼ if (x = \emptyset, 1_{𝑜} ∖ y, rec ((z \in V ⟼ z \cdot_{𝑜} x), 1_{𝑜}) (y)))$

Metamath Proof Explorer