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

Metamath Proof Explorer

Theorem nnind

Description: Principle of Mathematical Induction (inference schema). The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. See nnaddcl for an example of its use. See nn0ind for induction on nonnegative integers and uzind , uzind4 for induction on an arbitrary upper set of integers. See indstr for strong induction. See also nnindALT . This is an alternative for Metamath 100 proof #74. (Contributed by NM, 10-Jan-1997) (Revised by Mario Carneiro, 16-Jun-2013)

Ref Expression
Hypotheses nnind.1 ⊢ x = 1 → φ ↔ ψ
nnind.2 ⊢ x = y → φ ↔ χ
nnind.3 ⊢ x = y + 1 → φ ↔ θ
nnind.4 ⊢ x = A → φ ↔ τ
nnind.5 ⊢ ψ
nnind.6 ⊢ y ∈ ℕ → χ → θ
Assertion nnind ⊢ A ∈ ℕ → τ

Proof

Step Hyp Ref Expression
1 nnind.1 ⊢ x = 1 → φ ↔ ψ
2 nnind.2 ⊢ x = y → φ ↔ χ
3 nnind.3 ⊢ x = y + 1 → φ ↔ θ
4 nnind.4 ⊢ x = A → φ ↔ τ
5 nnind.5 ⊢ ψ
6 nnind.6 ⊢ y ∈ ℕ → χ → θ
7 1nn ⊢ 1 ∈ ℕ
8 1 elrab ⊢ 1 ∈ x ∈ ℕ | φ ↔ 1 ∈ ℕ ∧ ψ
9 7 5 8 mpbir2an ⊢ 1 ∈ x ∈ ℕ | φ
10 elrabi ⊢ y ∈ x ∈ ℕ | φ → y ∈ ℕ
11 peano2nn ⊢ y ∈ ℕ → y + 1 ∈ ℕ
12 11 a1d ⊢ y ∈ ℕ → y ∈ ℕ → y + 1 ∈ ℕ
13 12 6 anim12d ⊢ y ∈ ℕ → y ∈ ℕ ∧ χ → y + 1 ∈ ℕ ∧ θ
14 2 elrab ⊢ y ∈ x ∈ ℕ | φ ↔ y ∈ ℕ ∧ χ
15 3 elrab ⊢ y + 1 ∈ x ∈ ℕ | φ ↔ y + 1 ∈ ℕ ∧ θ
16 13 14 15 3imtr4g ⊢ y ∈ ℕ → y ∈ x ∈ ℕ | φ → y + 1 ∈ x ∈ ℕ | φ
17 10 16 mpcom ⊢ y ∈ x ∈ ℕ | φ → y + 1 ∈ x ∈ ℕ | φ
18 17 rgen ⊢ ∀ y ∈ x ∈ ℕ | φ y + 1 ∈ x ∈ ℕ | φ
19 peano5nni ⊢ 1 ∈ x ∈ ℕ | φ ∧ ∀ y ∈ x ∈ ℕ | φ y + 1 ∈ x ∈ ℕ | φ → ℕ ⊆ x ∈ ℕ | φ
20 9 18 19 mp2an ⊢ ℕ ⊆ x ∈ ℕ | φ
21 20 sseli ⊢ A ∈ ℕ → A ∈ x ∈ ℕ | φ
22 4 elrab ⊢ A ∈ x ∈ ℕ | φ ↔ A ∈ ℕ ∧ τ
23 21 22 sylib ⊢ A ∈ ℕ → A ∈ ℕ ∧ τ
24 23 simprd ⊢ A ∈ ℕ → τ