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 ∈ A B = f | f Fn x | x ∈ A ∧ ∀ x ∈ A f ⁡ x ∈ B

Detailed syntax breakdown

Step Hyp Ref Expression
0 vx setvar x
1 cA class A
2 cB class B
3 0 1 2 cixp class ⨉ x ∈ A B
4 vf setvar f
5 4 cv setvar f
6 0 cv setvar x
7 6 1 wcel wff x ∈ A
8 7 0 cab class x | x ∈ A
9 5 8 wfn wff f Fn x | x ∈ A
10 6 5 cfv class f ⁡ x
11 10 2 wcel wff f ⁡ x ∈ B
12 11 0 1 wral wff ∀ x ∈ A f ⁡ x ∈ B
13 9 12 wa wff f Fn x | x ∈ A ∧ ∀ x ∈ A f ⁡ x ∈ B
14 13 4 cab class f | f Fn x | x ∈ A ∧ ∀ x ∈ A f ⁡ x ∈ B
15 3 14 wceq wff ⨉ x ∈ A B = f | f Fn x | x ∈ A ∧ ∀ x ∈ A f ⁡ x ∈ B