Theorem bj-bdfindis 16542

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 4698 for a proof of full induction in IZF. From this version, it is easy to prove bounded versions of finds 4698, finds2 4699, finds1 4700. (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

Step	Hyp	Ref	Expression
1		bj-bdfindis.nf0	. . . 4 ⊢ Ⅎ𝑥𝜓
2		0ex 4216	. . . 4 ⊢ ∅ ∈ V
3		bj-bdfindis.0	. . . 4 ⊢ (𝑥 = ∅ → (𝜓 → 𝜑))
4	1, 2, 3	elabf2 16378	. . 3 ⊢ (𝜓 → ∅ ∈ {𝑥 ∣ 𝜑})
5		bj-bdfindis.nf1	. . . . . 6 ⊢ Ⅎ𝑥𝜒
6		bj-bdfindis.1	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜒))
7	5, 6	elabf1 16377	. . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} → 𝜒)
8		bj-bdfindis.nfsuc	. . . . . 6 ⊢ Ⅎ𝑥𝜃
9		vex 2805	. . . . . . 7 ⊢ 𝑦 ∈ V
10	9	bj-sucex 16518	. . . . . 6 ⊢ suc 𝑦 ∈ V
11		bj-bdfindis.suc	. . . . . 6 ⊢ (𝑥 = suc 𝑦 → (𝜃 → 𝜑))
12	8, 10, 11	elabf2 16378	. . . . 5 ⊢ (𝜃 → suc 𝑦 ∈ {𝑥 ∣ 𝜑})
13	7, 12	imim12i 59	. . . 4 ⊢ ((𝜒 → 𝜃) → (𝑦 ∈ {𝑥 ∣ 𝜑} → suc 𝑦 ∈ {𝑥 ∣ 𝜑}))
14	13	ralimi 2595	. . 3 ⊢ (∀𝑦 ∈ ω (𝜒 → 𝜃) → ∀𝑦 ∈ ω (𝑦 ∈ {𝑥 ∣ 𝜑} → suc 𝑦 ∈ {𝑥 ∣ 𝜑}))
15		bj-bdfindis.bd	. . . . 5 ⊢ BOUNDED 𝜑
16	15	bdcab 16444	. . . 4 ⊢ BOUNDED {𝑥 ∣ 𝜑}
17	16	bdpeano5 16538	. . 3 ⊢ ((∅ ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑦 ∈ ω (𝑦 ∈ {𝑥 ∣ 𝜑} → suc 𝑦 ∈ {𝑥 ∣ 𝜑})) → ω ⊆ {𝑥 ∣ 𝜑})
18	4, 14, 17	syl2an 289	. 2 ⊢ ((𝜓 ∧ ∀𝑦 ∈ ω (𝜒 → 𝜃)) → ω ⊆ {𝑥 ∣ 𝜑})
19		ssabral 3298	. 2 ⊢ (ω ⊆ {𝑥 ∣ 𝜑} ↔ ∀𝑥 ∈ ω 𝜑)
20	18, 19	sylib 122	1 ⊢ ((𝜓 ∧ ∀𝑦 ∈ ω (𝜒 → 𝜃)) → ∀𝑥 ∈ ω 𝜑)

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1397  Ⅎwnf 1508   ∈ wcel 2202  {cab 2217  ∀wral 2510   ⊆ wss 3200  ∅c0 3494  suc csuc 4462  ωcom 4688  BOUNDED wbd 16407

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2204  ax-14 2205  ax-ext 2213  ax-nul 4215  ax-pr 4299  ax-un 4530  ax-bd0 16408  ax-bdor 16411  ax-bdex 16414  ax-bdeq 16415  ax-bdel 16416  ax-bdsb 16417  ax-bdsep 16479  ax-infvn 16536

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-rab 2519  df-v 2804  df-dif 3202  df-un 3204  df-in 3206  df-ss 3213  df-nul 3495  df-sn 3675  df-pr 3676  df-uni 3894  df-int 3929  df-suc 4468  df-iom 4689  df-bdc 16436  df-bj-ind 16522

This theorem is referenced by:  bj-bdfindisg  16543  bj-bdfindes  16544  bj-nn0suc0  16545