Theorem indpi 6532

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 6498	. . 3 ⊢ (𝑥 ∈ N ↔ (𝑥 ∈ ω ∧ 𝑥 ≠ ∅))
3		eqid 2081	. . . . . . . . . 10 ⊢ ∅ = ∅
4	3	orci 682	. . . . . . . . 9 ⊢ (∅ = ∅ ∨ [∅ / 𝑥]𝜑)
5		nfv 1461	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∅ = ∅
6		nfsbc1v 2833	. . . . . . . . . . 11 ⊢ Ⅎ𝑥[∅ / 𝑥]𝜑
7	5, 6	nfor 1506	. . . . . . . . . 10 ⊢ Ⅎ𝑥(∅ = ∅ ∨ [∅ / 𝑥]𝜑)
8		0ex 3905	. . . . . . . . . 10 ⊢ ∅ ∈ V
9		eqeq1 2087	. . . . . . . . . . 11 ⊢ (𝑥 = ∅ → (𝑥 = ∅ ↔ ∅ = ∅))
10		sbceq1a 2824	. . . . . . . . . . 11 ⊢ (𝑥 = ∅ → (𝜑 ↔ [∅ / 𝑥]𝜑))
11	9, 10	orbi12d 739	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → ((𝑥 = ∅ ∨ 𝜑) ↔ (∅ = ∅ ∨ [∅ / 𝑥]𝜑)))
12	7, 8, 11	elabf 2737	. . . . . . . . 9 ⊢ (∅ ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)} ↔ (∅ = ∅ ∨ [∅ / 𝑥]𝜑))
13	4, 12	mpbir 144	. . . . . . . 8 ⊢ ∅ ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)}
14		suceq 4157	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ∅ → suc 𝑦 = suc ∅)
15		df-1o 6024	. . . . . . . . . . . . . 14 ⊢ 1𝑜 = suc ∅
16	14, 15	syl6eqr 2131	. . . . . . . . . . . . 13 ⊢ (𝑦 = ∅ → suc 𝑦 = 1𝑜)
17		indpi.5	. . . . . . . . . . . . . . 15 ⊢ 𝜓
18	17	olci 683	. . . . . . . . . . . . . 14 ⊢ (1𝑜 = ∅ ∨ 𝜓)
19		1onn 6116	. . . . . . . . . . . . . . . 16 ⊢ 1𝑜 ∈ ω
20	19	elexi 2611	. . . . . . . . . . . . . . 15 ⊢ 1𝑜 ∈ V
21		eqeq1 2087	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 1𝑜 → (𝑥 = ∅ ↔ 1𝑜 = ∅))
22		indpi.1	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 1𝑜 → (𝜑 ↔ 𝜓))
23	21, 22	orbi12d 739	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 1𝑜 → ((𝑥 = ∅ ∨ 𝜑) ↔ (1𝑜 = ∅ ∨ 𝜓)))
24	20, 23	elab 2738	. . . . . . . . . . . . . 14 ⊢ (1𝑜 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)} ↔ (1𝑜 = ∅ ∨ 𝜓))
25	18, 24	mpbir 144	. . . . . . . . . . . . 13 ⊢ 1𝑜 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)}
26	16, 25	syl6eqel 2169	. . . . . . . . . . . 12 ⊢ (𝑦 = ∅ → suc 𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)})
27	26	a1d 22	. . . . . . . . . . 11 ⊢ (𝑦 = ∅ → (𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)} → suc 𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)}))
28	27	a1i 9	. . . . . . . . . 10 ⊢ (𝑦 ∈ ω → (𝑦 = ∅ → (𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)} → suc 𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)})))
29		indpi.6	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ N → (𝜒 → 𝜃))
30		elni 6498	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ N ↔ (𝑦 ∈ ω ∧ 𝑦 ≠ ∅))
31	30	simprbi 269	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ N → 𝑦 ≠ ∅)
32	31	neneqd 2266	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ N → ¬ 𝑦 = ∅)
33		biorf 695	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑦 = ∅ → (𝜒 ↔ (𝑦 = ∅ ∨ 𝜒)))
34	32, 33	syl 14	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ N → (𝜒 ↔ (𝑦 = ∅ ∨ 𝜒)))
35		vex 2604	. . . . . . . . . . . . . 14 ⊢ 𝑦 ∈ V
36		eqeq1 2087	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝑥 = ∅ ↔ 𝑦 = ∅))
37		indpi.2	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
38	36, 37	orbi12d 739	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((𝑥 = ∅ ∨ 𝜑) ↔ (𝑦 = ∅ ∨ 𝜒)))
39	35, 38	elab 2738	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)} ↔ (𝑦 = ∅ ∨ 𝜒))
40	34, 39	syl6bbr 196	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ N → (𝜒 ↔ 𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)}))
41		1pi 6505	. . . . . . . . . . . . . . . . . 18 ⊢ 1𝑜 ∈ N
42		addclpi 6517	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ N ∧ 1𝑜 ∈ N) → (𝑦 +N 1𝑜) ∈ N)
43	41, 42	mpan2 415	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ N → (𝑦 +N 1𝑜) ∈ N)
44		elni 6498	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 +N 1𝑜) ∈ N ↔ ((𝑦 +N 1𝑜) ∈ ω ∧ (𝑦 +N 1𝑜) ≠ ∅))
45	43, 44	sylib 120	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ N → ((𝑦 +N 1𝑜) ∈ ω ∧ (𝑦 +N 1𝑜) ≠ ∅))
46	45	simprd 112	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ N → (𝑦 +N 1𝑜) ≠ ∅)
47	46	neneqd 2266	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ N → ¬ (𝑦 +N 1𝑜) = ∅)
48		biorf 695	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑦 +N 1𝑜) = ∅ → (𝜃 ↔ ((𝑦 +N 1𝑜) = ∅ ∨ 𝜃)))
49	47, 48	syl 14	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ N → (𝜃 ↔ ((𝑦 +N 1𝑜) = ∅ ∨ 𝜃)))
50		eqeq1 2087	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝑦 +N 1𝑜) → (𝑥 = ∅ ↔ (𝑦 +N 1𝑜) = ∅))
51		indpi.3	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝑦 +N 1𝑜) → (𝜑 ↔ 𝜃))
52	50, 51	orbi12d 739	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑦 +N 1𝑜) → ((𝑥 = ∅ ∨ 𝜑) ↔ ((𝑦 +N 1𝑜) = ∅ ∨ 𝜃)))
53	52	elabg 2739	. . . . . . . . . . . . . 14 ⊢ ((𝑦 +N 1𝑜) ∈ N → ((𝑦 +N 1𝑜) ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)} ↔ ((𝑦 +N 1𝑜) = ∅ ∨ 𝜃)))
54	43, 53	syl 14	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ N → ((𝑦 +N 1𝑜) ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)} ↔ ((𝑦 +N 1𝑜) = ∅ ∨ 𝜃)))
55		addpiord 6506	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ N ∧ 1𝑜 ∈ N) → (𝑦 +N 1𝑜) = (𝑦 +𝑜 1𝑜))
56	41, 55	mpan2 415	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ N → (𝑦 +N 1𝑜) = (𝑦 +𝑜 1𝑜))
57		pion 6500	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ N → 𝑦 ∈ On)
58		oa1suc 6070	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ On → (𝑦 +𝑜 1𝑜) = suc 𝑦)
59	57, 58	syl 14	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ N → (𝑦 +𝑜 1𝑜) = suc 𝑦)
60	56, 59	eqtrd 2113	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ N → (𝑦 +N 1𝑜) = suc 𝑦)
61	60	eleq1d 2147	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ N → ((𝑦 +N 1𝑜) ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)} ↔ suc 𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)}))
62	49, 54, 61	3bitr2d 214	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ N → (𝜃 ↔ suc 𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)}))
63	29, 40, 62	3imtr3d 200	. . . . . . . . . . 11 ⊢ (𝑦 ∈ N → (𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)} → suc 𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)}))
64	63	a1i 9	. . . . . . . . . 10 ⊢ (𝑦 ∈ ω → (𝑦 ∈ N → (𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)} → suc 𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)})))
65		nndceq0 4357	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ω → DECID 𝑦 = ∅)
66		df-dc 776	. . . . . . . . . . . 12 ⊢ (DECID 𝑦 = ∅ ↔ (𝑦 = ∅ ∨ ¬ 𝑦 = ∅))
67	65, 66	sylib 120	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ω → (𝑦 = ∅ ∨ ¬ 𝑦 = ∅))
68		idd 21	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ω → (𝑦 = ∅ → 𝑦 = ∅))
69	68	necon3bd 2288	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ω → (¬ 𝑦 = ∅ → 𝑦 ≠ ∅))
70	69	anc2li 322	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ω → (¬ 𝑦 = ∅ → (𝑦 ∈ ω ∧ 𝑦 ≠ ∅)))
71	70, 30	syl6ibr 160	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ω → (¬ 𝑦 = ∅ → 𝑦 ∈ N))
72	71	orim2d 734	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ω → ((𝑦 = ∅ ∨ ¬ 𝑦 = ∅) → (𝑦 = ∅ ∨ 𝑦 ∈ N)))
73	67, 72	mpd 13	. . . . . . . . . 10 ⊢ (𝑦 ∈ ω → (𝑦 = ∅ ∨ 𝑦 ∈ N))
74	28, 64, 73	mpjaod 670	. . . . . . . . 9 ⊢ (𝑦 ∈ ω → (𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)} → suc 𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)}))
75	74	rgen 2416	. . . . . . . 8 ⊢ ∀𝑦 ∈ ω (𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)} → suc 𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)})
76		peano5 4339	. . . . . . . 8 ⊢ ((∅ ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)} ∧ ∀𝑦 ∈ ω (𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)} → suc 𝑦 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)})) → ω ⊆ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)})
77	13, 75, 76	mp2an 416	. . . . . . 7 ⊢ ω ⊆ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)}
78	77	sseli 2995	. . . . . 6 ⊢ (𝑥 ∈ ω → 𝑥 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)})
79		abid 2069	. . . . . 6 ⊢ (𝑥 ∈ {𝑥 ∣ (𝑥 = ∅ ∨ 𝜑)} ↔ (𝑥 = ∅ ∨ 𝜑))
80	78, 79	sylib 120	. . . . 5 ⊢ (𝑥 ∈ ω → (𝑥 = ∅ ∨ 𝜑))
81	80	adantr 270	. . . 4 ⊢ ((𝑥 ∈ ω ∧ 𝑥 ≠ ∅) → (𝑥 = ∅ ∨ 𝜑))
82		df-ne 2246	. . . . . 6 ⊢ (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅)
83		biorf 695	. . . . . 6 ⊢ (¬ 𝑥 = ∅ → (𝜑 ↔ (𝑥 = ∅ ∨ 𝜑)))
84	82, 83	sylbi 119	. . . . 5 ⊢ (𝑥 ≠ ∅ → (𝜑 ↔ (𝑥 = ∅ ∨ 𝜑)))
85	84	adantl 271	. . . 4 ⊢ ((𝑥 ∈ ω ∧ 𝑥 ≠ ∅) → (𝜑 ↔ (𝑥 = ∅ ∨ 𝜑)))
86	81, 85	mpbird 165	. . 3 ⊢ ((𝑥 ∈ ω ∧ 𝑥 ≠ ∅) → 𝜑)
87	2, 86	sylbi 119	. 2 ⊢ (𝑥 ∈ N → 𝜑)
88	1, 87	vtoclga 2664	1 ⊢ (𝐴 ∈ N → 𝜏)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 102   ↔ wb 103   ∨ wo 661  DECID wdc 775   = wceq 1284   ∈ wcel 1433  {cab 2067   ≠ wne 2245  ∀wral 2348  [wsbc 2815   ⊆ wss 2973  ∅c0 3251  Oncon0 4118  suc csuc 4120  ωcom 4331  (class class class)co 5532  1_𝑜c1o 6017   +_𝑜 coa 6021  Ncnpi 6462   +_N cpli 6463

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 576  ax-in2 577  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-13 1444  ax-14 1445  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-coll 3893  ax-sep 3896  ax-nul 3904  ax-pow 3948  ax-pr 3964  ax-un 4188  ax-setind 4280  ax-iinf 4329

This theorem depends on definitions:  df-bi 115  df-dc 776  df-3an 921  df-tru 1287  df-fal 1290  df-nf 1390  df-sb 1686  df-eu 1944  df-mo 1945  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-ne 2246  df-ral 2353  df-rex 2354  df-reu 2355  df-rab 2357  df-v 2603  df-sbc 2816  df-csb 2909  df-dif 2975  df-un 2977  df-in 2979  df-ss 2986  df-nul 3252  df-pw 3384  df-sn 3404  df-pr 3405  df-op 3407  df-uni 3602  df-int 3637  df-iun 3680  df-br 3786  df-opab 3840  df-mpt 3841  df-tr 3876  df-id 4048  df-iord 4121  df-on 4123  df-suc 4126  df-iom 4332  df-xp 4369  df-rel 4370  df-cnv 4371  df-co 4372  df-dm 4373  df-rn 4374  df-res 4375  df-ima 4376  df-iota 4887  df-fun 4924  df-fn 4925  df-f 4926  df-f1 4927  df-fo 4928  df-f1o 4929  df-fv 4930  df-ov 5535  df-oprab 5536  df-mpt2 5537  df-1st 5787  df-2nd 5788  df-recs 5943  df-irdg 5980  df-1o 6024  df-oadd 6028  df-ni 6494  df-pli 6495

This theorem is referenced by:  pitonn  7016