Definition df-ixp

Description: Definition of infinite Cartesian product of Enderton p. 54. Enderton uses a bold "X" with x e. A written underneath or as a subscript, as does Stoll p. 47. Some books use a capital pi, but we will reserve that notation for products of numbers. Usually B represents a class expression containing x free and thus can be thought of as B ( x ) . Normally, x is not free in A , although this is not a requirement of the definition. (Contributed by NM, 28-Sep-2006)

	Ref	Expression
Assertion	df-ixp	|- X_ x e. A B = { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	|- x
1		cA	|- A
2		cB	|- B
3	0 1 2	cixp	|- X_ x e. A B
4		vf	|- f
5	4	cv	|- f
6	0	cv	|- x
7	6 1	wcel	|- x e. A
8	7 0	cab	|- { x | x e. A }
9	5 8	wfn	|- f Fn { x | x e. A }
10	6 5	cfv	|- ( f ` x )
11	10 2	wcel	|- ( f ` x ) e. B
12	11 0 1	wral	|- A. x e. A ( f ` x ) e. B
13	9 12	wa	|- ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B )
14	13 4	cab	|- { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) }
15	3 14	wceq	|- X_ x e. A B = { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) }