Metamath Proof Explorer

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}={ℤ}_{\ge {M}}$
Assertion r19.2uz ${⊢}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {k}\in {Z}\phantom{\rule{.4em}{0ex}}{\phi }$

Proof

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