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

Metamath Proof Explorer

Theorem rexanuz2

Description: Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 26-Dec-2013)

Ref Expression
Hypothesis rexuz3.1 ⊢ Z = ℤ ≥ M
Assertion rexanuz2 ⊢ ∃ j ∈ Z ∀ k ∈ ℤ ≥ j φ ∧ ψ ↔ ∃ j ∈ Z ∀ k ∈ ℤ ≥ j φ ∧ ∃ j ∈ Z ∀ k ∈ ℤ ≥ j ψ

Proof

Step Hyp Ref Expression
1 rexuz3.1 ⊢ Z = ℤ ≥ M
2 eluzel2 ⊢ j ∈ ℤ ≥ M → M ∈ ℤ
3 2 1 eleq2s ⊢ j ∈ Z → M ∈ ℤ
4 3 a1d ⊢ j ∈ Z → ∀ k ∈ ℤ ≥ j φ ∧ ψ → M ∈ ℤ
5 4 rexlimiv ⊢ ∃ j ∈ Z ∀ k ∈ ℤ ≥ j φ ∧ ψ → M ∈ ℤ
6 3 a1d ⊢ j ∈ Z → ∀ k ∈ ℤ ≥ j φ → M ∈ ℤ
7 6 rexlimiv ⊢ ∃ j ∈ Z ∀ k ∈ ℤ ≥ j φ → M ∈ ℤ
8 7 adantr ⊢ ∃ j ∈ Z ∀ k ∈ ℤ ≥ j φ ∧ ∃ j ∈ Z ∀ k ∈ ℤ ≥ j ψ → M ∈ ℤ
9 1 rexuz3 ⊢ M ∈ ℤ → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j φ ∧ ψ ↔ ∃ j ∈ ℤ ∀ k ∈ ℤ ≥ j φ ∧ ψ
10 rexanuz ⊢ ∃ j ∈ ℤ ∀ k ∈ ℤ ≥ j φ ∧ ψ ↔ ∃ j ∈ ℤ ∀ k ∈ ℤ ≥ j φ ∧ ∃ j ∈ ℤ ∀ k ∈ ℤ ≥ j ψ
11 1 rexuz3 ⊢ M ∈ ℤ → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j φ ↔ ∃ j ∈ ℤ ∀ k ∈ ℤ ≥ j φ
12 1 rexuz3 ⊢ M ∈ ℤ → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j ψ ↔ ∃ j ∈ ℤ ∀ k ∈ ℤ ≥ j ψ
13 11 12 anbi12d ⊢ M ∈ ℤ → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j φ ∧ ∃ j ∈ Z ∀ k ∈ ℤ ≥ j ψ ↔ ∃ j ∈ ℤ ∀ k ∈ ℤ ≥ j φ ∧ ∃ j ∈ ℤ ∀ k ∈ ℤ ≥ j ψ
14 10 13 bitr4id ⊢ M ∈ ℤ → ∃ j ∈ ℤ ∀ k ∈ ℤ ≥ j φ ∧ ψ ↔ ∃ j ∈ Z ∀ k ∈ ℤ ≥ j φ ∧ ∃ j ∈ Z ∀ k ∈ ℤ ≥ j ψ
15 9 14 bitrd ⊢ M ∈ ℤ → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j φ ∧ ψ ↔ ∃ j ∈ Z ∀ k ∈ ℤ ≥ j φ ∧ ∃ j ∈ Z ∀ k ∈ ℤ ≥ j ψ
16 5 8 15 pm5.21nii ⊢ ∃ j ∈ Z ∀ k ∈ ℤ ≥ j φ ∧ ψ ↔ ∃ j ∈ Z ∀ k ∈ ℤ ≥ j φ ∧ ∃ j ∈ Z ∀ k ∈ ℤ ≥ j ψ