df-finxp

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 \in ω \land \emptyset = rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times 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 \in ω$
6		c0	$class \emptyset$
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 \in U$
15	12 14	wa	$wff (n = 1_{𝑜} \land x \in U)$
16	9 0	cxp	$class (V \times U)$
17	13 16	wcel	$wff x \in (V \times 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 \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩)$
24	15 6 23	cif	$class if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))$
25	7 8 4 9 24	cmpo	$class (n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times 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 \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨N, y⟩)$
29	1 28	cfv	$class rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨N, y⟩) (N)$
30	6 29	wceq	$wff \emptyset = rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨N, y⟩) (N)$
31	5 30	wa	$wff (N \in ω \land \emptyset = rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨N, y⟩) (N))$
32	31 3	cab	$class \{y \| (N \in ω \land \emptyset = rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨N, y⟩) (N))\}$
33	2 32	wceq	$wff U ↑↑ N = \{y \| (N \in ω \land \emptyset = rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨N, y⟩) (N))\}$

Metamath Proof Explorer

Definition df-finxp

Detailed syntax breakdown