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	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
Assertion	r19.2uz	⊢ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 → ∃ 𝑘 ∈ 𝑍 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		rexuz3.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		eluzelz	⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑗 ∈ ℤ )
3		uzid	⊢ ( 𝑗 ∈ ℤ → 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) )
4		ne0i	⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) → ( ℤ≥ ‘ 𝑗 ) ≠ ∅ )
5	2 3 4	3syl	⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ 𝑗 ) ≠ ∅ )
6	5 1	eleq2s	⊢ ( 𝑗 ∈ 𝑍 → ( ℤ≥ ‘ 𝑗 ) ≠ ∅ )
7		r19.2z	⊢ ( ( ( ℤ≥ ‘ 𝑗 ) ≠ ∅ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) → ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 )
8	6 7	sylan	⊢ ( ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) → ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 )
9	1	uztrn2	⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
10	9	ex	⊢ ( 𝑗 ∈ 𝑍 → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) → 𝑘 ∈ 𝑍 ) )
11	10	anim1d	⊢ ( 𝑗 ∈ 𝑍 → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝜑 ) → ( 𝑘 ∈ 𝑍 ∧ 𝜑 ) ) )
12	11	reximdv2	⊢ ( 𝑗 ∈ 𝑍 → ( ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 → ∃ 𝑘 ∈ 𝑍 𝜑 ) )
13	12	imp	⊢ ( ( 𝑗 ∈ 𝑍 ∧ ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) → ∃ 𝑘 ∈ 𝑍 𝜑 )
14	8 13	syldan	⊢ ( ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) → ∃ 𝑘 ∈ 𝑍 𝜑 )
15	14	rexlimiva	⊢ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 → ∃ 𝑘 ∈ 𝑍 𝜑 )