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 33558
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 8063 or df-map 8011 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 4787 can be used on it, and df-fv 6039 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 33566 and finxpsuc 33572 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 33557 . 2 class (𝑈↑↑𝑁)
4 com 7212 . . . . 5 class ω
52, 4wcel 2145 . . . 4 wff 𝑁 ∈ ω
6 c0 4063 . . . . 5 class
7 vn . . . . . . . 8 setvar 𝑛
8 vx . . . . . . . 8 setvar 𝑥
9 cvv 3351 . . . . . . . 8 class V
107cv 1630 . . . . . . . . . . 11 class 𝑛
11 c1o 7706 . . . . . . . . . . 11 class 1𝑜
1210, 11wceq 1631 . . . . . . . . . 10 wff 𝑛 = 1𝑜
138cv 1630 . . . . . . . . . . 11 class 𝑥
1413, 1wcel 2145 . . . . . . . . . 10 wff 𝑥𝑈
1512, 14wa 382 . . . . . . . . 9 wff (𝑛 = 1𝑜𝑥𝑈)
169, 1cxp 5247 . . . . . . . . . . 11 class (V × 𝑈)
1713, 16wcel 2145 . . . . . . . . . 10 wff 𝑥 ∈ (V × 𝑈)
1810cuni 4574 . . . . . . . . . . 11 class 𝑛
19 c1st 7313 . . . . . . . . . . . 12 class 1st
2013, 19cfv 6031 . . . . . . . . . . 11 class (1st𝑥)
2118, 20cop 4322 . . . . . . . . . 10 class 𝑛, (1st𝑥)⟩
2210, 13cop 4322 . . . . . . . . . 10 class 𝑛, 𝑥
2317, 21, 22cif 4225 . . . . . . . . 9 class if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩)
2415, 6, 23cif 4225 . . . . . . . 8 class if((𝑛 = 1𝑜𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))
257, 8, 4, 9, 24cmpt2 6795 . . . . . . 7 class (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩)))
26 vy . . . . . . . . 9 setvar 𝑦
2726cv 1630 . . . . . . . 8 class 𝑦
282, 27cop 4322 . . . . . . 7 class 𝑁, 𝑦
2925, 28crdg 7658 . . . . . 6 class rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)
302, 29cfv 6031 . . . . 5 class (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁)
316, 30wceq 1631 . . . 4 wff ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁)
325, 31wa 382 . . 3 wff (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))
3332, 26cab 2757 . 2 class {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))}
343, 33wceq 1631 1 wff (𝑈↑↑𝑁) = {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))}
Colors of variables: wff setvar class
This definition is referenced by:  dffinxpf  33559  finxpeq1  33560  finxpeq2  33561  csbfinxpg  33562  finxp0  33565  finxp1o  33566  finxpnom  33575
  Copyright terms: Public domain W3C validator