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

Definition df-ixp 7795
Description: Definition of infinite Cartesian product of [Enderton] p. 54. Enderton uses a bold "X" with 𝑥𝐴 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 𝐵 represents a class expression containing 𝑥 free and thus can be thought of as 𝐵(𝑥). Normally, 𝑥 is not free in 𝐴, although this is not a requirement of the definition. (Contributed by NM, 28-Sep-2006.)
Assertion
Ref Expression
df-ixp X𝑥𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn {𝑥𝑥𝐴} ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵)}
Distinct variable groups:   𝑥,𝑓   𝐴,𝑓   𝐵,𝑓
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)

Detailed syntax breakdown of Definition df-ixp
StepHypRef Expression
1 vx . . 3 setvar 𝑥
2 cA . . 3 class 𝐴
3 cB . . 3 class 𝐵
41, 2, 3cixp 7794 . 2 class X𝑥𝐴 𝐵
5 vf . . . . . 6 setvar 𝑓
65cv 1474 . . . . 5 class 𝑓
71cv 1474 . . . . . . 7 class 𝑥
87, 2wcel 1977 . . . . . 6 wff 𝑥𝐴
98, 1cab 2596 . . . . 5 class {𝑥𝑥𝐴}
106, 9wfn 5799 . . . 4 wff 𝑓 Fn {𝑥𝑥𝐴}
117, 6cfv 5804 . . . . . 6 class (𝑓𝑥)
1211, 3wcel 1977 . . . . 5 wff (𝑓𝑥) ∈ 𝐵
1312, 1, 2wral 2896 . . . 4 wff 𝑥𝐴 (𝑓𝑥) ∈ 𝐵
1410, 13wa 383 . . 3 wff (𝑓 Fn {𝑥𝑥𝐴} ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵)
1514, 5cab 2596 . 2 class {𝑓 ∣ (𝑓 Fn {𝑥𝑥𝐴} ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵)}
164, 15wceq 1475 1 wff X𝑥𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn {𝑥𝑥𝐴} ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ 𝐵)}
Colors of variables: wff setvar class
This definition is referenced by:  dfixp  7796  ss2ixp  7807  nfixp  7813  nfixp1  7814  ixpn0  7826
  Copyright terms: Public domain W3C validator