Mathbox for ML < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-finxp Structured version   Visualization version   GIF version

Definition df-finxp 32397
 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 7795 or df-map 7746 instead. The main advantage of this definition is that it integrates better with functions and relations. For example if 𝑅 is a subset of (𝐴↑↑2𝑜), then df-br 4584 can be used on it, and df-fv 5812 can also be used, and so on. It's also worth keeping in mind that ((𝑈↑↑𝑀) × (𝑈↑↑𝑁)) is generally not equal to (𝑈↑↑(𝑀 +𝑜 𝑁)). This definition is technical. Use finxp1o 32405 and finxpsuc 32411 for a more standard recursive experience. (Contributed by ML, 16-Oct-2020.)
Assertion
Ref Expression
df-finxp (𝑈↑↑𝑁) = {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))}
Distinct variable groups:   𝑈,𝑛,𝑥,𝑦   𝑛,𝑁,𝑥,𝑦

Detailed syntax breakdown of Definition df-finxp
StepHypRef Expression
1 cU . . 3 class 𝑈
2 cN . . 3 class 𝑁
31, 2cfinxp 32396 . 2 class (𝑈↑↑𝑁)
4 com 6957 . . . . 5 class ω
52, 4wcel 1977 . . . 4 wff 𝑁 ∈ ω
6 c0 3874 . . . . 5 class
7 vn . . . . . . . 8 setvar 𝑛
8 vx . . . . . . . 8 setvar 𝑥
9 cvv 3173 . . . . . . . 8 class V
107cv 1474 . . . . . . . . . . 11 class 𝑛
11 c1o 7440 . . . . . . . . . . 11 class 1𝑜
1210, 11wceq 1475 . . . . . . . . . 10 wff 𝑛 = 1𝑜
138cv 1474 . . . . . . . . . . 11 class 𝑥
1413, 1wcel 1977 . . . . . . . . . 10 wff 𝑥𝑈
1512, 14wa 383 . . . . . . . . 9 wff (𝑛 = 1𝑜𝑥𝑈)
169, 1cxp 5036 . . . . . . . . . . 11 class (V × 𝑈)
1713, 16wcel 1977 . . . . . . . . . 10 wff 𝑥 ∈ (V × 𝑈)
1810cuni 4372 . . . . . . . . . . 11 class 𝑛
19 c1st 7057 . . . . . . . . . . . 12 class 1st
2013, 19cfv 5804 . . . . . . . . . . 11 class (1st𝑥)
2118, 20cop 4131 . . . . . . . . . 10 class 𝑛, (1st𝑥)⟩
2210, 13cop 4131 . . . . . . . . . 10 class 𝑛, 𝑥
2317, 21, 22cif 4036 . . . . . . . . 9 class if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩)
2415, 6, 23cif 4036 . . . . . . . 8 class if((𝑛 = 1𝑜𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))
257, 8, 4, 9, 24cmpt2 6551 . . . . . . 7 class (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩)))
26 vy . . . . . . . . 9 setvar 𝑦
2726cv 1474 . . . . . . . 8 class 𝑦
282, 27cop 4131 . . . . . . 7 class 𝑁, 𝑦
2925, 28crdg 7392 . . . . . 6 class rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)
302, 29cfv 5804 . . . . 5 class (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁)
316, 30wceq 1475 . . . 4 wff ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁)
325, 31wa 383 . . 3 wff (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))
3332, 26cab 2596 . 2 class {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))}
343, 33wceq 1475 1 wff (𝑈↑↑𝑁) = {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))}
 Colors of variables: wff setvar class This definition is referenced by:  dffinxpf  32398  finxpeq1  32399  finxpeq2  32400  csbfinxpg  32401  finxp0  32404  finxp1o  32405  finxpnom  32414
 Copyright terms: Public domain W3C validator