# Metamath Proof Explorer

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