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 37385
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 8938 or df-map 8868 instead. The main advantage of this definition is that it integrates better with functions and relations. For example if 𝑅 is a subset of (𝐴↑↑2o), then df-br 5144 can be used on it, and df-fv 6569 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 37393 and finxpsuc 37399 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
StepHypRef Expression
1 cU . . 3 class 𝑈
2 cN . . 3 class 𝑁
31, 2cfinxp 37384 . 2 class (𝑈↑↑𝑁)
4 com 7887 . . . . 5 class ω
52, 4wcel 2108 . . . 4 wff 𝑁 ∈ ω
6 c0 4333 . . . . 5 class
7 vn . . . . . . . 8 setvar 𝑛
8 vx . . . . . . . 8 setvar 𝑥
9 cvv 3480 . . . . . . . 8 class V
107cv 1539 . . . . . . . . . . 11 class 𝑛
11 c1o 8499 . . . . . . . . . . 11 class 1o
1210, 11wceq 1540 . . . . . . . . . 10 wff 𝑛 = 1o
138cv 1539 . . . . . . . . . . 11 class 𝑥
1413, 1wcel 2108 . . . . . . . . . 10 wff 𝑥𝑈
1512, 14wa 395 . . . . . . . . 9 wff (𝑛 = 1o𝑥𝑈)
169, 1cxp 5683 . . . . . . . . . . 11 class (V × 𝑈)
1713, 16wcel 2108 . . . . . . . . . 10 wff 𝑥 ∈ (V × 𝑈)
1810cuni 4907 . . . . . . . . . . 11 class 𝑛
19 c1st 8012 . . . . . . . . . . . 12 class 1st
2013, 19cfv 6561 . . . . . . . . . . 11 class (1st𝑥)
2118, 20cop 4632 . . . . . . . . . 10 class 𝑛, (1st𝑥)⟩
2210, 13cop 4632 . . . . . . . . . 10 class 𝑛, 𝑥
2317, 21, 22cif 4525 . . . . . . . . 9 class if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩)
2415, 6, 23cif 4525 . . . . . . . 8 class if((𝑛 = 1o𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))
257, 8, 4, 9, 24cmpo 7433 . . . . . . 7 class (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩)))
26 vy . . . . . . . . 9 setvar 𝑦
2726cv 1539 . . . . . . . 8 class 𝑦
282, 27cop 4632 . . . . . . 7 class 𝑁, 𝑦
2925, 28crdg 8449 . . . . . 6 class rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)
302, 29cfv 6561 . . . . 5 class (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁)
316, 30wceq 1540 . . . 4 wff ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁)
325, 31wa 395 . . 3 wff (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))
3332, 26cab 2714 . 2 class {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))}
343, 33wceq 1540 1 wff (𝑈↑↑𝑁) = {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))}
Colors of variables: wff setvar class
This definition is referenced by:  dffinxpf  37386  finxpeq1  37387  finxpeq2  37388  csbfinxpg  37389  finxp0  37392  finxp1o  37393  finxpnom  37402
  Copyright terms: Public domain W3C validator