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

Metamath Proof Explorer

Theorem uzind4

Description: Induction on the upper set of integers that starts at an integer M . The first four hypotheses give us the substitution instances we need, and the last two are the basis and the induction step. (Contributed by NM, 7-Sep-2005)

Ref Expression
Hypotheses uzind4.1 ⊢ j = M → φ ↔ ψ
uzind4.2 ⊢ j = k → φ ↔ χ
uzind4.3 ⊢ j = k + 1 → φ ↔ θ
uzind4.4 ⊢ j = N → φ ↔ τ
uzind4.5 ⊢ M ∈ ℤ → ψ
uzind4.6 ⊢ k ∈ ℤ ≥ M → χ → θ
Assertion uzind4 ⊢ N ∈ ℤ ≥ M → τ

Proof

Step Hyp Ref Expression
1 uzind4.1 ⊢ j = M → φ ↔ ψ
2 uzind4.2 ⊢ j = k → φ ↔ χ
3 uzind4.3 ⊢ j = k + 1 → φ ↔ θ
4 uzind4.4 ⊢ j = N → φ ↔ τ
5 uzind4.5 ⊢ M ∈ ℤ → ψ
6 uzind4.6 ⊢ k ∈ ℤ ≥ M → χ → θ
7 eluzel2 ⊢ N ∈ ℤ ≥ M → M ∈ ℤ
8 breq2 ⊢ m = N → M ≤ m ↔ M ≤ N
9 eluzelz ⊢ N ∈ ℤ ≥ M → N ∈ ℤ
10 eluzle ⊢ N ∈ ℤ ≥ M → M ≤ N
11 8 9 10 elrabd ⊢ N ∈ ℤ ≥ M → N ∈ m ∈ ℤ | M ≤ m
12 breq2 ⊢ m = k → M ≤ m ↔ M ≤ k
13 12 elrab ⊢ k ∈ m ∈ ℤ | M ≤ m ↔ k ∈ ℤ ∧ M ≤ k
14 eluz2 ⊢ k ∈ ℤ ≥ M ↔ M ∈ ℤ ∧ k ∈ ℤ ∧ M ≤ k
15 14 biimpri ⊢ M ∈ ℤ ∧ k ∈ ℤ ∧ M ≤ k → k ∈ ℤ ≥ M
16 15 3expb ⊢ M ∈ ℤ ∧ k ∈ ℤ ∧ M ≤ k → k ∈ ℤ ≥ M
17 13 16 sylan2b ⊢ M ∈ ℤ ∧ k ∈ m ∈ ℤ | M ≤ m → k ∈ ℤ ≥ M
18 17 6 syl ⊢ M ∈ ℤ ∧ k ∈ m ∈ ℤ | M ≤ m → χ → θ
19 1 2 3 4 5 18 uzind3 ⊢ M ∈ ℤ ∧ N ∈ m ∈ ℤ | M ≤ m → τ
20 7 11 19 syl2anc ⊢ N ∈ ℤ ≥ M → τ