Definition df-finxp 34659

Description: Define Cartesian exponentiation on a class.

Note that this definition is limited to finite exponents, since it is defined using nested ordered pairs. If tuples of infinite length are needed, or if they might be needed in the future, use df-ixp 8456 or df-map 8402 instead. The main advantage of this definition is that it integrates better with functions and relations. For example if 𝑅 is a subset of (𝐴↑↑2_o), then df-br 5060 can be used on it, and df-fv 6358 can also be used, and so on.

It's also worth keeping in mind that ((𝑈↑↑𝑀) × (𝑈↑↑𝑁)) is generally not equal to (𝑈↑↑(𝑀 +_o 𝑁)).

This definition is technical. Use finxp1o 34667 and finxpsuc 34673 for a more standard recursive experience. (Contributed by ML, 16-Oct-2020.)

Assertion

Ref	Expression
df-finxp	⊢ (𝑈↑↑𝑁) = {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))}

Distinct variable groups:   𝑈,𝑛,𝑥,𝑦   𝑛,𝑁,𝑥,𝑦

Detailed syntax breakdown of Definition df-finxp

Step	Hyp	Ref	Expression
1		cU	. . 3 class 𝑈
2		cN	. . 3 class 𝑁
3	1, 2	cfinxp 34658	. 2 class (𝑈↑↑𝑁)
4		com 7574	. . . . 5 class ω
5	2, 4	wcel 2110	. . . 4 wff 𝑁 ∈ ω
6		c0 4291	. . . . 5 class ∅
7		vn	. . . . . . . 8 setvar 𝑛
8		vx	. . . . . . . 8 setvar 𝑥
9		cvv 3495	. . . . . . . 8 class V
10	7	cv 1532	. . . . . . . . . . 11 class 𝑛
11		c1o 8089	. . . . . . . . . . 11 class 1o
12	10, 11	wceq 1533	. . . . . . . . . 10 wff 𝑛 = 1o
13	8	cv 1532	. . . . . . . . . . 11 class 𝑥
14	13, 1	wcel 2110	. . . . . . . . . 10 wff 𝑥 ∈ 𝑈
15	12, 14	wa 398	. . . . . . . . 9 wff (𝑛 = 1o ∧ 𝑥 ∈ 𝑈)
16	9, 1	cxp 5548	. . . . . . . . . . 11 class (V × 𝑈)
17	13, 16	wcel 2110	. . . . . . . . . 10 wff 𝑥 ∈ (V × 𝑈)
18	10	cuni 4832	. . . . . . . . . . 11 class ∪ 𝑛
19		c1st 7681	. . . . . . . . . . . 12 class 1st
20	13, 19	cfv 6350	. . . . . . . . . . 11 class (1st ‘𝑥)
21	18, 20	cop 4567	. . . . . . . . . 10 class ⟨∪ 𝑛, (1st ‘𝑥)⟩
22	10, 13	cop 4567	. . . . . . . . . 10 class ⟨𝑛, 𝑥⟩
23	17, 21, 22	cif 4467	. . . . . . . . 9 class if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)
24	15, 6, 23	cif 4467	. . . . . . . 8 class if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))
25	7, 8, 4, 9, 24	cmpo 7152	. . . . . . 7 class (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))
26		vy	. . . . . . . . 9 setvar 𝑦
27	26	cv 1532	. . . . . . . 8 class 𝑦
28	2, 27	cop 4567	. . . . . . 7 class ⟨𝑁, 𝑦⟩
29	25, 28	crdg 8039	. . . . . 6 class rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)
30	2, 29	cfv 6350	. . . . 5 class (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁)
31	6, 30	wceq 1533	. . . 4 wff ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁)
32	5, 31	wa 398	. . 3 wff (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))
33	32, 26	cab 2799	. 2 class {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))}
34	3, 33	wceq 1533	1 wff (𝑈↑↑𝑁) = {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))}

This definition is referenced by:  dffinxpf  34660  finxpeq1  34661  finxpeq2  34662  csbfinxpg  34663  finxp0  34666  finxp1o  34667  finxpnom  34676