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 4559 for a proof of full induction in IZF. From this version, it is easy to prove bounded versions of finds 4559, finds2 4560, finds1 4561. (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 4091 | . . . 4 ⊢ ∅ ∈ V | |
3 | bj-bdfindis.0 | . . . 4 ⊢ (𝑥 = ∅ → (𝜓 → 𝜑)) | |
4 | 1, 2, 3 | elabf2 13356 | . . 3 ⊢ (𝜓 → ∅ ∈ {𝑥 ∣ 𝜑}) |
5 | bj-bdfindis.nf1 | . . . . . 6 ⊢ Ⅎ𝑥𝜒 | |
6 | bj-bdfindis.1 | . . . . . 6 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜒)) | |
7 | 5, 6 | elabf1 13355 | . . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} → 𝜒) |
8 | bj-bdfindis.nfsuc | . . . . . 6 ⊢ Ⅎ𝑥𝜃 | |
9 | vex 2715 | . . . . . . 7 ⊢ 𝑦 ∈ V | |
10 | 9 | bj-sucex 13498 | . . . . . 6 ⊢ suc 𝑦 ∈ V |
11 | bj-bdfindis.suc | . . . . . 6 ⊢ (𝑥 = suc 𝑦 → (𝜃 → 𝜑)) | |
12 | 8, 10, 11 | elabf2 13356 | . . . . 5 ⊢ (𝜃 → suc 𝑦 ∈ {𝑥 ∣ 𝜑}) |
13 | 7, 12 | imim12i 59 | . . . 4 ⊢ ((𝜒 → 𝜃) → (𝑦 ∈ {𝑥 ∣ 𝜑} → suc 𝑦 ∈ {𝑥 ∣ 𝜑})) |
14 | 13 | ralimi 2520 | . . 3 ⊢ (∀𝑦 ∈ ω (𝜒 → 𝜃) → ∀𝑦 ∈ ω (𝑦 ∈ {𝑥 ∣ 𝜑} → suc 𝑦 ∈ {𝑥 ∣ 𝜑})) |
15 | bj-bdfindis.bd | . . . . 5 ⊢ BOUNDED 𝜑 | |
16 | 15 | bdcab 13424 | . . . 4 ⊢ BOUNDED {𝑥 ∣ 𝜑} |
17 | 16 | bdpeano5 13518 | . . 3 ⊢ ((∅ ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑦 ∈ ω (𝑦 ∈ {𝑥 ∣ 𝜑} → suc 𝑦 ∈ {𝑥 ∣ 𝜑})) → ω ⊆ {𝑥 ∣ 𝜑}) |
18 | 4, 14, 17 | syl2an 287 | . 2 ⊢ ((𝜓 ∧ ∀𝑦 ∈ ω (𝜒 → 𝜃)) → ω ⊆ {𝑥 ∣ 𝜑}) |
19 | ssabral 3199 | . 2 ⊢ (ω ⊆ {𝑥 ∣ 𝜑} ↔ ∀𝑥 ∈ ω 𝜑) | |
20 | 18, 19 | sylib 121 | 1 ⊢ ((𝜓 ∧ ∀𝑦 ∈ ω (𝜒 → 𝜃)) → ∀𝑥 ∈ ω 𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 = wceq 1335 Ⅎwnf 1440 ∈ wcel 2128 {cab 2143 ∀wral 2435 ⊆ wss 3102 ∅c0 3394 suc csuc 4325 ωcom 4549 BOUNDED wbd 13387 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-10 1485 ax-11 1486 ax-i12 1487 ax-bndl 1489 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-13 2130 ax-14 2131 ax-ext 2139 ax-nul 4090 ax-pr 4169 ax-un 4393 ax-bd0 13388 ax-bdor 13391 ax-bdex 13394 ax-bdeq 13395 ax-bdel 13396 ax-bdsb 13397 ax-bdsep 13459 ax-infvn 13516 |
This theorem depends on definitions: df-bi 116 df-tru 1338 df-nf 1441 df-sb 1743 df-clab 2144 df-cleq 2150 df-clel 2153 df-nfc 2288 df-ral 2440 df-rex 2441 df-rab 2444 df-v 2714 df-dif 3104 df-un 3106 df-in 3108 df-ss 3115 df-nul 3395 df-sn 3566 df-pr 3567 df-uni 3773 df-int 3808 df-suc 4331 df-iom 4550 df-bdc 13416 df-bj-ind 13502 |
This theorem is referenced by: bj-bdfindisg 13523 bj-bdfindes 13524 bj-nn0suc0 13525 |
Copyright terms: Public domain | W3C validator |