Definition df-finxp 38414

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 8931 or df-map 8854 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 5103 can be used on it, and df-fv 6549 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 38422 and finxpsuc 38428 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 38413	. 2 class (𝑈↑↑𝑁)
4		com 7879	. . . . 5 class ω
5	2, 4	wcel 2144	. . . 4 wff 𝑁 ∈ ω
6		c0 4277	. . . . 5 class ∅
7		vn	. . . . . . . 8 setvar 𝑛
8		vx	. . . . . . . 8 setvar 𝑥
9		cvv 3450	. . . . . . . 8 class V
10	7	cv 1568	. . . . . . . . . . 11 class 𝑛
11		c1o 8474	. . . . . . . . . . 11 class 1o
12	10, 11	wceq 1569	. . . . . . . . . 10 wff 𝑛 = 1o
13	8	cv 1568	. . . . . . . . . . 11 class 𝑥
14	13, 1	wcel 2144	. . . . . . . . . 10 wff 𝑥 ∈ 𝑈
15	12, 14	wa 401	. . . . . . . . 9 wff (𝑛 = 1o ∧ 𝑥 ∈ 𝑈)
16	9, 1	cxp 5648	. . . . . . . . . . 11 class (V × 𝑈)
17	13, 16	wcel 2144	. . . . . . . . . 10 wff 𝑥 ∈ (V × 𝑈)
18	10	cuni 4866	. . . . . . . . . . 11 class ∪ 𝑛
19		c1st 8001	. . . . . . . . . . . 12 class 1st
20	13, 19	cfv 6541	. . . . . . . . . . 11 class (1st ‘𝑥)
21	18, 20	cop 4834	. . . . . . . . . 10 class ⟨∪ 𝑛, (1st ‘𝑥)⟩
22	10, 13	cop 4834	. . . . . . . . . 10 class ⟨𝑛, 𝑥⟩
23	17, 21, 22	cif 4481	. . . . . . . . 9 class if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)
24	15, 6, 23	cif 4481	. . . . . . . 8 class if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))
25	7, 8, 4, 9, 24	cmpo 7424	. . . . . . 7 class (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))
26		vy	. . . . . . . . 9 setvar 𝑦
27	26	cv 1568	. . . . . . . 8 class 𝑦
28	2, 27	cop 4834	. . . . . . 7 class ⟨𝑁, 𝑦⟩
29	25, 28	crdg 8422	. . . . . 6 class rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)
30	2, 29	cfv 6541	. . . . 5 class (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁)
31	6, 30	wceq 1569	. . . 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 1569	1 wff (𝑈↑↑𝑁) = {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))}

This definition is used by:  dffinxpf  38415  finxpeq1  38416  finxpeq2  38417  csbfinxpg  38418  finxp0  38421  finxp1o  38422  finxpnom  38431