A Poset has the -chain condition (-c.c.)
if any Strong Antichain in has size
If we call this the countable chain condition (c.c.c.).
Theorem
Let be a Transitive Model of ,
with a cardinal in and a Forcing Partial Order such that
Suppose we have a Model Extension and such that
for some .
Then there is a function such that with
Proof
Let .
Then
for the Canonical Names and .
By definition then some has
Now define
Clearly .
Let .
Now for some so some has .
As is a Filter, we find and so so .
For each , consider
Using Axiom of Choice in , pick with
Finally, write
We can check that is an Strong Antichain:
let for some and assume .
Then and so .
But because has -chain condition in we conclude
But the function is an injection from to thus
Corollary
If is a Regular Cardinal in and
then the Model Extension has:
Proof
Suppose not, so find with surjective.
By above theorem, find with and
We conclude
But then is a union of many sets of size ,
so cannot be Regular Cardinal.