Theorem findsg 7873

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 3973	. . . . . . 7 ⊢ (𝑥 = ∅ → (𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ ∅))
2	1	adantl 481	. . . . . 6 ⊢ ((𝐵 = ∅ ∧ 𝑥 = ∅) → (𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ ∅))
3		eqeq2 2741	. . . . . . . 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 4365	. . . . . . . . 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 811	. . . 4 ⊢ (𝑥 = ∅ → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓)))
15	14	imbi2d 340	. . 3 ⊢ (𝑥 = ∅ → ((𝐵 ∈ ω → (𝐵 ⊆ 𝑥 → 𝜑)) ↔ (𝐵 ∈ ω → (𝐵 ⊆ ∅ → 𝜓))))
16		sseq2 3973	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ 𝑦))
17		findsg.2	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
18	16, 17	imbi12d 344	. . . 4 ⊢ (𝑥 = 𝑦 → ((𝐵 ⊆ 𝑥 → 𝜑) ↔ (𝐵 ⊆ 𝑦 → 𝜒)))
19	18	imbi2d 340	. . 3 ⊢ (𝑥 = 𝑦 → ((𝐵 ∈ ω → (𝐵 ⊆ 𝑥 → 𝜑)) ↔ (𝐵 ∈ ω → (𝐵 ⊆ 𝑦 → 𝜒))))
20		sseq2 3973	. . . . 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 3973	. . . . 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 3451	. . . . . . . . . . . . . 14 ⊢ 𝑦 ∈ V
31	30	sucex 7782	. . . . . . . . . . . . 13 ⊢ suc 𝑦 ∈ V
32	31	eqvinc 3615	. . . . . . . . . . . 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 2737	. . . . . . . . . 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 2926	. . . . . . . . 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 7848	. . . . . . . . 9 ⊢ (𝐵 ∈ ω → 𝐵 ∈ On)
48		nnon 7848	. . . . . . . . 9 ⊢ (𝑦 ∈ ω → 𝑦 ∈ On)
49		onsssuc 6424	. . . . . . . . . 10 ⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ⊆ 𝑦 ↔ 𝐵 ∈ suc 𝑦))
50		onsuc 7787	. . . . . . . . . . 11 ⊢ (𝑦 ∈ On → suc 𝑦 ∈ On)
51		onelpss 6372	. . . . . . . . . . 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 7872	. 2 ⊢ (𝐴 ∈ ω → (𝐵 ∈ ω → (𝐵 ⊆ 𝐴 → 𝜏)))
66	65	imp31 417	1 ⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐵 ⊆ 𝐴) → 𝜏)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ≠ wne 2925   ⊆ wss 3914  ∅c0 4296  Oncon0 6332  suc csuc 6334  ωcom 7842

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-tr 5215  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-om 7843

This theorem is referenced by:  nnaordi  8582  inf3lem5  9585  ackbij2lem4  10194  sornom  10230  fin23lem15  10287  fin23lem36  10301  isf32lem1  10306  isf32lem2  10307  wunex2  10691  indpi  10860  satfsschain  35351