r19.29uz

Description: A version of 19.29 for upper integer quantifiers. (Contributed by Mario Carneiro, 10-Feb-2014)

		Ref	Expression
	Hypothesis	rexuz3.1	$⊢ Z = ℤ_{\geq M}$
	Assertion	r19.29uz	$⊢ (\forall k \in Z φ \land \exists j \in Z \forall k \in ℤ_{\geq j} ψ) \to \exists j \in Z \forall k \in ℤ_{\geq j} (φ \land ψ)$

Step	Hyp	Ref	Expression
1		rexuz3.1	$⊢ Z = ℤ_{\geq M}$
2	1	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
3	2	ex	$⊢ j \in Z \to (k \in ℤ_{\geq j} \to k \in Z)$
4		pm3.2	$⊢ φ \to (ψ \to (φ \land ψ))$
5	4	a1i	$⊢ j \in Z \to (φ \to (ψ \to (φ \land ψ)))$
6	3 5	imim12d	$⊢ j \in Z \to ((k \in Z \to φ) \to (k \in ℤ_{\geq j} \to (ψ \to (φ \land ψ))))$
7	6	ralimdv2	$⊢ j \in Z \to (\forall k \in Z φ \to \forall k \in ℤ_{\geq j} (ψ \to (φ \land ψ)))$
8	7	impcom	$⊢ (\forall k \in Z φ \land j \in Z) \to \forall k \in ℤ_{\geq j} (ψ \to (φ \land ψ))$
9		ralim	$⊢ \forall k \in ℤ_{\geq j} (ψ \to (φ \land ψ)) \to (\forall k \in ℤ_{\geq j} ψ \to \forall k \in ℤ_{\geq j} (φ \land ψ))$
10	8 9	syl	$⊢ (\forall k \in Z φ \land j \in Z) \to (\forall k \in ℤ_{\geq j} ψ \to \forall k \in ℤ_{\geq j} (φ \land ψ))$
11	10	reximdva	$⊢ \forall k \in Z φ \to (\exists j \in Z \forall k \in ℤ_{\geq j} ψ \to \exists j \in Z \forall k \in ℤ_{\geq j} (φ \land ψ))$
12	11	imp	$⊢ (\forall k \in Z φ \land \exists j \in Z \forall k \in ℤ_{\geq j} ψ) \to \exists j \in Z \forall k \in ℤ_{\geq j} (φ \land ψ)$

Metamath Proof Explorer