Metamath Proof Explorer

Theorem raluz2

Description: Restricted universal quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005)

Ref Expression
Assertion raluz2 ⊢ ∀ n ∈ ℤ ≥ M φ ↔ M ∈ ℤ → ∀ n ∈ ℤ M ≤ n → φ

Proof

Step Hyp Ref Expression
1 eluz2 ⊢ n ∈ ℤ ≥ M ↔ M ∈ ℤ ∧ n ∈ ℤ ∧ M ≤ n
2 3anass ⊢ M ∈ ℤ ∧ n ∈ ℤ ∧ M ≤ n ↔ M ∈ ℤ ∧ n ∈ ℤ ∧ M ≤ n
3 1 2 bitri ⊢ n ∈ ℤ ≥ M ↔ M ∈ ℤ ∧ n ∈ ℤ ∧ M ≤ n
4 3 imbi1i ⊢ n ∈ ℤ ≥ M → φ ↔ M ∈ ℤ ∧ n ∈ ℤ ∧ M ≤ n → φ
5 impexp ⊢ M ∈ ℤ ∧ n ∈ ℤ ∧ M ≤ n → φ ↔ M ∈ ℤ → n ∈ ℤ ∧ M ≤ n → φ
6 impexp ⊢ n ∈ ℤ ∧ M ≤ n → φ ↔ n ∈ ℤ → M ≤ n → φ
7 6 imbi2i ⊢ M ∈ ℤ → n ∈ ℤ ∧ M ≤ n → φ ↔ M ∈ ℤ → n ∈ ℤ → M ≤ n → φ
8 5 7 bitri ⊢ M ∈ ℤ ∧ n ∈ ℤ ∧ M ≤ n → φ ↔ M ∈ ℤ → n ∈ ℤ → M ≤ n → φ
9 bi2.04 ⊢ M ∈ ℤ → n ∈ ℤ → M ≤ n → φ ↔ n ∈ ℤ → M ∈ ℤ → M ≤ n → φ
10 8 9 bitri ⊢ M ∈ ℤ ∧ n ∈ ℤ ∧ M ≤ n → φ ↔ n ∈ ℤ → M ∈ ℤ → M ≤ n → φ
11 4 10 bitri ⊢ n ∈ ℤ ≥ M → φ ↔ n ∈ ℤ → M ∈ ℤ → M ≤ n → φ
12 11 ralbii2 ⊢ ∀ n ∈ ℤ ≥ M φ ↔ ∀ n ∈ ℤ M ∈ ℤ → M ≤ n → φ
13 r19.21v ⊢ ∀ n ∈ ℤ M ∈ ℤ → M ≤ n → φ ↔ M ∈ ℤ → ∀ n ∈ ℤ M ≤ n → φ
14 12 13 bitri ⊢ ∀ n ∈ ℤ ≥ M φ ↔ M ∈ ℤ → ∀ n ∈ ℤ M ≤ n → φ