Theorem bj-bdfindis 16717

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 4722 for a proof of full induction in IZF. From this version, it is easy to prove bounded versions of finds 4722, finds2 4723, finds1 4724. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)

Hypotheses

Ref	Expression
bj-bdfindis.bd	|- BOUNDED ph
bj-bdfindis.nf0	|- F/ x ps
bj-bdfindis.nf1	|- F/ x ch
bj-bdfindis.nfsuc	|- F/ x th
bj-bdfindis.0	|- ( x = (/) -> ( ps -> ph ) )
bj-bdfindis.1	|- ( x = y -> ( ph -> ch ) )
bj-bdfindis.suc	|- ( x = suc y -> ( th -> ph ) )

Assertion

Ref	Expression
bj-bdfindis	|- ( ( ps /\ A. y e. om ( ch -> th ) ) -> A. x e. om ph )

Distinct variable groups:   x, y   ph, y

Allowed substitution hints:   ph( x)   ps( x, y)   ch( x, y)   th( x, y)

Proof of Theorem bj-bdfindis

Step	Hyp	Ref	Expression
1		bj-bdfindis.nf0	. . . 4 |- F/ x ps
2		0ex 4237	. . . 4 |- (/) e. _V
3		bj-bdfindis.0	. . . 4 |- ( x = (/) -> ( ps -> ph ) )
4	1, 2, 3	elabf2 16554	. . 3 |- ( ps -> (/) e. { x | ph } )
5		bj-bdfindis.nf1	. . . . . 6 |- F/ x ch
6		bj-bdfindis.1	. . . . . 6 |- ( x = y -> ( ph -> ch ) )
7	5, 6	elabf1 16553	. . . . 5 |- ( y e. { x | ph } -> ch )
8		bj-bdfindis.nfsuc	. . . . . 6 |- F/ x th
9		vex 2816	. . . . . . 7 |- y e. _V
10	9	bj-sucex 16693	. . . . . 6 |- suc y e. _V
11		bj-bdfindis.suc	. . . . . 6 |- ( x = suc y -> ( th -> ph ) )
12	8, 10, 11	elabf2 16554	. . . . 5 |- ( th -> suc y e. { x | ph } )
13	7, 12	imim12i 59	. . . 4 |- ( ( ch -> th ) -> ( y e. { x | ph } -> suc y e. { x | ph } ) )
14	13	ralimi 2605	. . 3 |- ( A. y e. om ( ch -> th ) -> A. y e. om ( y e. { x | ph } -> suc y e. { x | ph } ) )
15		bj-bdfindis.bd	. . . . 5 |- BOUNDED ph
16	15	bdcab 16619	. . . 4 |- BOUNDED { x | ph }
17	16	bdpeano5 16713	. . 3 |- ( ( (/) e. { x | ph } /\ A. y e. om ( y e. { x | ph } -> suc y e. { x | ph } ) ) -> om C_ { x | ph } )
18	4, 14, 17	syl2an 289	. 2 |- ( ( ps /\ A. y e. om ( ch -> th ) ) -> om C_ { x | ph } )
19		ssabral 3309	. 2 |- ( om C_ { x | ph } <-> A. x e. om ph )
20	18, 19	sylib 122	1 |- ( ( ps /\ A. y e. om ( ch -> th ) ) -> A. x e. om ph )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1398   F/wnf 1509   e. wcel 2203   {cab 2218   A.wral 2520   C_ wss 3211   (/)c0 3508   suc csuc 4486   omcom 4712  BOUNDED wbd 16582

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-nul 4236  ax-pr 4322  ax-un 4554  ax-bd0 16583  ax-bdor 16586  ax-bdex 16589  ax-bdeq 16590  ax-bdel 16591  ax-bdsb 16592  ax-bdsep 16654  ax-infvn 16711

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-rab 2529  df-v 2815  df-dif 3213  df-un 3215  df-in 3217  df-ss 3224  df-nul 3509  df-sn 3695  df-pr 3696  df-uni 3915  df-int 3950  df-suc 4492  df-iom 4713  df-bdc 16611  df-bj-ind 16697

This theorem is referenced by:  bj-bdfindisg  16718  bj-bdfindes  16719  bj-nn0suc0  16720