Definition df-finxp 37379

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 8874 or df-map 8804 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 5111 can be used on it, and df-fv 6522 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 37387 and finxpsuc 37393 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 37378	. 2 class (𝑈↑↑𝑁)
4		com 7845	. . . . 5 class ω
5	2, 4	wcel 2109	. . . 4 wff 𝑁 ∈ ω
6		c0 4299	. . . . 5 class ∅
7		vn	. . . . . . . 8 setvar 𝑛
8		vx	. . . . . . . 8 setvar 𝑥
9		cvv 3450	. . . . . . . 8 class V
10	7	cv 1539	. . . . . . . . . . 11 class 𝑛
11		c1o 8430	. . . . . . . . . . 11 class 1o
12	10, 11	wceq 1540	. . . . . . . . . 10 wff 𝑛 = 1o
13	8	cv 1539	. . . . . . . . . . 11 class 𝑥
14	13, 1	wcel 2109	. . . . . . . . . 10 wff 𝑥 ∈ 𝑈
15	12, 14	wa 395	. . . . . . . . 9 wff (𝑛 = 1o ∧ 𝑥 ∈ 𝑈)
16	9, 1	cxp 5639	. . . . . . . . . . 11 class (V × 𝑈)
17	13, 16	wcel 2109	. . . . . . . . . 10 wff 𝑥 ∈ (V × 𝑈)
18	10	cuni 4874	. . . . . . . . . . 11 class ∪ 𝑛
19		c1st 7969	. . . . . . . . . . . 12 class 1st
20	13, 19	cfv 6514	. . . . . . . . . . 11 class (1st ‘𝑥)
21	18, 20	cop 4598	. . . . . . . . . 10 class ⟨∪ 𝑛, (1st ‘𝑥)⟩
22	10, 13	cop 4598	. . . . . . . . . 10 class ⟨𝑛, 𝑥⟩
23	17, 21, 22	cif 4491	. . . . . . . . 9 class if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)
24	15, 6, 23	cif 4491	. . . . . . . 8 class if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))
25	7, 8, 4, 9, 24	cmpo 7392	. . . . . . 7 class (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))
26		vy	. . . . . . . . 9 setvar 𝑦
27	26	cv 1539	. . . . . . . 8 class 𝑦
28	2, 27	cop 4598	. . . . . . 7 class ⟨𝑁, 𝑦⟩
29	25, 28	crdg 8380	. . . . . 6 class rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)
30	2, 29	cfv 6514	. . . . 5 class (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁)
31	6, 30	wceq 1540	. . . 4 wff ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁)
32	5, 31	wa 395	. . 3 wff (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))
33	32, 26	cab 2708	. 2 class {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))}
34	3, 33	wceq 1540	1 wff (𝑈↑↑𝑁) = {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))}

This definition is referenced by:  dffinxpf  37380  finxpeq1  37381  finxpeq2  37382  csbfinxpg  37383  finxp0  37386  finxp1o  37387  finxpnom  37396