Theorem findsg 7919

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 4010	. . . . . . 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 4402	. . . . . . . . 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 4010	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ 𝑦))
17		findsg.2	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
18	16, 17	imbi12d 344	. . . 4 ⊢ (𝑥 = 𝑦 → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ 𝑦 → 𝜒)))
19	18	imbi2d 340	. . 3 ⊢ (𝑥 = 𝑦 → ((𝐵 ∈ ω → (𝐵 ⊆ 𝑥 → 𝜑)) ↔ (𝐵 ∈ ω → (𝐵 ⊆ 𝑦 → 𝜒))))
20		sseq2 4010	. . . . 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 4010	. . . . 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 3484	. . . . . . . . . . . . . 14 ⊢ 𝑦 ∈ V
31	30	sucex 7826	. . . . . . . . . . . . 13 ⊢ suc 𝑦 ∈ V
32	31	eqvinc 3649	. . . . . . . . . . . 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 1930	. . . . . . . . . . . 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 2941	. . . . . . . . 9 ⊢ (𝐵 ≠ suc 𝑦 ↔ ¬ 𝐵 = suc 𝑦)
44	43	anbi2i 623	. . . . . . . 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 7893	. . . . . . . . 9 ⊢ (𝐵 ∈ ω → 𝐵 ∈ On)
48		nnon 7893	. . . . . . . . 9 ⊢ (𝑦 ∈ ω → 𝑦 ∈ On)
49		onsssuc 6474	. . . . . . . . . 10 ⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ⊆ 𝑦 ↔ 𝐵 ∈ suc 𝑦))
50		onsuc 7831	. . . . . . . . . . 11 ⊢ (𝑦 ∈ On → suc 𝑦 ∈ On)
51		onelpss 6424	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ On ∧ suc 𝑦 ∈ On) → (𝐵 ∈ suc 𝑦 ↔ (𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦)))
52	50, 51	sylan2 593	. . . . . . . . . 10 ⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ∈ suc 𝑦 ↔ (𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦)))
53	49, 52	bitrd 279	. . . . . . . . 9 ⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ⊆ 𝑦 ↔ (𝐵 ⊆ suc 𝑦 ∧ 𝐵 ≠ suc 𝑦)))
54	47, 48, 53	syl2anr 597	. . . . . . . 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 7918	. 2 ⊢ (𝐴 ∈ ω → (𝐵 ∈ ω → (𝐵 ⊆ 𝐴 → 𝜏)))
66	65	imp31 417	1 ⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐵 ⊆ 𝐴) → 𝜏)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2108   ≠ wne 2940   ⊆ wss 3951  ∅c0 4333  Oncon0 6384  suc csuc 6386  ωcom 7887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-tr 5260  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-om 7888

This theorem is referenced by:  nnaordi  8656  inf3lem5  9672  ackbij2lem4  10281  sornom  10317  fin23lem15  10374  fin23lem36  10388  isf32lem1  10393  isf32lem2  10394  wunex2  10778  indpi  10947  satfsschain  35369