Theorem r19.2uz

Description: A version of r19.2z for upper integer quantifiers. (Contributed by Mario Carneiro, 15-Feb-2014)

	Ref	Expression
Hypothesis	rexuz3.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
Assertion	r19.2uz	$$⊢\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\phi \to \exists k\in Z\phi$$

Proof

Step	Hyp	Ref	Expression
1		rexuz3.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		eluzelz	$$⊢j\in {\mathbb{Z}}_{\ge M}\to j\in \mathbb{Z}$$
3		uzid	$$⊢j\in \mathbb{Z}\to j\in {\mathbb{Z}}_{\ge j}$$
4		ne0i	$$⊢j\in {\mathbb{Z}}_{\ge j}\to {\mathbb{Z}}_{\ge j}\ne \varnothing$$
5	2 3 4	3syl	$$⊢j\in {\mathbb{Z}}_{\ge M}\to {\mathbb{Z}}_{\ge j}\ne \varnothing$$
6	5 1	eleq2s	$$⊢j\in Z\to {\mathbb{Z}}_{\ge j}\ne \varnothing$$
7		r19.2z	$$⊢\left({\mathbb{Z}}_{\ge j}\ne \varnothing \wedge \forall k\in {\mathbb{Z}}_{\ge j}\phi \right)\to \exists k\in {\mathbb{Z}}_{\ge j}\phi$$
8	6 7	sylan	$$⊢\left(j\in Z\wedge \forall k\in {\mathbb{Z}}_{\ge j}\phi \right)\to \exists k\in {\mathbb{Z}}_{\ge j}\phi$$
9	1	uztrn2	$$⊢\left(j\in Z\wedge k\in {\mathbb{Z}}_{\ge j}\right)\to k\in Z$$
10	9	ex	$$⊢j\in Z\to \left(k\in {\mathbb{Z}}_{\ge j}\to k\in Z\right)$$
11	10	anim1d	$$⊢j\in Z\to \left(\left(k\in {\mathbb{Z}}_{\ge j}\wedge \phi \right)\to \left(k\in Z\wedge \phi \right)\right)$$
12	11	reximdv2	$$⊢j\in Z\to \left(\exists k\in {\mathbb{Z}}_{\ge j}\phi \to \exists k\in Z\phi \right)$$
13	12	imp	$$⊢\left(j\in Z\wedge \exists k\in {\mathbb{Z}}_{\ge j}\phi \right)\to \exists k\in Z\phi$$
14	8 13	syldan	$$⊢\left(j\in Z\wedge \forall k\in {\mathbb{Z}}_{\ge j}\phi \right)\to \exists k\in Z\phi$$
15	14	rexlimiva	$$⊢\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\phi \to \exists k\in Z\phi$$