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

Theorem bj-bdfindis 14702
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 4600 for a proof of full induction in IZF. From this version, it is easy to prove bounded versions of finds 4600, finds2 4601, finds1 4602. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.)
Hypotheses
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 𝑦 → (𝜃𝜑))
Assertion
Ref Expression
bj-bdfindis ((𝜓 ∧ ∀𝑦 ∈ ω (𝜒𝜃)) → ∀𝑥 ∈ ω 𝜑)
Distinct variable groups:   𝑥,𝑦   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥,𝑦)   𝜒(𝑥,𝑦)   𝜃(𝑥,𝑦)

Proof of Theorem bj-bdfindis
StepHypRef Expression
1 bj-bdfindis.nf0 . . . 4 𝑥𝜓
2 0ex 4131 . . . 4 ∅ ∈ V
3 bj-bdfindis.0 . . . 4 (𝑥 = ∅ → (𝜓𝜑))
41, 2, 3elabf2 14537 . . 3 (𝜓 → ∅ ∈ {𝑥𝜑})
5 bj-bdfindis.nf1 . . . . . 6 𝑥𝜒
6 bj-bdfindis.1 . . . . . 6 (𝑥 = 𝑦 → (𝜑𝜒))
75, 6elabf1 14536 . . . . 5 (𝑦 ∈ {𝑥𝜑} → 𝜒)
8 bj-bdfindis.nfsuc . . . . . 6 𝑥𝜃
9 vex 2741 . . . . . . 7 𝑦 ∈ V
109bj-sucex 14678 . . . . . 6 suc 𝑦 ∈ V
11 bj-bdfindis.suc . . . . . 6 (𝑥 = suc 𝑦 → (𝜃𝜑))
128, 10, 11elabf2 14537 . . . . 5 (𝜃 → suc 𝑦 ∈ {𝑥𝜑})
137, 12imim12i 59 . . . 4 ((𝜒𝜃) → (𝑦 ∈ {𝑥𝜑} → suc 𝑦 ∈ {𝑥𝜑}))
1413ralimi 2540 . . 3 (∀𝑦 ∈ ω (𝜒𝜃) → ∀𝑦 ∈ ω (𝑦 ∈ {𝑥𝜑} → suc 𝑦 ∈ {𝑥𝜑}))
15 bj-bdfindis.bd . . . . 5 BOUNDED 𝜑
1615bdcab 14604 . . . 4 BOUNDED {𝑥𝜑}
1716bdpeano5 14698 . . 3 ((∅ ∈ {𝑥𝜑} ∧ ∀𝑦 ∈ ω (𝑦 ∈ {𝑥𝜑} → suc 𝑦 ∈ {𝑥𝜑})) → ω ⊆ {𝑥𝜑})
184, 14, 17syl2an 289 . 2 ((𝜓 ∧ ∀𝑦 ∈ ω (𝜒𝜃)) → ω ⊆ {𝑥𝜑})
19 ssabral 3227 . 2 (ω ⊆ {𝑥𝜑} ↔ ∀𝑥 ∈ ω 𝜑)
2018, 19sylib 122 1 ((𝜓 ∧ ∀𝑦 ∈ ω (𝜒𝜃)) → ∀𝑥 ∈ ω 𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104   = wceq 1353  wnf 1460  wcel 2148  {cab 2163  wral 2455  wss 3130  c0 3423  suc csuc 4366  ωcom 4590  BOUNDED wbd 14567
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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-nul 4130  ax-pr 4210  ax-un 4434  ax-bd0 14568  ax-bdor 14571  ax-bdex 14574  ax-bdeq 14575  ax-bdel 14576  ax-bdsb 14577  ax-bdsep 14639  ax-infvn 14696
This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2740  df-dif 3132  df-un 3134  df-in 3136  df-ss 3143  df-nul 3424  df-sn 3599  df-pr 3600  df-uni 3811  df-int 3846  df-suc 4372  df-iom 4591  df-bdc 14596  df-bj-ind 14682
This theorem is referenced by:  bj-bdfindisg  14703  bj-bdfindes  14704  bj-nn0suc0  14705
  Copyright terms: Public domain W3C validator