Definition df-ce 6107

Description: Define cardinal exponentiation. Definition from [Rosser] p. 381. (Contributed by Scott Fenton, 24-Feb-2015.)

Assertion

Ref	Expression
df-ce	⊢ ↑c = (n ∈ NC , m ∈ NC ↦ {g ∣ ∃a∃b(℘1a ∈ n ∧ ℘1b ∈ m ∧ g ≈ (a ↑m b))})

Distinct variable group:   m,n,g,a,b

Detailed syntax breakdown of Definition df-ce

Step	Hyp	Ref	Expression
1		cce 6097	. 2 class ↑c
2		vn	. . 3 setvar n
3		vm	. . 3 setvar m
4		cncs 6089	. . 3 class NC
5		va	. . . . . . . . . 10 setvar a
6	5	cv 1641	. . . . . . . . 9 class a
7	6	cpw1 4136	. . . . . . . 8 class ℘1a
8	2	cv 1641	. . . . . . . 8 class n
9	7, 8	wcel 1710	. . . . . . 7 wff ℘1a ∈ n
10		vb	. . . . . . . . . 10 setvar b
11	10	cv 1641	. . . . . . . . 9 class b
12	11	cpw1 4136	. . . . . . . 8 class ℘1b
13	3	cv 1641	. . . . . . . 8 class m
14	12, 13	wcel 1710	. . . . . . 7 wff ℘1b ∈ m
15		vg	. . . . . . . . 9 setvar g
16	15	cv 1641	. . . . . . . 8 class g
17		cmap 6000	. . . . . . . . 9 class ↑m
18	6, 11, 17	co 5526	. . . . . . . 8 class (a ↑m b)
19		cen 6029	. . . . . . . 8 class ≈
20	16, 18, 19	wbr 4640	. . . . . . 7 wff g ≈ (a ↑m b)
21	9, 14, 20	w3a 934	. . . . . 6 wff (℘1a ∈ n ∧ ℘1b ∈ m ∧ g ≈ (a ↑m b))
22	21, 10	wex 1541	. . . . 5 wff ∃b(℘1a ∈ n ∧ ℘1b ∈ m ∧ g ≈ (a ↑m b))
23	22, 5	wex 1541	. . . 4 wff ∃a∃b(℘1a ∈ n ∧ ℘1b ∈ m ∧ g ≈ (a ↑m b))
24	23, 15	cab 2339	. . 3 class {g ∣ ∃a∃b(℘1a ∈ n ∧ ℘1b ∈ m ∧ g ≈ (a ↑m b))}
25	2, 3, 4, 4, 24	cmpt2 5654	. 2 class (n ∈ NC , m ∈ NC ↦ {g ∣ ∃a∃b(℘1a ∈ n ∧ ℘1b ∈ m ∧ g ≈ (a ↑m b))})
26	1, 25	wceq 1642	1 wff ↑c = (n ∈ NC , m ∈ NC ↦ {g ∣ ∃a∃b(℘1a ∈ n ∧ ℘1b ∈ m ∧ g ≈ (a ↑m b))})

This definition is used by:  ovce  6173  ceex  6175  fnce  6177