MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ixp Unicode version

Definition df-ixp 6751
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.)
Assertion
Ref Expression
df-ixp  |-  X_ x  e.  A  B  =  { f  |  ( f  Fn  { x  |  x  e.  A }  /\  A. x  e.  A  ( f `  x )  e.  B
) }
Distinct variable groups:    x, f    A, f    B, f
Allowed substitution hints:    A( x)    B( x)

Detailed syntax breakdown of Definition df-ixp
StepHypRef Expression
1 vx . . 3  set  x
2 cA . . 3  class  A
3 cB . . 3  class  B
41, 2, 3cixp 6750 . 2  class  X_ x  e.  A  B
5 vf . . . . . 6  set  f
65cv 1618 . . . . 5  class  f
71cv 1618 . . . . . . 7  class  x
87, 2wcel 1621 . . . . . 6  wff  x  e.  A
98, 1cab 2242 . . . . 5  class  { x  |  x  e.  A }
106, 9wfn 4633 . . . 4  wff  f  Fn 
{ x  |  x  e.  A }
117, 6cfv 4638 . . . . . 6  class  ( f `
 x )
1211, 3wcel 1621 . . . . 5  wff  ( f `
 x )  e.  B
1312, 1, 2wral 2516 . . . 4  wff  A. x  e.  A  ( f `  x )  e.  B
1410, 13wa 360 . . 3  wff  ( f  Fn  { x  |  x  e.  A }  /\  A. x  e.  A  ( f `  x
)  e.  B )
1514, 5cab 2242 . 2  class  { f  |  ( f  Fn 
{ x  |  x  e.  A }  /\  A. x  e.  A  ( f `  x )  e.  B ) }
164, 15wceq 1619 1  wff  X_ x  e.  A  B  =  { f  |  ( f  Fn  { x  |  x  e.  A }  /\  A. x  e.  A  ( f `  x )  e.  B
) }
Colors of variables: wff set class
This definition is referenced by:  dfixp  6752  ss2ixp  6762  nfixp  6768  nfixp1  6769  ixpn0  6781  elixp2b  24486
  Copyright terms: Public domain W3C validator