Users' Mathboxes 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 33719
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 8149 or df-map 8097 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 4844 can be used on it, and df-fv 6109 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 33727 and finxpsuc 33733 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 33718 . 2 class (𝑈↑↑𝑁)
4 com 7299 . . . . 5 class ω
52, 4wcel 2157 . . . 4 wff 𝑁 ∈ ω
6 c0 4115 . . . . 5 class
7 vn . . . . . . . 8 setvar 𝑛
8 vx . . . . . . . 8 setvar 𝑥
9 cvv 3385 . . . . . . . 8 class V
107cv 1652 . . . . . . . . . . 11 class 𝑛
11 c1o 7792 . . . . . . . . . . 11 class 1𝑜
1210, 11wceq 1653 . . . . . . . . . 10 wff 𝑛 = 1𝑜
138cv 1652 . . . . . . . . . . 11 class 𝑥
1413, 1wcel 2157 . . . . . . . . . 10 wff 𝑥𝑈
1512, 14wa 385 . . . . . . . . 9 wff (𝑛 = 1𝑜𝑥𝑈)
169, 1cxp 5310 . . . . . . . . . . 11 class (V × 𝑈)
1713, 16wcel 2157 . . . . . . . . . 10 wff 𝑥 ∈ (V × 𝑈)
1810cuni 4628 . . . . . . . . . . 11 class 𝑛
19 c1st 7399 . . . . . . . . . . . 12 class 1st
2013, 19cfv 6101 . . . . . . . . . . 11 class (1st𝑥)
2118, 20cop 4374 . . . . . . . . . 10 class 𝑛, (1st𝑥)⟩
2210, 13cop 4374 . . . . . . . . . 10 class 𝑛, 𝑥
2317, 21, 22cif 4277 . . . . . . . . 9 class if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩)
2415, 6, 23cif 4277 . . . . . . . 8 class if((𝑛 = 1𝑜𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))
257, 8, 4, 9, 24cmpt2 6880 . . . . . . 7 class (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩)))
26 vy . . . . . . . . 9 setvar 𝑦
2726cv 1652 . . . . . . . 8 class 𝑦
282, 27cop 4374 . . . . . . 7 class 𝑁, 𝑦
2925, 28crdg 7744 . . . . . 6 class rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)
302, 29cfv 6101 . . . . 5 class (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁)
316, 30wceq 1653 . . . 4 wff ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁)
325, 31wa 385 . . 3 wff (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))
3332, 26cab 2785 . 2 class {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))}
343, 33wceq 1653 1 wff (𝑈↑↑𝑁) = {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))}
Colors of variables: wff setvar class
This definition is referenced by:  dffinxpf  33720  finxpeq1  33721  finxpeq2  33722  csbfinxpg  33723  finxp0  33726  finxp1o  33727  finxpnom  33736
  Copyright terms: Public domain W3C validator