Definition df-ixp 4354

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.

Assertion

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

Distinct variable groups:   x,f   A,f   B,f

Detailed syntax breakdown of Definition df-ixp

Step	Hyp	Ref	Expression
1		vx	. . 3 set x
2		cA	. . 3 class A
3		cB	. . 3 class B
4	1, 2, 3	cixp 4353	. 2 class X_x e. A B
5		vf	. . . . . 6 set f
6	5	cv 957	. . . . 5 class f
7	6, 2	wfn 3183	. . . 4 wff f Fn A
8	1	cv 957	. . . . . . 7 class x
9	8, 6	cfv 3188	. . . . . 6 class (f` x)
10	9, 3	wcel 960	. . . . 5 wff (f` x) e. B
11	10, 1, 2	wral 1648	. . . 4 wff A.x e. A (f` x) e. B
12	7, 11	wa 223	. . 3 wff (f Fn A /\ A.x e. A (f` x) e. B)
13	12, 5	cab 1466	. 2 class {f | (f Fn A /\ A.x e. A (f` x) e. B)}
14	4, 13	wceq 958	1 wff X_x e. A B = {f | (f Fn A /\ A.x e. A (f` x) e. B)}

This definition is referenced by:  elixp2 4355  ixpeq1 4359  ixp0x 4365

Copyright terms: Public domain