![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > finds1 | GIF version |
Description: Principle of Finite Induction (inference schema), using implicit substitutions. The first three hypotheses establish the substitutions we need. The last two are the basis and the induction step. Theorem Schema 22 of [Suppes] p. 136. (Contributed by NM, 22-Mar-2006.) |
Ref | Expression |
---|---|
finds1.1 | ⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) |
finds1.2 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) |
finds1.3 | ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)) |
finds1.4 | ⊢ 𝜓 |
finds1.5 | ⊢ (𝑦 ∈ ω → (𝜒 → 𝜃)) |
Ref | Expression |
---|---|
finds1 | ⊢ (𝑥 ∈ ω → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2082 | . 2 ⊢ ∅ = ∅ | |
2 | finds1.1 | . . 3 ⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) | |
3 | finds1.2 | . . 3 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) | |
4 | finds1.3 | . . 3 ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)) | |
5 | finds1.4 | . . . 4 ⊢ 𝜓 | |
6 | 5 | a1i 9 | . . 3 ⊢ (∅ = ∅ → 𝜓) |
7 | finds1.5 | . . . 4 ⊢ (𝑦 ∈ ω → (𝜒 → 𝜃)) | |
8 | 7 | a1d 22 | . . 3 ⊢ (𝑦 ∈ ω → (∅ = ∅ → (𝜒 → 𝜃))) |
9 | 2, 3, 4, 6, 8 | finds2 4350 | . 2 ⊢ (𝑥 ∈ ω → (∅ = ∅ → 𝜑)) |
10 | 1, 9 | mpi 15 | 1 ⊢ (𝑥 ∈ ω → 𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 103 = wceq 1285 ∈ wcel 1434 ∅c0 3258 suc csuc 4128 ωcom 4339 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-13 1445 ax-14 1446 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2064 ax-sep 3904 ax-nul 3912 ax-pow 3956 ax-pr 3972 ax-un 4196 ax-iinf 4337 |
This theorem depends on definitions: df-bi 115 df-3an 922 df-tru 1288 df-nf 1391 df-sb 1687 df-clab 2069 df-cleq 2075 df-clel 2078 df-nfc 2209 df-ral 2354 df-rex 2355 df-v 2604 df-dif 2976 df-un 2978 df-in 2980 df-ss 2987 df-nul 3259 df-pw 3392 df-sn 3412 df-pr 3413 df-uni 3610 df-int 3645 df-suc 4134 df-iom 4340 |
This theorem is referenced by: findcard 6422 findcard2 6423 findcard2s 6424 |
Copyright terms: Public domain | W3C validator |