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

Metamath Proof Explorer

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