$\omega_1$-closedness and fullness for $\searrow$ $\omega$-sequences

Let $\pi$ is a $\Bbb{P}$-name for a partial order, i.e. there is a name $\pi'$ and $\pi''$ such that $$1\Vdash_\Bbb{P} \pi '' \in \pi\land (\text{\pi' is a partial order of \pi with largest element \pi''}).$$ We call $\pi$ is full for $\searrow$ $\omega$-sequences if whenever $p\in \Bbb{P}$, $\rho_n\in\operatorname{dom} \pi$ for each $n<\omega$ and $$p\Vdash \rho_n\in\pi \land \rho_{n+1} \le \rho_n$$ for each $n$ then there is a $\sigma\in\operatorname{dom} \pi$ s.t. $p\Vdash \sigma\in\pi$ and $p\Vdash \sigma\le \rho_n$ for each $n$.

I try to prove following statement: if $\Bbb{P}$ is $\omega_1$-closed and $\pi$ is full for $\searrow$ $\omega$-sequences, then $1\Vdash \text{$\pi$is$\omega_1$-closed}.$

I made two 'proofs' which the former one is regarded as false and the latter one is incomplete. The 'false proof' goes as follow:

Let $\rho$ is a $\Bbb{P}$-name satisfying $$1\Vdash \forall n<\check{\omega}:\rho(n+1)\le \rho(n) \,\land\, \rho(n)\in \pi .$$ so for each $n$, $1\Vdash \rho(n+1)\le \rho(n)$ and $1\Vdash \rho(n)\in\pi$. (*)

Therefore, since $\pi$ is full for $\searrow$ $\omega$-sequences, we can find a name $\sigma$ such that $1\Vdash \sigma\le \rho(n)$ for all $n<\omega$ and $1\Vdash \sigma\in\pi$, so $1\Vdash \forall n<\check{\omega}: \sigma\le\rho(n)$ (**) and therefore $1\Vdash \text{$\pi$is$\omega_1$-closed}$.

I doubt the part (*) and (**) are problematic. Is it right? I didn't get why they are problematic so I need an explanation for them.

I guess the 'proof' given below goes to right direction:

Let $p\in \Bbb{P}$ be arbitrary and $\rho$ be a $\Bbb{P}$-name satisfying $$p\Vdash \forall n<\check{\omega}: \rho(n+1) \le\rho(n)\,\land\, \rho(n)\in\pi.$$ Since $p\Vdash \exists x \in \pi : \rho(\check{0}) = x$, there is $p_0\le p$ and $\Bbb{P}$-name $\sigma_0$ s.t. $$p_0 \Vdash \sigma_0\in \pi\,\land\, \rho(\check{0}) = \sigma_0.$$ Similarly, we can take $p_1\le p_0$ and a $\Bbb{P}$-name $\sigma_1$ satisfying $$p_1 \Vdash \sigma_1\in \pi\,\land\, \rho(\check{1}) = \sigma_1.$$ and so on. Since $\langle p_n : n<\omega\rangle$ is decreasing $\Bbb{P}$-sequence, we can find some $q\in \Bbb{P}$ with $q\le p_n$ for all $n<\omega$. For such $q$ should satisfy $$q\Vdash \sigma_{n+1}\le\sigma_n\,\land\, \sigma_n\in\pi$$ for each $n<\omega$, so we can find a $\Bbb{P}$-name $\sigma$ s.t. $q\Vdash \sigma\le\sigma_n$ and $q\Vdash \sigma\in\pi$ for each $n$.

In above proof, however, I wonder can I conclude that $q\Vdash \forall n<\check{\omega} : \sigma\le \rho(n)$ holds. I would appreciate any help, thanks!

• What comes to my mind concerning the first proof is: In the assumption needed to apply "fullness", we need a name $\rho_n$ for every $n<\omega$, but in your proof, you only use one name $\rho$. (*) is correct, but it doesn't enable you to apply the consequence for "full". – user35359 Aug 29 '15 at 3:42

The answer to your last question is affirmative: Any extension by a generic filter that contains $q$ will satisfy the formula on the right side. (For the same reason, your steps (*) and (**) are correct, but the problem with the first proof is a different one I think, see my comment.)
Your proof is almost done. To complete the argument, we could assume for a contradiction that there is $p$ so that
$p\Vdash (\rho : \check{\omega} \to \pi) \land (\forall n<\check{\omega} \ (\rho(n)\in\pi \land \rho(n+1)\leq \rho(n)))\land (\forall x\in\pi \, \exists n<\check{\omega} \ x \not \leq \rho(n))$
Then by your argument we get $q\leq p$ with $q\Vdash \sigma\in\pi \land \forall n<\check{\omega}\ \sigma \leq \rho(n)$
so $q$ forces a contradiction, which is impossible.