Theorem r19.29uz

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

	Ref	Expression
Hypothesis	rexuz3.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
Assertion	r19.29uz	⊢ ( ( ∀ 𝑘 ∈ 𝑍 𝜑 ∧ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜑 ∧ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		rexuz3.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2	1	uztrn2	⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
3	2	ex	⊢ ( 𝑗 ∈ 𝑍 → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) → 𝑘 ∈ 𝑍 ) )
4		pm3.2	⊢ ( 𝜑 → ( 𝜓 → ( 𝜑 ∧ 𝜓 ) ) )
5	4	a1i	⊢ ( 𝑗 ∈ 𝑍 → ( 𝜑 → ( 𝜓 → ( 𝜑 ∧ 𝜓 ) ) ) )
6	3 5	imim12d	⊢ ( 𝑗 ∈ 𝑍 → ( ( 𝑘 ∈ 𝑍 → 𝜑 ) → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) → ( 𝜓 → ( 𝜑 ∧ 𝜓 ) ) ) ) )
7	6	ralimdv2	⊢ ( 𝑗 ∈ 𝑍 → ( ∀ 𝑘 ∈ 𝑍 𝜑 → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜓 → ( 𝜑 ∧ 𝜓 ) ) ) )
8	7	impcom	⊢ ( ( ∀ 𝑘 ∈ 𝑍 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜓 → ( 𝜑 ∧ 𝜓 ) ) )
9		ralim	⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜓 → ( 𝜑 ∧ 𝜓 ) ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜑 ∧ 𝜓 ) ) )
10	8 9	syl	⊢ ( ( ∀ 𝑘 ∈ 𝑍 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜑 ∧ 𝜓 ) ) )
11	10	reximdva	⊢ ( ∀ 𝑘 ∈ 𝑍 𝜑 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜑 ∧ 𝜓 ) ) )
12	11	imp	⊢ ( ( ∀ 𝑘 ∈ 𝑍 𝜑 ∧ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜓 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝜑 ∧ 𝜓 ) )