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 ) }

Metamath Proof Explorer

Definition df-ixp

Detailed syntax breakdown