Metamath Proof Explorer

Definition df-finxp

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 or df-map instead. The main advantage of this definition is that it integrates better with functions and relations. For example if R is a subset of ( A ^^ 2o ) , then df-br can be used on it, and df-fv can also be used, and so on.

It's also worth keeping in mind that ( ( U ^^ M ) X. ( U ^^ N ) ) is generally not equal to ( U ^^ ( M +o N ) ) .

This definition is technical. Use finxp1o and finxpsuc for a more standard recursive experience. (Contributed by ML, 16-Oct-2020)

Ref Expression
Assertion df-finxp ⊢ U ↑↑ N = y | N ∈ ω ∧ ∅ = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x N y ⁡ N

Detailed syntax breakdown

Step Hyp Ref Expression
0 cU class U
1 cN class N
2 0 1 cfinxp class U ↑↑ N
3 vy setvar y
4 com class ω
5 1 4 wcel wff N ∈ ω
6 c0 class ∅
7 vn setvar n
8 vx setvar x
9 cvv class V
10 7 cv setvar n
11 c1o class 1 𝑜
12 10 11 wceq wff n = 1 𝑜
13 8 cv setvar x
14 13 0 wcel wff x ∈ U
15 12 14 wa wff n = 1 𝑜 ∧ x ∈ U
16 9 0 cxp class V × U
17 13 16 wcel wff x ∈ V × U
18 10 cuni class ⋃ n
19 c1st class 1 st
20 13 19 cfv class 1 st ⁡ x
21 18 20 cop class ⋃ n 1 st ⁡ x
22 10 13 cop class n x
23 17 21 22 cif class if x ∈ V × U ⋃ n 1 st ⁡ x n x
24 15 6 23 cif class if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x
25 7 8 4 9 24 cmpo class n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x
26 3 cv setvar y
27 1 26 cop class N y
28 25 27 crdg class rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x N y
29 1 28 cfv class rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x N y ⁡ N
30 6 29 wceq wff ∅ = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x N y ⁡ N
31 5 30 wa wff N ∈ ω ∧ ∅ = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x N y ⁡ N
32 31 3 cab class y | N ∈ ω ∧ ∅ = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x N y ⁡ N
33 2 32 wceq wff U ↑↑ N = y | N ∈ ω ∧ ∅ = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x N y ⁡ N