Theorem indpi 6440

Description: Principle of Finite Induction on positive integers. (Contributed by NM, 23-Mar-1996.)

Hypotheses

Ref	Expression
indpi.1	⊢ (𝑥 = 1𝑜 → (𝜑 ↔ 𝜓))
indpi.2	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
indpi.3	⊢ (𝑥 = (𝑦 +N 1𝑜) → (𝜑 ↔ 𝜃))
indpi.4	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
indpi.5	⊢ 𝜓
indpi.6	⊢ (𝑦 ∈ N → (𝜒 → 𝜃))

Assertion

Ref	Expression
indpi	⊢ (𝐴 ∈ N → 𝜏)

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

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

Proof of Theorem indpi

Step	Hyp	Ref	Expression
1		indpi.4	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
2		elni 6406	. . 3 ⊢ (𝑥 ∈ N ↔ (𝑥 ∈ ω ∧ 𝑥 ≠ ∅))
3		eqid 2040	. . . . . . . . . 10 ⊢ ∅ = ∅
4	3	orci 650	. . . . . . . . 9 ⊢ (∅ = ∅ ∨ [∅ / 𝑥]𝜑)
5		nfv 1421	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∅ = ∅
6		nfsbc1v 2782	. . . . . . . . . . 11 ⊢ Ⅎ𝑥[∅ / 𝑥]𝜑
7	5, 6	nfor 1466	. . . . . . . . . 10 ⊢ Ⅎ𝑥(∅ = ∅ ∨ [∅ / 𝑥]𝜑)
8		0ex 3884	. . . . . . . . . 10 ⊢ ∅ ∈ V
9		eqeq1 2046	. . . . . . . . . . 11 ⊢ (𝑥 = ∅ → (𝑥 = ∅ ↔ ∅ = ∅))
10		sbceq1a 2773	. . . . . . . . . . 11 ⊢ (𝑥 = ∅ → (𝜑 ↔ [∅ / 𝑥]𝜑))
11	9, 10	orbi12d 707	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → ((𝑥 = ∅ ∨ 𝜑) ↔ (∅ = ∅ ∨ [∅ / 𝑥]𝜑)))
12	7, 8, 11	elabf 2686	. . . . . . . . 9 ⊢ (∅ ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)} ↔ (∅ = ∅ ∨ [∅ / 𝑥]𝜑))
13	4, 12	mpbir 134	. . . . . . . 8 ⊢ ∅ ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)}
14		suceq 4139	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ∅ → suc 𝑦 = suc ∅)
15		df-1o 6001	. . . . . . . . . . . . . 14 ⊢ 1𝑜 = suc ∅
16	14, 15	syl6eqr 2090	. . . . . . . . . . . . 13 ⊢ (𝑦 = ∅ → suc 𝑦 = 1𝑜)
17		indpi.5	. . . . . . . . . . . . . . 15 ⊢ 𝜓
18	17	olci 651	. . . . . . . . . . . . . 14 ⊢ (1𝑜 = ∅ ∨ 𝜓)
19		1onn 6093	. . . . . . . . . . . . . . . 16 ⊢ 1𝑜 ∈ ω
20	19	elexi 2567	. . . . . . . . . . . . . . 15 ⊢ 1𝑜 ∈ V
21		eqeq1 2046	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 1𝑜 → (𝑥 = ∅ ↔ 1𝑜 = ∅))
22		indpi.1	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 1𝑜 → (𝜑 ↔ 𝜓))
23	21, 22	orbi12d 707	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 1𝑜 → ((𝑥 = ∅ ∨ 𝜑) ↔ (1𝑜 = ∅ ∨ 𝜓)))
24	20, 23	elab 2687	. . . . . . . . . . . . . 14 ⊢ (1𝑜 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)} ↔ (1𝑜 = ∅ ∨ 𝜓))
25	18, 24	mpbir 134	. . . . . . . . . . . . 13 ⊢ 1𝑜 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)}
26	16, 25	syl6eqel 2128	. . . . . . . . . . . 12 ⊢ (𝑦 = ∅ → suc 𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)})
27	26	a1d 22	. . . . . . . . . . 11 ⊢ (𝑦 = ∅ → (𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)} → suc 𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)}))
28	27	a1i 9	. . . . . . . . . 10 ⊢ (𝑦 ∈ ω → (𝑦 = ∅ → (𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)} → suc 𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)})))
29		indpi.6	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ N → (𝜒 → 𝜃))
30		elni 6406	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ N ↔ (𝑦 ∈ ω ∧ 𝑦 ≠ ∅))
31	30	simprbi 260	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ N → 𝑦 ≠ ∅)
32	31	neneqd 2226	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ N → ¬ 𝑦 = ∅)
33		biorf 663	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑦 = ∅ → (𝜒 ↔ (𝑦 = ∅ ∨ 𝜒)))
34	32, 33	syl 14	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ N → (𝜒 ↔ (𝑦 = ∅ ∨ 𝜒)))
35		vex 2560	. . . . . . . . . . . . . 14 ⊢ 𝑦 ∈ V
36		eqeq1 2046	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑥 = ∅ ↔ 𝑦 = ∅))
37		indpi.2	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
38	36, 37	orbi12d 707	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((𝑥 = ∅ ∨ 𝜑) ↔ (𝑦 = ∅ ∨ 𝜒)))
39	35, 38	elab 2687	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)} ↔ (𝑦 = ∅ ∨ 𝜒))
40	34, 39	syl6bbr 187	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ N → (𝜒 ↔ 𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)}))
41		1pi 6413	. . . . . . . . . . . . . . . . . 18 ⊢ 1𝑜 ∈ N
42		addclpi 6425	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ N ∧ 1𝑜 ∈ N) → (𝑦 +N 1𝑜) ∈ N)
43	41, 42	mpan2 401	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ N → (𝑦 +N 1𝑜) ∈ N)
44		elni 6406	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 +N 1𝑜) ∈ N ↔ ((𝑦 +N 1𝑜) ∈ ω ∧ (𝑦 +N 1𝑜) ≠ ∅))
45	43, 44	sylib 127	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ N → ((𝑦 +N 1𝑜) ∈ ω ∧ (𝑦 +N 1𝑜) ≠ ∅))
46	45	simprd 107	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ N → (𝑦 +N 1𝑜) ≠ ∅)
47	46	neneqd 2226	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ N → ¬ (𝑦 +N 1𝑜) = ∅)
48		biorf 663	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑦 +N 1𝑜) = ∅ → (𝜃 ↔ ((𝑦 +N 1𝑜) = ∅ ∨ 𝜃)))
49	47, 48	syl 14	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ N → (𝜃 ↔ ((𝑦 +N 1𝑜) = ∅ ∨ 𝜃)))
50		eqeq1 2046	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝑦 +N 1𝑜) → (𝑥 = ∅ ↔ (𝑦 +N 1𝑜) = ∅))
51		indpi.3	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝑦 +N 1𝑜) → (𝜑 ↔ 𝜃))
52	50, 51	orbi12d 707	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑦 +N 1𝑜) → ((𝑥 = ∅ ∨ 𝜑) ↔ ((𝑦 +N 1𝑜) = ∅ ∨ 𝜃)))
53	52	elabg 2688	. . . . . . . . . . . . . 14 ⊢ ((𝑦 +N 1𝑜) ∈ N → ((𝑦 +N 1𝑜) ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)} ↔ ((𝑦 +N 1𝑜) = ∅ ∨ 𝜃)))
54	43, 53	syl 14	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ N → ((𝑦 +N 1𝑜) ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)} ↔ ((𝑦 +N 1𝑜) = ∅ ∨ 𝜃)))
55		addpiord 6414	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ N ∧ 1𝑜 ∈ N) → (𝑦 +N 1𝑜) = (𝑦 +𝑜 1𝑜))
56	41, 55	mpan2 401	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ N → (𝑦 +N 1𝑜) = (𝑦 +𝑜 1𝑜))
57		pion 6408	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ N → 𝑦 ∈ On)
58		oa1suc 6047	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ On → (𝑦 +𝑜 1𝑜) = suc 𝑦)
59	57, 58	syl 14	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ N → (𝑦 +𝑜 1𝑜) = suc 𝑦)
60	56, 59	eqtrd 2072	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ N → (𝑦 +N 1𝑜) = suc 𝑦)
61	60	eleq1d 2106	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ N → ((𝑦 +N 1𝑜) ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)} ↔ suc 𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)}))
62	49, 54, 61	3bitr2d 205	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ N → (𝜃 ↔ suc 𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)}))
63	29, 40, 62	3imtr3d 191	. . . . . . . . . . 11 ⊢ (𝑦 ∈ N → (𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)} → suc 𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)}))
64	63	a1i 9	. . . . . . . . . 10 ⊢ (𝑦 ∈ ω → (𝑦 ∈ N → (𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)} → suc 𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)})))
65		nndceq0 4339	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ω → DECID 𝑦 = ∅)
66		df-dc 743	. . . . . . . . . . . 12 ⊢ (DECID 𝑦 = ∅ ↔ (𝑦 = ∅ ∨ ¬ 𝑦 = ∅))
67	65, 66	sylib 127	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ω → (𝑦 = ∅ ∨ ¬ 𝑦 = ∅))
68		idd 21	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ω → (𝑦 = ∅ → 𝑦 = ∅))
69	68	necon3bd 2248	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ω → (¬ 𝑦 = ∅ → 𝑦 ≠ ∅))
70	69	anc2li 312	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ω → (¬ 𝑦 = ∅ → (𝑦 ∈ ω ∧ 𝑦 ≠ ∅)))
71	70, 30	syl6ibr 151	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ω → (¬ 𝑦 = ∅ → 𝑦 ∈ N))
72	71	orim2d 702	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ω → ((𝑦 = ∅ ∨ ¬ 𝑦 = ∅) → (𝑦 = ∅ ∨ 𝑦 ∈ N)))
73	67, 72	mpd 13	. . . . . . . . . 10 ⊢ (𝑦 ∈ ω → (𝑦 = ∅ ∨ 𝑦 ∈ N))
74	28, 64, 73	mpjaod 638	. . . . . . . . 9 ⊢ (𝑦 ∈ ω → (𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)} → suc 𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)}))
75	74	rgen 2374	. . . . . . . 8 ⊢ ∀𝑦 ∈ ω (𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)} → suc 𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)})
76		peano5 4321	. . . . . . . 8 ⊢ ((∅ ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)} ∧ ∀𝑦 ∈ ω (𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)} → suc 𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)})) → ω ⊆ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)})
77	13, 75, 76	mp2an 402	. . . . . . 7 ⊢ ω ⊆ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)}
78	77	sseli 2941	. . . . . 6 ⊢ (𝑥 ∈ ω → 𝑥 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)})
79		abid 2028	. . . . . 6 ⊢ (𝑥 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)} ↔ (𝑥 = ∅ ∨ 𝜑))
80	78, 79	sylib 127	. . . . 5 ⊢ (𝑥 ∈ ω → (𝑥 = ∅ ∨ 𝜑))
81	80	adantr 261	. . . 4 ⊢ ((𝑥 ∈ ω ∧ 𝑥 ≠ ∅) → (𝑥 = ∅ ∨ 𝜑))
82		df-ne 2206	. . . . . 6 ⊢ (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅)
83		biorf 663	. . . . . 6 ⊢ (¬ 𝑥 = ∅ → (𝜑 ↔ (𝑥 = ∅ ∨ 𝜑)))
84	82, 83	sylbi 114	. . . . 5 ⊢ (𝑥 ≠ ∅ → (𝜑 ↔ (𝑥 = ∅ ∨ 𝜑)))
85	84	adantl 262	. . . 4 ⊢ ((𝑥 ∈ ω ∧ 𝑥 ≠ ∅) → (𝜑 ↔ (𝑥 = ∅ ∨ 𝜑)))
86	81, 85	mpbird 156	. . 3 ⊢ ((𝑥 ∈ ω ∧ 𝑥 ≠ ∅) → 𝜑)
87	2, 86	sylbi 114	. 2 ⊢ (𝑥 ∈ N → 𝜑)
88	1, 87	vtoclga 2619	1 ⊢ (𝐴 ∈ N → 𝜏)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98   ∨ wo 629  DECID wdc 742   = wceq 1243   ∈ wcel 1393  {cab 2026   ≠ wne 2204  ∀wral 2306  [wsbc 2764   ⊆ wss 2917  ∅c0 3224  Oncon0 4100  suc csuc 4102  ωcom 4313  (class class class)co 5512  1_𝑜c1o 5994   +_𝑜 coa 5998  Ncnpi 6370   +_N cpli 6371

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-13 1404  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-coll 3872  ax-sep 3875  ax-nul 3883  ax-pow 3927  ax-pr 3944  ax-un 4170  ax-setind 4262  ax-iinf 4311

This theorem depends on definitions:  df-bi 110  df-dc 743  df-3an 887  df-tru 1246  df-fal 1249  df-nf 1350  df-sb 1646  df-eu 1903  df-mo 1904  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ne 2206  df-ral 2311  df-rex 2312  df-reu 2313  df-rab 2315  df-v 2559  df-sbc 2765  df-csb 2853  df-dif 2920  df-un 2922  df-in 2924  df-ss 2931  df-nul 3225  df-pw 3361  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-int 3616  df-iun 3659  df-br 3765  df-opab 3819  df-mpt 3820  df-tr 3855  df-id 4030  df-iord 4103  df-on 4105  df-suc 4108  df-iom 4314  df-xp 4351  df-rel 4352  df-cnv 4353  df-co 4354  df-dm 4355  df-rn 4356  df-res 4357  df-ima 4358  df-iota 4867  df-fun 4904  df-fn 4905  df-f 4906  df-f1 4907  df-fo 4908  df-f1o 4909  df-fv 4910  df-ov 5515  df-oprab 5516  df-mpt2 5517  df-1st 5767  df-2nd 5768  df-recs 5920  df-irdg 5957  df-1o 6001  df-oadd 6005  df-ni 6402  df-pli 6403

This theorem is referenced by:  pitonn  6924