Theorem findsg 7841

Description: Principle of Finite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last two are the basis and the induction step. The basis of this version is an arbitrary natural number 𝐵 instead of zero. (Contributed by NM, 16-Sep-1995.)

Hypotheses

Ref	Expression
findsg.1	⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))
findsg.2	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
findsg.3	⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃))
findsg.4	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
findsg.5	⊢ (𝐵 ∈ ω → 𝜓)
findsg.6	⊢ (((𝑦 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐵 ⊆ 𝑦) → (𝜒 → 𝜃))

Assertion

Ref	Expression
findsg	⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐵 ⊆ 𝐴) → 𝜏)

Distinct variable groups:   𝑥,𝐴   𝑥,𝑦,𝐵   𝜓,𝑥   𝜒,𝑥   𝜃,𝑥   𝜏,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)   𝜒(𝑦)   𝜃(𝑦)   𝜏(𝑦)   𝐴(𝑦)

Proof of Theorem findsg

Step	Hyp	Ref	Expression
1		sseq2 3949	. . . . . . 7 ⊢ (𝑥 = ∅ → (𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ ∅))
2	1	adantl 481	. . . . . 6 ⊢ ((𝐵 = ∅ ∧ 𝑥 = ∅) → (𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ ∅))
3		eqeq2 2749	. . . . . . . 8 ⊢ (𝐵 = ∅ → (𝑥 = 𝐵 ↔ 𝑥 = ∅))
4		findsg.1	. . . . . . . 8 ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))
5	3, 4	biimtrrdi 254	. . . . . . 7 ⊢ (𝐵 = ∅ → (𝑥 = ∅ → (𝜑 ↔ 𝜓)))
6	5	imp 406	. . . . . 6 ⊢ ((𝐵 = ∅ ∧ 𝑥 = ∅) → (𝜑 ↔ 𝜓))
7	2, 6	imbi12d 344	. . . . 5 ⊢ ((𝐵 = ∅ ∧ 𝑥 = ∅) → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓)))
8	1	imbi1d 341	. . . . . 6 ⊢ (𝑥 = ∅ → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ ∅ → 𝜑)))
9		ss0 4343	. . . . . . . . 9 ⊢ (𝐵 ⊆ ∅ → 𝐵 = ∅)
10	9	con3i 154	. . . . . . . 8 ⊢ (¬ 𝐵 = ∅ → ¬ 𝐵 ⊆ ∅)
11	10	pm2.21d 121	. . . . . . 7 ⊢ (¬ 𝐵 = ∅ → (𝐵 ⊆ ∅ → (𝜑 ↔ 𝜓)))
12	11	pm5.74d 273	. . . . . 6 ⊢ (¬ 𝐵 = ∅ → ((𝐵 ⊆ ∅ → 𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓)))
13	8, 12	sylan9bbr 510	. . . . 5 ⊢ ((¬ 𝐵 = ∅ ∧ 𝑥 = ∅) → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓)))
14	7, 13	pm2.61ian 812	. . . 4 ⊢ (𝑥 = ∅ → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓)))
15	14	imbi2d 340	. . 3 ⊢ (𝑥 = ∅ → ((𝐵 ∈ ω → (𝐵 ⊆ 𝑥 → 𝜑)) ↔ (𝐵 ∈ ω → (𝐵 ⊆ ∅ → 𝜓))))
16		sseq2 3949	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ 𝑦))
17		findsg.2	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
18	16, 17	imbi12d 344	. . . 4 ⊢ (𝑥 = 𝑦 → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ 𝑦 → 𝜒)))
19	18	imbi2d 340	. . 3 ⊢ (𝑥 = 𝑦 → ((𝐵 ∈ ω → (𝐵 ⊆ 𝑥 → 𝜑)) ↔ (𝐵 ∈ ω → (𝐵 ⊆ 𝑦 → 𝜒))))
20		sseq2 3949	. . . . 5 ⊢ (𝑥 = suc 𝑦 → (𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ suc 𝑦))
21		findsg.3	. . . . 5 ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃))
22	20, 21	imbi12d 344	. . . 4 ⊢ (𝑥 = suc 𝑦 → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ suc 𝑦 → 𝜃)))
23	22	imbi2d 340	. . 3 ⊢ (𝑥 = suc 𝑦 → ((𝐵 ∈ ω → (𝐵 ⊆ 𝑥 → 𝜑)) ↔ (𝐵 ∈ ω → (𝐵 ⊆ suc 𝑦 → 𝜃))))
24		sseq2 3949	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ 𝐴))
25		findsg.4	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
26	24, 25	imbi12d 344	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ 𝐴 → 𝜏)))
27	26	imbi2d 340	. . 3 ⊢ (𝑥 = 𝐴 → ((𝐵 ∈ ω → (𝐵 ⊆ 𝑥 → 𝜑)) ↔ (𝐵 ∈ ω → (𝐵 ⊆ 𝐴 → 𝜏))))
28		findsg.5	. . . 4 ⊢ (𝐵 ∈ ω → 𝜓)
29	28	a1d 25	. . 3 ⊢ (𝐵 ∈ ω → (𝐵 ⊆ ∅ → 𝜓))
30		vex 3434	. . . . . . . . . . . . . 14 ⊢ 𝑦 ∈ V
31	30	sucex 7753	. . . . . . . . . . . . 13 ⊢ suc 𝑦 ∈ V
32	31	eqvinc 3592	. . . . . . . . . . . 12 ⊢ (suc 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 = suc 𝑦 ∧ 𝑥 = 𝐵))
33	28, 4	imbitrrid 246	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝐵 → (𝐵 ∈ ω → 𝜑))
34	21	biimpd 229	. . . . . . . . . . . . . 14 ⊢ (𝑥 = suc 𝑦 → (𝜑 → 𝜃))
35	33, 34	sylan9r 508	. . . . . . . . . . . . 13 ⊢ ((𝑥 = suc 𝑦 ∧ 𝑥 = 𝐵) → (𝐵 ∈ ω → 𝜃))
36	35	exlimiv 1932	. . . . . . . . . . . 12 ⊢ (∃𝑥(𝑥 = suc 𝑦 ∧ 𝑥 = 𝐵) → (𝐵 ∈ ω → 𝜃))
37	32, 36	sylbi 217	. . . . . . . . . . 11 ⊢ (suc 𝑦 = 𝐵 → (𝐵 ∈ ω → 𝜃))
38	37	eqcoms 2745	. . . . . . . . . 10 ⊢ (𝐵 = suc 𝑦 → (𝐵 ∈ ω → 𝜃))
39	38	imim2i 16	. . . . . . . . 9 ⊢ ((𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦) → (𝐵 ⊆ suc 𝑦 → (𝐵 ∈ ω → 𝜃)))
40	39	a1d 25	. . . . . . . 8 ⊢ ((𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦) → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → (𝐵 ∈ ω → 𝜃))))
41	40	com4r 94	. . . . . . 7 ⊢ (𝐵 ∈ ω → ((𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦) → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → 𝜃))))
42	41	adantl 481	. . . . . 6 ⊢ ((𝑦 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦) → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → 𝜃))))
43		df-ne 2934	. . . . . . . . 9 ⊢ (𝐵 ≠ suc 𝑦 ↔ ¬ 𝐵 = suc 𝑦)
44	43	anbi2i 624	. . . . . . . 8 ⊢ ((𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦) ↔ (𝐵 ⊆ suc 𝑦 ∧ ¬ 𝐵 = suc 𝑦))
45		annim 403	. . . . . . . 8 ⊢ ((𝐵 ⊆ suc 𝑦 ∧ ¬ 𝐵 = suc 𝑦) ↔ ¬ (𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦))
46	44, 45	bitri 275	. . . . . . 7 ⊢ ((𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦) ↔ ¬ (𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦))
47		nnon 7816	. . . . . . . . 9 ⊢ (𝐵 ∈ ω → 𝐵 ∈ On)
48		nnon 7816	. . . . . . . . 9 ⊢ (𝑦 ∈ ω → 𝑦 ∈ On)
49		onsssuc 6409	. . . . . . . . . 10 ⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ⊆ 𝑦 ↔ 𝐵 ∈ suc 𝑦))
50		onsuc 7757	. . . . . . . . . . 11 ⊢ (𝑦 ∈ On → suc 𝑦 ∈ On)
51		onelpss 6357	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ On ∧ suc 𝑦 ∈ On) → (𝐵 ∈ suc 𝑦 ↔ (𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦)))
52	50, 51	sylan2 594	. . . . . . . . . 10 ⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ∈ suc 𝑦 ↔ (𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦)))
53	49, 52	bitrd 279	. . . . . . . . 9 ⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ⊆ 𝑦 ↔ (𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦)))
54	47, 48, 53	syl2anr 598	. . . . . . . 8 ⊢ ((𝑦 ∈ ω ∧ 𝐵 ∈ ω) → (𝐵 ⊆ 𝑦 ↔ (𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦)))
55		findsg.6	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐵 ⊆ 𝑦) → (𝜒 → 𝜃))
56	55	ex 412	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ω ∧ 𝐵 ∈ ω) → (𝐵 ⊆ 𝑦 → (𝜒 → 𝜃)))
57	56	a1ddd 80	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ω ∧ 𝐵 ∈ ω) → (𝐵 ⊆ 𝑦 → (𝜒 → (𝐵 ⊆ suc 𝑦 → 𝜃))))
58	57	a2d 29	. . . . . . . . 9 ⊢ ((𝑦 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ 𝑦 → (𝐵 ⊆ suc 𝑦 → 𝜃))))
59	58	com23 86	. . . . . . . 8 ⊢ ((𝑦 ∈ ω ∧ 𝐵 ∈ ω) → (𝐵 ⊆ 𝑦 → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → 𝜃))))
60	54, 59	sylbird 260	. . . . . . 7 ⊢ ((𝑦 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦) → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → 𝜃))))
61	46, 60	biimtrrid 243	. . . . . 6 ⊢ ((𝑦 ∈ ω ∧ 𝐵 ∈ ω) → (¬ (𝐵 ⊆ suc 𝑦 → 𝐵 = suc 𝑦) → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → 𝜃))))
62	42, 61	pm2.61d 179	. . . . 5 ⊢ ((𝑦 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → 𝜃)))
63	62	ex 412	. . . 4 ⊢ (𝑦 ∈ ω → (𝐵 ∈ ω → ((𝐵 ⊆ 𝑦 → 𝜒) → (𝐵 ⊆ suc 𝑦 → 𝜃))))
64	63	a2d 29	. . 3 ⊢ (𝑦 ∈ ω → ((𝐵 ∈ ω → (𝐵 ⊆ 𝑦 → 𝜒)) → (𝐵 ∈ ω → (𝐵 ⊆ suc 𝑦 → 𝜃))))
65	15, 19, 23, 27, 29, 64	finds 7840	. 2 ⊢ (𝐴 ∈ ω → (𝐵 ∈ ω → (𝐵 ⊆ 𝐴 → 𝜏)))
66	65	imp31 417	1 ⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐵 ⊆ 𝐴) → 𝜏)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114   ≠ wne 2933   ⊆ wss 3890  ∅c0 4274  Oncon0 6317  suc csuc 6319  ωcom 7810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-tr 5194  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-om 7811

This theorem is referenced by:  nnaordi  8547  inf3lem5  9544  ackbij2lem4  10154  sornom  10190  fin23lem15  10247  fin23lem36  10261  isf32lem1  10266  isf32lem2  10267  wunex2  10652  indpi  10821  satfsschain  35562