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 ${⊢}\underset{{x}\in {A}}{⨉}{B}=\left\{{f}|\left({f}Fn\left\{{x}|{x}\in {A}\right\}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}\right)\right\}$

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}\underset{{x}\in {A}}{⨉}{B}$
4 vf ${setvar}{f}$
5 4 cv ${setvar}{f}$
6 0 cv ${setvar}{x}$
7 6 1 wcel ${wff}{x}\in {A}$
8 7 0 cab ${class}\left\{{x}|{x}\in {A}\right\}$
9 5 8 wfn ${wff}{f}Fn\left\{{x}|{x}\in {A}\right\}$
10 6 5 cfv ${class}{f}\left({x}\right)$
11 10 2 wcel ${wff}{f}\left({x}\right)\in {B}$
12 11 0 1 wral ${wff}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}$
13 9 12 wa ${wff}\left({f}Fn\left\{{x}|{x}\in {A}\right\}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}\right)$
14 13 4 cab ${class}\left\{{f}|\left({f}Fn\left\{{x}|{x}\in {A}\right\}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}\right)\right\}$
15 3 14 wceq ${wff}\underset{{x}\in {A}}{⨉}{B}=\left\{{f}|\left({f}Fn\left\{{x}|{x}\in {A}\right\}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}\right)\right\}$