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	⊢ ( 𝑈 ↑↑ 𝑁 ) = { 𝑦 ∣ ( 𝑁 ∈ ω ∧ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cU	⊢ 𝑈
1		cN	⊢ 𝑁
2	0 1	cfinxp	⊢ ( 𝑈 ↑↑ 𝑁 )
3		vy	⊢ 𝑦
4		com	⊢ ω
5	1 4	wcel	⊢ 𝑁 ∈ ω
6		c0	⊢ ∅
7		vn	⊢ 𝑛
8		vx	⊢ 𝑥
9		cvv	⊢ V
10	7	cv	⊢ 𝑛
11		c1o	⊢ 1o
12	10 11	wceq	⊢ 𝑛 = 1o
13	8	cv	⊢ 𝑥
14	13 0	wcel	⊢ 𝑥 ∈ 𝑈
15	12 14	wa	⊢ ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 )
16	9 0	cxp	⊢ ( V × 𝑈 )
17	13 16	wcel	⊢ 𝑥 ∈ ( V × 𝑈 )
18	10	cuni	⊢ ∪ 𝑛
19		c1st	⊢ 1st
20	13 19	cfv	⊢ ( 1st ‘ 𝑥 )
21	18 20	cop	⊢ ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩
22	10 13	cop	⊢ ⟨ 𝑛 , 𝑥 ⟩
23	17 21 22	cif	⊢ if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ )
24	15 6 23	cif	⊢ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) )
25	7 8 4 9 24	cmpo	⊢ ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) )
26	3	cv	⊢ 𝑦
27	1 26	cop	⊢ ⟨ 𝑁 , 𝑦 ⟩
28	25 27	crdg	⊢ rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ )
29	1 28	cfv	⊢ ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 )
30	6 29	wceq	⊢ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 )
31	5 30	wa	⊢ ( 𝑁 ∈ ω ∧ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) )
32	31 3	cab	⊢ { 𝑦 ∣ ( 𝑁 ∈ ω ∧ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ) }
33	2 32	wceq	⊢ ( 𝑈 ↑↑ 𝑁 ) = { 𝑦 ∣ ( 𝑁 ∈ ω ∧ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ) }