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 36260
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 8891 or df-map 8821 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 5149 can be used on it, and df-fv 6551 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 36268 and finxpsuc 36274 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 36259 . 2 class (𝑈↑↑𝑁)
4 com 7854 . . . . 5 class ω
52, 4wcel 2106 . . . 4 wff 𝑁 ∈ ω
6 c0 4322 . . . . 5 class
7 vn . . . . . . . 8 setvar 𝑛
8 vx . . . . . . . 8 setvar 𝑥
9 cvv 3474 . . . . . . . 8 class V
107cv 1540 . . . . . . . . . . 11 class 𝑛
11 c1o 8458 . . . . . . . . . . 11 class 1o
1210, 11wceq 1541 . . . . . . . . . 10 wff 𝑛 = 1o
138cv 1540 . . . . . . . . . . 11 class 𝑥
1413, 1wcel 2106 . . . . . . . . . 10 wff 𝑥𝑈
1512, 14wa 396 . . . . . . . . 9 wff (𝑛 = 1o𝑥𝑈)
169, 1cxp 5674 . . . . . . . . . . 11 class (V × 𝑈)
1713, 16wcel 2106 . . . . . . . . . 10 wff 𝑥 ∈ (V × 𝑈)
1810cuni 4908 . . . . . . . . . . 11 class 𝑛
19 c1st 7972 . . . . . . . . . . . 12 class 1st
2013, 19cfv 6543 . . . . . . . . . . 11 class (1st𝑥)
2118, 20cop 4634 . . . . . . . . . 10 class 𝑛, (1st𝑥)⟩
2210, 13cop 4634 . . . . . . . . . 10 class 𝑛, 𝑥
2317, 21, 22cif 4528 . . . . . . . . 9 class if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩)
2415, 6, 23cif 4528 . . . . . . . 8 class if((𝑛 = 1o𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))
257, 8, 4, 9, 24cmpo 7410 . . . . . . 7 class (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩)))
26 vy . . . . . . . . 9 setvar 𝑦
2726cv 1540 . . . . . . . 8 class 𝑦
282, 27cop 4634 . . . . . . 7 class 𝑁, 𝑦
2925, 28crdg 8408 . . . . . 6 class rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)
302, 29cfv 6543 . . . . 5 class (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁)
316, 30wceq 1541 . . . 4 wff ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁)
325, 31wa 396 . . 3 wff (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))
3332, 26cab 2709 . 2 class {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))}
343, 33wceq 1541 1 wff (𝑈↑↑𝑁) = {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o𝑥𝑈), ∅, if(𝑥 ∈ (V × 𝑈), ⟨ 𝑛, (1st𝑥)⟩, ⟨𝑛, 𝑥⟩))), ⟨𝑁, 𝑦⟩)‘𝑁))}
Colors of variables: wff setvar class
This definition is referenced by:  dffinxpf  36261  finxpeq1  36262  finxpeq2  36263  csbfinxpg  36264  finxp0  36267  finxp1o  36268  finxpnom  36277
  Copyright terms: Public domain W3C validator