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 = ℤ_{\geq M}$
	Assertion	r19.2uz	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} φ \to \exists k \in Z φ$

Step	Hyp	Ref	Expression
1		rexuz3.1	$⊢ Z = ℤ_{\geq M}$
2		eluzelz	$⊢ j \in ℤ_{\geq M} \to j \in ℤ$
3		uzid	$⊢ j \in ℤ \to j \in ℤ_{\geq j}$
4		ne0i	$⊢ j \in ℤ_{\geq j} \to ℤ_{\geq j} \neq \emptyset$
5	2 3 4	3syl	$⊢ j \in ℤ_{\geq M} \to ℤ_{\geq j} \neq \emptyset$
6	5 1	eleq2s	$⊢ j \in Z \to ℤ_{\geq j} \neq \emptyset$
7		r19.2z	$⊢ (ℤ_{\geq j} \neq \emptyset \land \forall k \in ℤ_{\geq j} φ) \to \exists k \in ℤ_{\geq j} φ$
8	6 7	sylan	$⊢ (j \in Z \land \forall k \in ℤ_{\geq j} φ) \to \exists k \in ℤ_{\geq j} φ$
9	1	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
10	9	ex	$⊢ j \in Z \to (k \in ℤ_{\geq j} \to k \in Z)$
11	10	anim1d	$⊢ j \in Z \to ((k \in ℤ_{\geq j} \land φ) \to (k \in Z \land φ))$
12	11	reximdv2	$⊢ j \in Z \to (\exists k \in ℤ_{\geq j} φ \to \exists k \in Z φ)$
13	12	imp	$⊢ (j \in Z \land \exists k \in ℤ_{\geq j} φ) \to \exists k \in Z φ$
14	8 13	syldan	$⊢ (j \in Z \land \forall k \in ℤ_{\geq j} φ) \to \exists k \in Z φ$
15	14	rexlimiva	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} φ \to \exists k \in Z φ$

Metamath Proof Explorer