Definition df-finxp 34801

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 8445 or df-map 8391 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 5031 can be used on it, and df-fv 6332 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 34809 and finxpsuc 34815 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 34800	. 2 class (𝑈↑↑𝑁)
4		com 7560	. . . . 5 class ω
5	2, 4	wcel 2111	. . . 4 wff 𝑁 ∈ ω
6		c0 4243	. . . . 5 class ∅
7		vn	. . . . . . . 8 setvar 𝑛
8		vx	. . . . . . . 8 setvar 𝑥
9		cvv 3441	. . . . . . . 8 class V
10	7	cv 1537	. . . . . . . . . . 11 class 𝑛
11		c1o 8078	. . . . . . . . . . 11 class 1o
12	10, 11	wceq 1538	. . . . . . . . . 10 wff 𝑛 = 1o
13	8	cv 1537	. . . . . . . . . . 11 class 𝑥
14	13, 1	wcel 2111	. . . . . . . . . 10 wff 𝑥 ∈ 𝑈
15	12, 14	wa 399	. . . . . . . . 9 wff (𝑛 = 1o ∧ 𝑥 ∈ 𝑈)
16	9, 1	cxp 5517	. . . . . . . . . . 11 class (V × 𝑈)
17	13, 16	wcel 2111	. . . . . . . . . 10 wff 𝑥 ∈ (V × 𝑈)
18	10	cuni 4800	. . . . . . . . . . 11 class ∪ 𝑛
19		c1st 7669	. . . . . . . . . . . 12 class 1st
20	13, 19	cfv 6324	. . . . . . . . . . 11 class (1st ‘𝑥)
21	18, 20	cop 4531	. . . . . . . . . 10 class ⟨∪ 𝑛, (1st ‘𝑥)⟩
22	10, 13	cop 4531	. . . . . . . . . 10 class ⟨𝑛, 𝑥⟩
23	17, 21, 22	cif 4425	. . . . . . . . 9 class if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)
24	15, 6, 23	cif 4425	. . . . . . . 8 class if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))
25	7, 8, 4, 9, 24	cmpo 7137	. . . . . . 7 class (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩)))
26		vy	. . . . . . . . 9 setvar 𝑦
27	26	cv 1537	. . . . . . . 8 class 𝑦
28	2, 27	cop 4531	. . . . . . 7 class ⟨𝑁, 𝑦⟩
29	25, 28	crdg 8028	. . . . . 6 class rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)
30	2, 29	cfv 6324	. . . . 5 class (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁)
31	6, 30	wceq 1538	. . . 4 wff ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁)
32	5, 31	wa 399	. . 3 wff (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))
33	32, 26	cab 2776	. 2 class {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))}
34	3, 33	wceq 1538	1 wff (𝑈↑↑𝑁) = {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨∪ 𝑛, (1st ‘𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))}

This definition is referenced by:  dffinxpf  34802  finxpeq1  34803  finxpeq2  34804  csbfinxpg  34805  finxp0  34808  finxp1o  34809  finxpnom  34818