| Mathbox for BJ |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > Mathboxes > bj-bdfindis | GIF version | ||
| Description: Bounded induction (principle of induction for bounded formulas), using implicit substitutions (the biconditional versions of the hypotheses are implicit substitutions, and we have weakened them to implications). Constructive proof (from CZF). See finds 4647 for a proof of full induction in IZF. From this version, it is easy to prove bounded versions of finds 4647, finds2 4648, finds1 4649. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) |
| Ref | Expression |
|---|---|
| bj-bdfindis.bd | ⊢ BOUNDED 𝜑 |
| bj-bdfindis.nf0 | ⊢ Ⅎ𝑥𝜓 |
| bj-bdfindis.nf1 | ⊢ Ⅎ𝑥𝜒 |
| bj-bdfindis.nfsuc | ⊢ Ⅎ𝑥𝜃 |
| bj-bdfindis.0 | ⊢ (𝑥 = ∅ → (𝜓 → 𝜑)) |
| bj-bdfindis.1 | ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜒)) |
| bj-bdfindis.suc | ⊢ (𝑥 = suc 𝑦 → (𝜃 → 𝜑)) |
| Ref | Expression |
|---|---|
| bj-bdfindis | ⊢ ((𝜓 ∧ ∀𝑦 ∈ ω (𝜒 → 𝜃)) → ∀𝑥 ∈ ω 𝜑) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bj-bdfindis.nf0 | . . . 4 ⊢ Ⅎ𝑥𝜓 | |
| 2 | 0ex 4170 | . . . 4 ⊢ ∅ ∈ V | |
| 3 | bj-bdfindis.0 | . . . 4 ⊢ (𝑥 = ∅ → (𝜓 → 𝜑)) | |
| 4 | 1, 2, 3 | elabf2 15680 | . . 3 ⊢ (𝜓 → ∅ ∈ {𝑥 ∣ 𝜑}) |
| 5 | bj-bdfindis.nf1 | . . . . . 6 ⊢ Ⅎ𝑥𝜒 | |
| 6 | bj-bdfindis.1 | . . . . . 6 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜒)) | |
| 7 | 5, 6 | elabf1 15679 | . . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} → 𝜒) |
| 8 | bj-bdfindis.nfsuc | . . . . . 6 ⊢ Ⅎ𝑥𝜃 | |
| 9 | vex 2774 | . . . . . . 7 ⊢ 𝑦 ∈ V | |
| 10 | 9 | bj-sucex 15821 | . . . . . 6 ⊢ suc 𝑦 ∈ V |
| 11 | bj-bdfindis.suc | . . . . . 6 ⊢ (𝑥 = suc 𝑦 → (𝜃 → 𝜑)) | |
| 12 | 8, 10, 11 | elabf2 15680 | . . . . 5 ⊢ (𝜃 → suc 𝑦 ∈ {𝑥 ∣ 𝜑}) |
| 13 | 7, 12 | imim12i 59 | . . . 4 ⊢ ((𝜒 → 𝜃) → (𝑦 ∈ {𝑥 ∣ 𝜑} → suc 𝑦 ∈ {𝑥 ∣ 𝜑})) |
| 14 | 13 | ralimi 2568 | . . 3 ⊢ (∀𝑦 ∈ ω (𝜒 → 𝜃) → ∀𝑦 ∈ ω (𝑦 ∈ {𝑥 ∣ 𝜑} → suc 𝑦 ∈ {𝑥 ∣ 𝜑})) |
| 15 | bj-bdfindis.bd | . . . . 5 ⊢ BOUNDED 𝜑 | |
| 16 | 15 | bdcab 15747 | . . . 4 ⊢ BOUNDED {𝑥 ∣ 𝜑} |
| 17 | 16 | bdpeano5 15841 | . . 3 ⊢ ((∅ ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑦 ∈ ω (𝑦 ∈ {𝑥 ∣ 𝜑} → suc 𝑦 ∈ {𝑥 ∣ 𝜑})) → ω ⊆ {𝑥 ∣ 𝜑}) |
| 18 | 4, 14, 17 | syl2an 289 | . 2 ⊢ ((𝜓 ∧ ∀𝑦 ∈ ω (𝜒 → 𝜃)) → ω ⊆ {𝑥 ∣ 𝜑}) |
| 19 | ssabral 3263 | . 2 ⊢ (ω ⊆ {𝑥 ∣ 𝜑} ↔ ∀𝑥 ∈ ω 𝜑) | |
| 20 | 18, 19 | sylib 122 | 1 ⊢ ((𝜓 ∧ ∀𝑦 ∈ ω (𝜒 → 𝜃)) → ∀𝑥 ∈ ω 𝜑) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ∧ wa 104 = wceq 1372 Ⅎwnf 1482 ∈ wcel 2175 {cab 2190 ∀wral 2483 ⊆ wss 3165 ∅c0 3459 suc csuc 4411 ωcom 4637 BOUNDED wbd 15710 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1469 ax-7 1470 ax-gen 1471 ax-ie1 1515 ax-ie2 1516 ax-8 1526 ax-10 1527 ax-11 1528 ax-i12 1529 ax-bndl 1531 ax-4 1532 ax-17 1548 ax-i9 1552 ax-ial 1556 ax-i5r 1557 ax-13 2177 ax-14 2178 ax-ext 2186 ax-nul 4169 ax-pr 4252 ax-un 4479 ax-bd0 15711 ax-bdor 15714 ax-bdex 15717 ax-bdeq 15718 ax-bdel 15719 ax-bdsb 15720 ax-bdsep 15782 ax-infvn 15839 |
| This theorem depends on definitions: df-bi 117 df-tru 1375 df-nf 1483 df-sb 1785 df-clab 2191 df-cleq 2197 df-clel 2200 df-nfc 2336 df-ral 2488 df-rex 2489 df-rab 2492 df-v 2773 df-dif 3167 df-un 3169 df-in 3171 df-ss 3178 df-nul 3460 df-sn 3638 df-pr 3639 df-uni 3850 df-int 3885 df-suc 4417 df-iom 4638 df-bdc 15739 df-bj-ind 15825 |
| This theorem is referenced by: bj-bdfindisg 15846 bj-bdfindes 15847 bj-nn0suc0 15848 |
| Copyright terms: Public domain | W3C validator |