Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  bj-bdfindis Unicode version

Theorem bj-bdfindis 11271
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 4386 for a proof of full induction in IZF. From this version, it is easy to prove bounded versions of finds 4386, finds2 4387, finds1 4388. (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
StepHypRef Expression
1 bj-bdfindis.nf0 . . . 4  |-  F/ x ps
2 0ex 3939 . . . 4  |-  (/)  e.  _V
3 bj-bdfindis.0 . . . 4  |-  ( x  =  (/)  ->  ( ps 
->  ph ) )
41, 2, 3elabf2 11111 . . 3  |-  ( ps 
->  (/)  e.  { x  |  ph } )
5 bj-bdfindis.nf1 . . . . . 6  |-  F/ x ch
6 bj-bdfindis.1 . . . . . 6  |-  ( x  =  y  ->  ( ph  ->  ch ) )
75, 6elabf1 11110 . . . . 5  |-  ( y  e.  { x  | 
ph }  ->  ch )
8 bj-bdfindis.nfsuc . . . . . 6  |-  F/ x th
9 vex 2618 . . . . . . 7  |-  y  e. 
_V
109bj-sucex 11243 . . . . . 6  |-  suc  y  e.  _V
11 bj-bdfindis.suc . . . . . 6  |-  ( x  =  suc  y  -> 
( th  ->  ph )
)
128, 10, 11elabf2 11111 . . . . 5  |-  ( th 
->  suc  y  e.  {
x  |  ph }
)
137, 12imim12i 58 . . . 4  |-  ( ( ch  ->  th )  ->  ( y  e.  {
x  |  ph }  ->  suc  y  e.  {
x  |  ph }
) )
1413ralimi 2434 . . 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
1615bdcab 11169 . . . 4  |- BOUNDED  { x  |  ph }
1716bdpeano5 11267 . . 3  |-  ( (
(/)  e.  { x  |  ph }  /\  A. y  e.  om  (
y  e.  { x  |  ph }  ->  suc  y  e.  { x  |  ph } ) )  ->  om  C_  { x  |  ph } )
184, 14, 17syl2an 283 . 2  |-  ( ( ps  /\  A. y  e.  om  ( ch  ->  th ) )  ->  om  C_  { x  |  ph } )
19 ssabral 3081 . 2  |-  ( om  C_  { x  |  ph } 
<-> 
A. x  e.  om  ph )
2018, 19sylib 120 1  |-  ( ( ps  /\  A. y  e.  om  ( ch  ->  th ) )  ->  A. x  e.  om  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    = wceq 1287   F/wnf 1392    e. wcel 1436   {cab 2071   A.wral 2355    C_ wss 2988   (/)c0 3275   suc csuc 4164   omcom 4376  BOUNDED wbd 11132
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-nul 3938  ax-pr 4008  ax-un 4232  ax-bd0 11133  ax-bdor 11136  ax-bdex 11139  ax-bdeq 11140  ax-bdel 11141  ax-bdsb 11142  ax-bdsep 11204  ax-infvn 11265
This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ral 2360  df-rex 2361  df-rab 2364  df-v 2617  df-dif 2990  df-un 2992  df-in 2994  df-ss 3001  df-nul 3276  df-sn 3436  df-pr 3437  df-uni 3636  df-int 3671  df-suc 4170  df-iom 4377  df-bdc 11161  df-bj-ind 11251
This theorem is referenced by:  bj-bdfindisg  11272  bj-bdfindes  11273  bj-nn0suc0  11274
  Copyright terms: Public domain W3C validator