![]() |
Mathbox for BJ |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > Mathboxes > bj-bdfindis | Unicode 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 4553 for a proof of full induction in IZF. From this version, it is easy to prove bounded versions of finds 4553, finds2 4554, finds1 4555. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
bj-bdfindis.bd |
![]() ![]() |
bj-bdfindis.nf0 |
![]() ![]() ![]() ![]() |
bj-bdfindis.nf1 |
![]() ![]() ![]() ![]() |
bj-bdfindis.nfsuc |
![]() ![]() ![]() ![]() |
bj-bdfindis.0 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
bj-bdfindis.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
bj-bdfindis.suc |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
bj-bdfindis |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-bdfindis.nf0 |
. . . 4
![]() ![]() ![]() ![]() | |
2 | 0ex 4087 |
. . . 4
![]() ![]() ![]() ![]() | |
3 | bj-bdfindis.0 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | elabf2 13294 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | bj-bdfindis.nf1 |
. . . . . 6
![]() ![]() ![]() ![]() | |
6 | bj-bdfindis.1 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 5, 6 | elabf1 13293 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | bj-bdfindis.nfsuc |
. . . . . 6
![]() ![]() ![]() ![]() | |
9 | vex 2712 |
. . . . . . 7
![]() ![]() ![]() ![]() | |
10 | 9 | bj-sucex 13436 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() |
11 | bj-bdfindis.suc |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
12 | 8, 10, 11 | elabf2 13294 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
13 | 7, 12 | imim12i 59 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 13 | ralimi 2517 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | bj-bdfindis.bd |
. . . . 5
![]() ![]() | |
16 | 15 | bdcab 13362 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() |
17 | 16 | bdpeano5 13456 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
18 | 4, 14, 17 | syl2an 287 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
19 | ssabral 3195 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
20 | 18, 19 | sylib 121 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
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 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1481 ax-10 1482 ax-11 1483 ax-i12 1484 ax-bndl 1486 ax-4 1487 ax-17 1503 ax-i9 1507 ax-ial 1511 ax-i5r 1512 ax-13 2127 ax-14 2128 ax-ext 2136 ax-nul 4086 ax-pr 4164 ax-un 4388 ax-bd0 13326 ax-bdor 13329 ax-bdex 13332 ax-bdeq 13333 ax-bdel 13334 ax-bdsb 13335 ax-bdsep 13397 ax-infvn 13454 |
This theorem depends on definitions: df-bi 116 df-tru 1335 df-nf 1438 df-sb 1740 df-clab 2141 df-cleq 2147 df-clel 2150 df-nfc 2285 df-ral 2437 df-rex 2438 df-rab 2441 df-v 2711 df-dif 3100 df-un 3102 df-in 3104 df-ss 3111 df-nul 3391 df-sn 3562 df-pr 3563 df-uni 3769 df-int 3804 df-suc 4326 df-iom 4544 df-bdc 13354 df-bj-ind 13440 |
This theorem is referenced by: bj-bdfindisg 13461 bj-bdfindes 13462 bj-nn0suc0 13463 |
Copyright terms: Public domain | W3C validator |