From the product lemma to to a result about powersets Recall the product lemma from Easton's famous paper, which tells us something about when we have a forcing notion (which may be a proper class) that splits as a product with one factor $\lambda^+$-cc and the other factor $\lambda$-closed. The proof that in the resulting model the powerset of $\lambda$ can be calculated using the $\lambda^+$-cc forcing alone uses Replacement in Easton's paper, and in Jech's formalism (at the above link) he states it as being about functions from $\lambda$ to the base model $M$. 
Is there a published proof that doesn't use either Replacement or the trick of talking about functions to the universe, that is, a direct proof of the result about the powerset of $\lambda$? If not, can someone supply one?

EDIT: OK, here I am with another problem, but it is closely related, so I tack it on the end. This is separate from the issue of using Replacement.
How does Jech get Powerset for the proper class forcing from showing it just for regular cardinals $\lambda$? I gather he only considers $\lambda$ from the ground model. (Aside: Easton's proof here is totally opaque to me, I don't recognise anything in it that I can get a handle on.) Is it the case that every new set is bijective with some old set, or embeddable in some appropriate way in some old set, or otherwise bijective with something built out of old sets - and this makes it work?
 A: Let me handle just the set-forcing case, since I think the class forcing case is problematic. 
Suppose that $\mathbb{P}$
is $\lambda^+$-c.c., and $\mathbb{Q}$ is $\leq\lambda$-closed. If
$G\times H\subset\mathbb{P}\times\mathbb{Q}$ is $V$-generic, then
the claim is that $P(\lambda)^{V[G][H]}=P(\lambda)^{V[G]}$.
First, I claim that $\mathbb{P}$ remains $\lambda^+$-c.c. in
$V[H]$. To see this, if we had a $\mathbb{Q}$-name $\tau$ for an
antichain in $\mathbb{P}$ of size $\lambda^+$, then we may
undertake in $V$ the construction of what is called a
psuedo-generic, namely, we build a decreasing sequence of length
$\lambda^+$ of conditions in $\mathbb{Q}$ to decide the next
element of $\tau$. The point is that since $\mathbb{Q}$ is
$\leq\lambda$-closed, we may continue through limits of this
construction. Although the resulting filter that we build is not
actually $V$-generic, every two elements that it decides are in
$\tau$ must be incompatible in $\mathbb{P}$, and this violates the
chain condition in $\mathbb{P}$ in $V$.
(Perhaps you object here that since I am undertaking a transfinite
recursion, I am using the replacement axiom. That is true. My
answer to this objection, however, is that I don't really need a
version of replacement that is reaching arbitrarily high in the
universe, but instead I am merely undertaking a transfinite
recursion to build a descending sequence inside $\mathbb{Q}$,
which is a set. So all I need is to know that the set of all
$\leq\lambda^+$-sequences over $\mathbb{Q}$ exists, which does not
require the replacement axiom. That is, my uses of replacement are
sufficiently bounded, which seems to keep you safe. This reply doesn't work when the forcing is 
proper class forcing, since then it seems one is really using replacement.)
Continuing the argument, suppose that $A\subset\lambda$ in
$V[G][H]=V[H][G]$. Thus, $A$ has a $\mathbb{P}$-name in $V[H]$.
Since $\mathbb{P}$ is $\lambda^+$-c.c. in $V[H]$, we may find such
a nice name $\dot A$ having size $\lambda$. Since $\mathbb{Q}$ is
$\leq\lambda$-closed in $V$, it follows that $\dot A\in V$. Thus,
$A={\dot A}_G\in V[G]$, as desired.
The argument generalizes to show that any $\lambda$-sequence in $V[G][H]$ from a set in $V$ is in already $V[G]$. All that is needed for this is to know that if one has $\lambda^+$-c.c. forcing $\sigma$ is the name of a $\lambda$-sequence of elements of a set $B$, then there is a nice name, consisting essentially of a $\lambda$-sequence of $B$-labeled antichains. One argues similarly that such a name cannot have been added by the $\mathbb{Q}$-forcing, and so the name is already in $V$, putting the sequence into $V[G]$, just as with the subsets of $\lambda$. Since everything is bounded here nicely, I don't see that one is using replacement even for the general case of $\lambda$-sequences (although of course without replacement there simply are fewer such sequences that one might have in ZFC). 
A: When doing this in a set theory without replacement, the issue is really in the definition of $(\leq \lambda)$-closed. Here is a concrete example to illustrate.
Work in $V_{\omega+\omega}$, which is a model of ZC. Obvious failure of replacement in this model is that $\omega+\omega \notin V_{\omega+\omega}$ and yet there is an easy bijection between $\omega$ and $\omega+\omega$. For $\mathbb{Q}$, use the set of all finite partial functions $p:\lbrace\omega,\omega+1,\omega+2,\ldots\rbrace\to\lbrace0,1\rbrace$. Note that $\mathbb{Q}$ is isomorphic to standard Cohen forcing, except that $\mathbb{Q}$ is a proper class. Interestingly, $\mathbb{Q}$ is $(\leq\omega)$-closed for the trivial reason that $\mathbb{Q}$ has no infinite sub-set! Nevertheless, forcing with $\mathbb{Q}$ is the same as standard Cohen forcing and therefore adds a new subset of $\omega$.
For class forcing in models without replacement, the appropriate definition of $(\leq\lambda)$-closed is that every sub-class of $\mathbb{Q}$ which is a chain of size at most $\lambda$ has a lower bound in $\mathbb{Q}$. With this definition, the argument that Joel gave works perfectly.
