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	$$⊢\underset{x\in A}{⨉}B=\left\{f|\left(fFn\left\{x|x\in A\right\}\wedge \forall x\in Af\left(x\right)\in B\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		cA	$$classA$$
2		cB	$$classB$$
3	0 1 2	cixp	$$class\underset{x\in A}{⨉}B$$
4		vf	$$setvarf$$
5	4	cv	$$setvarf$$
6	0	cv	$$setvarx$$
7	6 1	wcel	$$wffx\in A$$
8	7 0	cab	$$class\left\{x|x\in A\right\}$$
9	5 8	wfn	$$wfffFn\left\{x|x\in A\right\}$$
10	6 5	cfv	$$classf\left(x\right)$$
11	10 2	wcel	$$wfff\left(x\right)\in B$$
12	11 0 1	wral	$$wff\forall x\in Af\left(x\right)\in B$$
13	9 12	wa	$$wff\left(fFn\left\{x|x\in A\right\}\wedge \forall x\in Af\left(x\right)\in B\right)$$
14	13 4	cab	$$class\left\{f|\left(fFn\left\{x|x\in A\right\}\wedge \forall x\in Af\left(x\right)\in B\right)\right\}$$
15	3 14	wceq	$$wff\underset{x\in A}{⨉}B=\left\{f|\left(fFn\left\{x|x\in A\right\}\wedge \forall x\in Af\left(x\right)\in B\right)\right\}$$