Definition df-finxp 38138

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 8905 or df-map 8828 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 5104 can be used on it, and df-fv 6541 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 38146 and finxpsuc 38152 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 38137	. 2 class (𝑈↑↑𝑁)
4		com 7862	. . . . 5 class ω
5	2, 4	wcel 2145	. . . 4 wff 𝑁 ∈ ω
6		c0 4279	. . . . 5 class ∅
7		vn	. . . . . . . 8 setvar 𝑛
8		vx	. . . . . . . 8 setvar 𝑥
9		cvv 3450	. . . . . . . 8 class V
10	7	cv 1569	. . . . . . . . . . 11 class 𝑛
11		c1o 8448	. . . . . . . . . . 11 class 1o
12	10, 11	wceq 1570	. . . . . . . . . 10 wff 𝑛 = 1o
13	8	cv 1569	. . . . . . . . . . 11 class 𝑥
14	13, 1	wcel 2145	. . . . . . . . . 10 wff 𝑥 ∈ 𝑈
15	12, 14	wa 401	. . . . . . . . 9 wff (𝑛 = 1o ∧ 𝑥 ∈ 𝑈)
16	9, 1	cxp 5653	. . . . . . . . . . 11 class (V × 𝑈)
17	13, 16	wcel 2145	. . . . . . . . . 10 wff 𝑥 ∈ (V × 𝑈)
18	10	cuni 4867	. . . . . . . . . . 11 class ∪ 𝑛
19		c1st 7984	. . . . . . . . . . . 12 class 1st
20	13, 19	cfv 6533	. . . . . . . . . . 11 class (1st ‘𝑥)
21	18, 20	cop 4590	. . . . . . . . . 10 class ⟨∪ 𝑛, (1st ‘𝑥)⟩
22	10, 13	cop 4590	. . . . . . . . . 10 class ⟨𝑛, 𝑥⟩
23	17, 21, 22	cif 4482	. . . . . . . . 9 class if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)
24	15, 6, 23	cif 4482	. . . . . . . 8 class if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))
25	7, 8, 4, 9, 24	cmpo 7415	. . . . . . 7 class (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))
26		vy	. . . . . . . . 9 setvar 𝑦
27	26	cv 1569	. . . . . . . 8 class 𝑦
28	2, 27	cop 4590	. . . . . . 7 class ⟨𝑁, 𝑦⟩
29	25, 28	crdg 8398	. . . . . 6 class rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)
30	2, 29	cfv 6533	. . . . 5 class (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁)
31	6, 30	wceq 1570	. . . 4 wff ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁)
32	5, 31	wa 401	. . 3 wff (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))
33	32, 26	cab 2738	. 2 class {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))}
34	3, 33	wceq 1570	1 wff (𝑈↑↑𝑁) = {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))}

This definition is used by:  dffinxpf  38139  finxpeq1  38140  finxpeq2  38141  csbfinxpg  38142  finxp0  38145  finxp1o  38146  finxpnom  38155