Theorem 2sqreunnlem2

Description: Lemma 2 for 2sqreunn . (Contributed by AV, 25-Jun-2023)

	Ref	Expression
Hypothesis	2sqreulem4.1	$$⊢\phi \leftrightarrow \left(\psi \wedge a^2+b^2=P\right)$$
Assertion	2sqreunnlem2	$$⊢\forall a\in \mathbb{N}{\exists }^{*}b\in \mathbb{N}\phi$$

Proof

Step	Hyp	Ref	Expression
1		2sqreulem4.1	$$⊢\phi \leftrightarrow \left(\psi \wedge a^2+b^2=P\right)$$
2		nnssnn0	$$⊢\mathbb{N}\subseteq {\mathbb{N}}_0$$
3	1	2sqreulem4	$$⊢\forall a\in {\mathbb{N}}_0{\exists }^{*}b\in {\mathbb{N}}_0\phi$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}b\mathbb{N}$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}b{\mathbb{N}}_0$$
6	4 5	ssrmof	$$⊢\mathbb{N}\subseteq {\mathbb{N}}_0\to \left({\exists }^{*}b\in {\mathbb{N}}_0\phi \to {\exists }^{*}b\in \mathbb{N}\phi \right)$$
7	6	ralimdv	$$⊢\mathbb{N}\subseteq {\mathbb{N}}_0\to \left(\forall a\in {\mathbb{N}}_0{\exists }^{*}b\in {\mathbb{N}}_0\phi \to \forall a\in {\mathbb{N}}_0{\exists }^{*}b\in \mathbb{N}\phi \right)$$
8	2 3 7	mp2	$$⊢\forall a\in {\mathbb{N}}_0{\exists }^{*}b\in \mathbb{N}\phi$$
9		ssralv	$$⊢\mathbb{N}\subseteq {\mathbb{N}}_0\to \left(\forall a\in {\mathbb{N}}_0{\exists }^{*}b\in \mathbb{N}\phi \to \forall a\in \mathbb{N}{\exists }^{*}b\in \mathbb{N}\phi \right)$$
10	2 8 9	mp2	$$⊢\forall a\in \mathbb{N}{\exists }^{*}b\in \mathbb{N}\phi$$