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

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 ( ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) 𝜑 ↔ ( 𝑀 ∈ ℤ → ∀ 𝑛 ∈ ℤ ( 𝑀 ≤ 𝑛 → 𝜑 ) ) )

Proof

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