This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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