![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nnind | GIF version |
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 7715 for an example of its use. This is an alternative for Metamath 100 proof #74. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 16-Jun-2013.) |
Ref | Expression |
---|---|
nnind.1 | ⊢ (x = 1 → (φ ↔ ψ)) |
nnind.2 | ⊢ (x = y → (φ ↔ χ)) |
nnind.3 | ⊢ (x = (y + 1) → (φ ↔ θ)) |
nnind.4 | ⊢ (x = A → (φ ↔ τ)) |
nnind.5 | ⊢ ψ |
nnind.6 | ⊢ (y ∈ ℕ → (χ → θ)) |
Ref | Expression |
---|---|
nnind | ⊢ (A ∈ ℕ → τ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1nn 7706 | . . . . . 6 ⊢ 1 ∈ ℕ | |
2 | nnind.5 | . . . . . 6 ⊢ ψ | |
3 | nnind.1 | . . . . . . 7 ⊢ (x = 1 → (φ ↔ ψ)) | |
4 | 3 | elrab 2692 | . . . . . 6 ⊢ (1 ∈ {x ∈ ℕ ∣ φ} ↔ (1 ∈ ℕ ∧ ψ)) |
5 | 1, 2, 4 | mpbir2an 848 | . . . . 5 ⊢ 1 ∈ {x ∈ ℕ ∣ φ} |
6 | elrabi 2689 | . . . . . . 7 ⊢ (y ∈ {x ∈ ℕ ∣ φ} → y ∈ ℕ) | |
7 | peano2nn 7707 | . . . . . . . . . 10 ⊢ (y ∈ ℕ → (y + 1) ∈ ℕ) | |
8 | 7 | a1d 22 | . . . . . . . . 9 ⊢ (y ∈ ℕ → (y ∈ ℕ → (y + 1) ∈ ℕ)) |
9 | nnind.6 | . . . . . . . . 9 ⊢ (y ∈ ℕ → (χ → θ)) | |
10 | 8, 9 | anim12d 318 | . . . . . . . 8 ⊢ (y ∈ ℕ → ((y ∈ ℕ ∧ χ) → ((y + 1) ∈ ℕ ∧ θ))) |
11 | nnind.2 | . . . . . . . . 9 ⊢ (x = y → (φ ↔ χ)) | |
12 | 11 | elrab 2692 | . . . . . . . 8 ⊢ (y ∈ {x ∈ ℕ ∣ φ} ↔ (y ∈ ℕ ∧ χ)) |
13 | nnind.3 | . . . . . . . . 9 ⊢ (x = (y + 1) → (φ ↔ θ)) | |
14 | 13 | elrab 2692 | . . . . . . . 8 ⊢ ((y + 1) ∈ {x ∈ ℕ ∣ φ} ↔ ((y + 1) ∈ ℕ ∧ θ)) |
15 | 10, 12, 14 | 3imtr4g 194 | . . . . . . 7 ⊢ (y ∈ ℕ → (y ∈ {x ∈ ℕ ∣ φ} → (y + 1) ∈ {x ∈ ℕ ∣ φ})) |
16 | 6, 15 | mpcom 32 | . . . . . 6 ⊢ (y ∈ {x ∈ ℕ ∣ φ} → (y + 1) ∈ {x ∈ ℕ ∣ φ}) |
17 | 16 | rgen 2368 | . . . . 5 ⊢ ∀y ∈ {x ∈ ℕ ∣ φ} (y + 1) ∈ {x ∈ ℕ ∣ φ} |
18 | peano5nni 7698 | . . . . 5 ⊢ ((1 ∈ {x ∈ ℕ ∣ φ} ∧ ∀y ∈ {x ∈ ℕ ∣ φ} (y + 1) ∈ {x ∈ ℕ ∣ φ}) → ℕ ⊆ {x ∈ ℕ ∣ φ}) | |
19 | 5, 17, 18 | mp2an 402 | . . . 4 ⊢ ℕ ⊆ {x ∈ ℕ ∣ φ} |
20 | 19 | sseli 2935 | . . 3 ⊢ (A ∈ ℕ → A ∈ {x ∈ ℕ ∣ φ}) |
21 | nnind.4 | . . . 4 ⊢ (x = A → (φ ↔ τ)) | |
22 | 21 | elrab 2692 | . . 3 ⊢ (A ∈ {x ∈ ℕ ∣ φ} ↔ (A ∈ ℕ ∧ τ)) |
23 | 20, 22 | sylib 127 | . 2 ⊢ (A ∈ ℕ → (A ∈ ℕ ∧ τ)) |
24 | 23 | simprd 107 | 1 ⊢ (A ∈ ℕ → τ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ↔ wb 98 = wceq 1242 ∈ wcel 1390 ∀wral 2300 {crab 2304 ⊆ wss 2911 (class class class)co 5455 1c1 6712 + caddc 6714 ℕcn 7695 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-io 629 ax-5 1333 ax-7 1334 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-8 1392 ax-10 1393 ax-11 1394 ax-i12 1395 ax-bndl 1396 ax-4 1397 ax-17 1416 ax-i9 1420 ax-ial 1424 ax-i5r 1425 ax-ext 2019 ax-sep 3866 ax-cnex 6774 ax-resscn 6775 ax-1re 6777 ax-addrcl 6780 |
This theorem depends on definitions: df-bi 110 df-3an 886 df-tru 1245 df-nf 1347 df-sb 1643 df-clab 2024 df-cleq 2030 df-clel 2033 df-nfc 2164 df-ral 2305 df-rex 2306 df-rab 2309 df-v 2553 df-un 2916 df-in 2918 df-ss 2925 df-sn 3373 df-pr 3374 df-op 3376 df-uni 3572 df-int 3607 df-br 3756 df-iota 4810 df-fv 4853 df-ov 5458 df-inn 7696 |
This theorem is referenced by: nnindALT 7712 nn1m1nn 7713 nnaddcl 7715 nnmulcl 7716 nnge1 7718 nn1gt1 7728 nnsub 7733 zaddcllempos 8058 zaddcllemneg 8060 nneoor 8116 peano5uzti 8122 nn0ind-raph 8131 indstr 8312 expivallem 8910 expcllem 8920 expap0 8939 |
Copyright terms: Public domain | W3C validator |