Theorem nnind 12222

Description: Principle of Mathematical Induction (inference schema). The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. See nnaddcl 12227 for an example of its use. See nn0ind 12662 for induction on nonnegative integers and uzind 12659, uzind4 12901 for induction on an arbitrary upper set of integers. See indstr 12911 for strong induction. See also nnindALT 12223. This is an alternative for Metamath 100 proof #74. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 16-Jun-2013.)

Hypotheses

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

Assertion

Ref	Expression
nnind	⊢ (𝐴 ∈ ℕ → 𝜏)

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

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

Proof of Theorem nnind

Step	Hyp	Ref	Expression
1		1nn 12215	. . . . . 6 ⊢ 1 ∈ ℕ
2		nnind.5	. . . . . 6 ⊢ 𝜓
3		nnind.1	. . . . . . 7 ⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓))
4	3	elrab 3649	. . . . . 6 ⊢ (1 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ (1 ∈ ℕ ∧ 𝜓))
5	1, 2, 4	mpbir2an 721	. . . . 5 ⊢ 1 ∈ {𝑥 ∈ ℕ ∣ 𝜑}
6		elrabi 3645	. . . . . . 7 ⊢ (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} → 𝑦 ∈ ℕ)
7		peano2nn 12216	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ)
8	7	a1d 25	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ))
9		nnind.6	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → (𝜒 → 𝜃))
10	8, 9	anim12d 618	. . . . . . . 8 ⊢ (𝑦 ∈ ℕ → ((𝑦 ∈ ℕ ∧ 𝜒) → ((𝑦 + 1) ∈ ℕ ∧ 𝜃)))
11		nnind.2	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
12	11	elrab 3649	. . . . . . . 8 ⊢ (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ (𝑦 ∈ ℕ ∧ 𝜒))
13		nnind.3	. . . . . . . . 9 ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃))
14	13	elrab 3649	. . . . . . . 8 ⊢ ((𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ ((𝑦 + 1) ∈ ℕ ∧ 𝜃))
15	10, 12, 14	3imtr4g 298	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} → (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑}))
16	6, 15	mpcom 38	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} → (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑})
17	16	rgen 3077	. . . . 5 ⊢ ∀𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑}
18		peano5nni 12207	. . . . 5 ⊢ ((1 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ∧ ∀𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝜑} (𝑦 + 1) ∈ {𝑥 ∈ ℕ ∣ 𝜑}) → ℕ ⊆ {𝑥 ∈ ℕ ∣ 𝜑})
19	5, 17, 18	mp2an 702	. . . 4 ⊢ ℕ ⊆ {𝑥 ∈ ℕ ∣ 𝜑}
20	19	sseli 3930	. . 3 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ {𝑥 ∈ ℕ ∣ 𝜑})
21		nnind.4	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
22	21	elrab 3649	. . 3 ⊢ (𝐴 ∈ {𝑥 ∈ ℕ ∣ 𝜑} ↔ (𝐴 ∈ ℕ ∧ 𝜏))
23	20, 22	sylib 220	. 2 ⊢ (𝐴 ∈ ℕ → (𝐴 ∈ ℕ ∧ 𝜏))
24	23	simprd 499	1 ⊢ (𝐴 ∈ ℕ → 𝜏)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1559   ∈ wcel 2141  ∀wral 3075  {crab 3413   ⊆ wss 3902  (class class class)co 7391  1c1 11068   + caddc 11070  ℕcn 12204

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pr 5387  ax-un 7713  ax-1cn 11125

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6283  df-ord 6344  df-on 6345  df-lim 6346  df-suc 6347  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-ov 7394  df-om 7842  df-2nd 7966  df-frecs 8256  df-wrecs 8287  df-recs 8336  df-rdg 8375  df-nn 12205

This theorem is referenced by:  nnindALT  12223  nnindd  12224  nn1m1nn  12225  nnaddcl  12227  nnmulcl  12228  nnadd1com  12230  nnaddcom  12231  nnge1  12235  nnne0  12241  nnsub  12251  nnadddir  12263  nnmul1com  12264  nnmulcom  12265  nneo  12651  peano5uzi  12656  nn0ind-raph  12667  ser1const  14065  expcllem  14079  expeq0  14099  expmordi  14174  seqcoll  14471  relexpsucnnl  15037  relexpcnv  15042  relexprelg  15045  relexpnndm  15048  relexpaddnn  15058  climcndslem2  15871  sqrt2irr  16272  rplpwr  16583  prmind2  16710  prmdvdsexp  16741  eulerthlem2  16808  pcmpt  16919  prmpwdvds  16931  vdwlem10  17017  mulgnnass  19142  ofldchr  21616  imasdsf1olem  24421  ovolunlem1a  25546  ovolicc2lem3  25569  voliunlem1  25600  volsup  25606  dvexp  26003  plyco  26289  dgrcolem1  26321  vieta1  26364  emcllem6  27053  bposlem5  27340  2sqlem10  27480  dchrisum0flb  27562  iuninc  32720  nexple  32996  esumfzf  34327  rrvsum  34712  subfacp1lem6  35496  cvmliftlem10  35605  bcprod  36049  faclimlem1  36054  incsequz  38208  bfplem1  38282  nnn1suc  42842  2nn0ind  43483  relexpxpnnidm  44240  relexpss1d  44242  iunrelexpmin1  44245  relexpmulnn  44246  trclrelexplem  44248  iunrelexpmin2  44249  relexp0a  44253  cotrcltrcl  44262  trclimalb2  44263  cotrclrcl  44279  inductionexd  44692  fmuldfeq  46120  dvnmptconst  46476  stoweidlem20  46555  wallispilem4  46603  wallispi2lem1  46606  wallispi2lem2  46607  dirkertrigeqlem1  46633  iccelpart  48000  nn0sumshdiglem2  49205