| 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 4648 for a proof of full induction in IZF. From this version, it is easy to prove bounded versions of finds 4648, finds2 4649, finds1 4650. (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 4171 | . . . 4 ⊢ ∅ ∈ V | |
| 3 | bj-bdfindis.0 | . . . 4 ⊢ (𝑥 = ∅ → (𝜓 → 𝜑)) | |
| 4 | 1, 2, 3 | elabf2 15718 | . . 3 ⊢ (𝜓 → ∅ ∈ {𝑥 ∣ 𝜑}) |
| 5 | bj-bdfindis.nf1 | . . . . . 6 ⊢ Ⅎ𝑥𝜒 | |
| 6 | bj-bdfindis.1 | . . . . . 6 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜒)) | |
| 7 | 5, 6 | elabf1 15717 | . . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} → 𝜒) |
| 8 | bj-bdfindis.nfsuc | . . . . . 6 ⊢ Ⅎ𝑥𝜃 | |
| 9 | vex 2775 | . . . . . . 7 ⊢ 𝑦 ∈ V | |
| 10 | 9 | bj-sucex 15859 | . . . . . 6 ⊢ suc 𝑦 ∈ V |
| 11 | bj-bdfindis.suc | . . . . . 6 ⊢ (𝑥 = suc 𝑦 → (𝜃 → 𝜑)) | |
| 12 | 8, 10, 11 | elabf2 15718 | . . . . 5 ⊢ (𝜃 → suc 𝑦 ∈ {𝑥 ∣ 𝜑}) |
| 13 | 7, 12 | imim12i 59 | . . . 4 ⊢ ((𝜒 → 𝜃) → (𝑦 ∈ {𝑥 ∣ 𝜑} → suc 𝑦 ∈ {𝑥 ∣ 𝜑})) |
| 14 | 13 | ralimi 2569 | . . 3 ⊢ (∀𝑦 ∈ ω (𝜒 → 𝜃) → ∀𝑦 ∈ ω (𝑦 ∈ {𝑥 ∣ 𝜑} → suc 𝑦 ∈ {𝑥 ∣ 𝜑})) |
| 15 | bj-bdfindis.bd | . . . . 5 ⊢ BOUNDED 𝜑 | |
| 16 | 15 | bdcab 15785 | . . . 4 ⊢ BOUNDED {𝑥 ∣ 𝜑} |
| 17 | 16 | bdpeano5 15879 | . . 3 ⊢ ((∅ ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑦 ∈ ω (𝑦 ∈ {𝑥 ∣ 𝜑} → suc 𝑦 ∈ {𝑥 ∣ 𝜑})) → ω ⊆ {𝑥 ∣ 𝜑}) |
| 18 | 4, 14, 17 | syl2an 289 | . 2 ⊢ ((𝜓 ∧ ∀𝑦 ∈ ω (𝜒 → 𝜃)) → ω ⊆ {𝑥 ∣ 𝜑}) |
| 19 | ssabral 3264 | . 2 ⊢ (ω ⊆ {𝑥 ∣ 𝜑} ↔ ∀𝑥 ∈ ω 𝜑) | |
| 20 | 18, 19 | sylib 122 | 1 ⊢ ((𝜓 ∧ ∀𝑦 ∈ ω (𝜒 → 𝜃)) → ∀𝑥 ∈ ω 𝜑) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ∧ wa 104 = wceq 1373 Ⅎwnf 1483 ∈ wcel 2176 {cab 2191 ∀wral 2484 ⊆ wss 3166 ∅c0 3460 suc csuc 4412 ωcom 4638 BOUNDED wbd 15748 |
| 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 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-13 2178 ax-14 2179 ax-ext 2187 ax-nul 4170 ax-pr 4253 ax-un 4480 ax-bd0 15749 ax-bdor 15752 ax-bdex 15755 ax-bdeq 15756 ax-bdel 15757 ax-bdsb 15758 ax-bdsep 15820 ax-infvn 15877 |
| This theorem depends on definitions: df-bi 117 df-tru 1376 df-nf 1484 df-sb 1786 df-clab 2192 df-cleq 2198 df-clel 2201 df-nfc 2337 df-ral 2489 df-rex 2490 df-rab 2493 df-v 2774 df-dif 3168 df-un 3170 df-in 3172 df-ss 3179 df-nul 3461 df-sn 3639 df-pr 3640 df-uni 3851 df-int 3886 df-suc 4418 df-iom 4639 df-bdc 15777 df-bj-ind 15863 |
| This theorem is referenced by: bj-bdfindisg 15884 bj-bdfindes 15885 bj-nn0suc0 15886 |
| Copyright terms: Public domain | W3C validator |