Definition df-oexp 3108

Description: Define the ordinal exponentiation operation.

Assertion

Ref	Expression
df-oexp	⊢ ↑o = {⟨⟨x, y⟩, z⟩∣((x ∈ On ∧ y ∈ On) ∧ z = if(x = ∅, (1o ∖ y), (rec({⟨w, v⟩∣v = (w ·o x)}, 1o) ‘y)))}

Distinct variable group(s):   x,y,z,w,v

Detailed syntax breakdown of Definition df-oexp

Step	Hyp	Ref	Expression
1		coe 3103	. 2 class ↑o
2		vx	. . . . . . 7 set x
3	2	cv 1089	. . . . . 6 class x
4		con0 2199	. . . . . 6 class On
5	3, 4	wcel 1092	. . . . 5 wff x ∈ On
6		vy	. . . . . . 7 set y
7	6	cv 1089	. . . . . 6 class y
8	7, 4	wcel 1092	. . . . 5 wff y ∈ On
9	5, 8	wa 196	. . . 4 wff (x ∈ On ∧ y ∈ On)
10		vz	. . . . . 6 set z
11	10	cv 1089	. . . . 5 class z
12		c0 1707	. . . . . . 7 class ∅
13	3, 12	wceq 1091	. . . . . 6 wff x = ∅
14		c1o 3099	. . . . . . 7 class 1o
15	14, 7	cdif 1484	. . . . . 6 class (1o ∖ y)
16		vv	. . . . . . . . . . 11 set v
17	16	cv 1089	. . . . . . . . . 10 class v
18		vw	. . . . . . . . . . . 12 set w
19	18	cv 1089	. . . . . . . . . . 11 class w
20		comu 3102	. . . . . . . . . . 11 class ·o
21	19, 3, 20	co 3001	. . . . . . . . . 10 class (w ·o x)
22	17, 21	wceq 1091	. . . . . . . . 9 wff v = (w ·o x)
23	22, 18, 16	copab 2055	. . . . . . . 8 class {⟨w, v⟩∣v = (w ·o x)}
24	23, 14	crdg 2969	. . . . . . 7 class rec({⟨w, v⟩∣v = (w ·o x)}, 1o)
25	7, 24	cfv 2422	. . . . . 6 class (rec({⟨w, v⟩∣v = (w ·o x)}, 1o) ‘y)
26	13, 15, 25	cif 1776	. . . . 5 class if(x = ∅, (1o ∖ y), (rec({⟨w, v⟩∣v = (w ·o x)}, 1o) ‘y))
27	11, 26	wceq 1091	. . . 4 wff z = if(x = ∅, (1o ∖ y), (rec({⟨w, v⟩∣v = (w ·o x)}, 1o) ‘y))
28	9, 27	wa 196	. . 3 wff ((x ∈ On ∧ y ∈ On) ∧ z = if(x = ∅, (1o ∖ y), (rec({⟨w, v⟩∣v = (w ·o x)}, 1o) ‘y)))
29	28, 2, 6, 10	copab2 3002	. 2 class {⟨⟨x, y⟩, z⟩∣((x ∈ On ∧ y ∈ On) ∧ z = if(x = ∅, (1o ∖ y), (rec({⟨w, v⟩∣v = (w ·o x)}, 1o) ‘y)))}
30	1, 29	wceq 1091	1 wff ↑o = {⟨⟨x, y⟩, z⟩∣((x ∈ On ∧ y ∈ On) ∧ z = if(x = ∅, (1o ∖ y), (rec({⟨w, v⟩∣v = (w ·o x)}, 1o) ‘y)))}

This definition is referenced by:  oev 3122

metamath.org