Description: An infinite Cartesian product is a subset of set exponentiation. Remark in Enderton p. 54. (Contributed by NM, 28-Sep-2006)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ixpssmap.2 | |- B e. _V |
|
Assertion | ixpssmap | |- X_ x e. A B C_ ( U_ x e. A B ^m A ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ixpssmap.2 | |- B e. _V |
|
2 | 1 | rgenw | |- A. x e. A B e. _V |
3 | ixpssmapg | |- ( A. x e. A B e. _V -> X_ x e. A B C_ ( U_ x e. A B ^m A ) ) |
|
4 | 2 3 | ax-mp | |- X_ x e. A B C_ ( U_ x e. A B ^m A ) |