Theorem peano2nn 9030

Description: Peano postulate: a successor of a positive integer is a positive integer. (Contributed by NM, 11-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.)

Assertion

Ref	Expression
peano2nn	⊢ (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℕ)

Proof of Theorem peano2nn

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfnn2 9020	. . . . . 6 ⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
2	1	eleq2i 2271	. . . . 5 ⊢ (𝐴 ∈ ℕ ↔ 𝐴 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)})
3		elintg 3892	. . . . 5 ⊢ (𝐴 ∈ ℕ → (𝐴 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 ∈ 𝑧))
4	2, 3	bitrid 192	. . . 4 ⊢ (𝐴 ∈ ℕ → (𝐴 ∈ ℕ ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 ∈ 𝑧))
5	4	ibi 176	. . 3 ⊢ (𝐴 ∈ ℕ → ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 ∈ 𝑧)
6		vex 2774	. . . . . . . 8 ⊢ 𝑧 ∈ V
7		eleq2 2268	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (1 ∈ 𝑥 ↔ 1 ∈ 𝑧))
8		eleq2 2268	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → ((𝑦 + 1) ∈ 𝑥 ↔ (𝑦 + 1) ∈ 𝑧))
9	8	raleqbi1dv 2713	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥 ↔ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))
10	7, 9	anbi12d 473	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → ((1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥) ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧)))
11	6, 10	elab 2916	. . . . . . 7 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))
12	11	simprbi 275	. . . . . 6 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} → ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧)
13		oveq1 5941	. . . . . . . 8 ⊢ (𝑦 = 𝐴 → (𝑦 + 1) = (𝐴 + 1))
14	13	eleq1d 2273	. . . . . . 7 ⊢ (𝑦 = 𝐴 → ((𝑦 + 1) ∈ 𝑧 ↔ (𝐴 + 1) ∈ 𝑧))
15	14	rspcva 2874	. . . . . 6 ⊢ ((𝐴 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧) → (𝐴 + 1) ∈ 𝑧)
16	12, 15	sylan2 286	. . . . 5 ⊢ ((𝐴 ∈ 𝑧 ∧ 𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}) → (𝐴 + 1) ∈ 𝑧)
17	16	expcom 116	. . . 4 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} → (𝐴 ∈ 𝑧 → (𝐴 + 1) ∈ 𝑧))
18	17	ralimia 2566	. . 3 ⊢ (∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 ∈ 𝑧 → ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} (𝐴 + 1) ∈ 𝑧)
19	5, 18	syl 14	. 2 ⊢ (𝐴 ∈ ℕ → ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} (𝐴 + 1) ∈ 𝑧)
20		nnre 9025	. . . 4 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
21		1red 8069	. . . 4 ⊢ (𝐴 ∈ ℕ → 1 ∈ ℝ)
22	20, 21	readdcld 8084	. . 3 ⊢ (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℝ)
23	1	eleq2i 2271	. . . 4 ⊢ ((𝐴 + 1) ∈ ℕ ↔ (𝐴 + 1) ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)})
24		elintg 3892	. . . 4 ⊢ ((𝐴 + 1) ∈ ℝ → ((𝐴 + 1) ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} (𝐴 + 1) ∈ 𝑧))
25	23, 24	bitrid 192	. . 3 ⊢ ((𝐴 + 1) ∈ ℝ → ((𝐴 + 1) ∈ ℕ ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} (𝐴 + 1) ∈ 𝑧))
26	22, 25	syl 14	. 2 ⊢ (𝐴 ∈ ℕ → ((𝐴 + 1) ∈ ℕ ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} (𝐴 + 1) ∈ 𝑧))
27	19, 26	mpbird 167	1 ⊢ (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℕ)

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1372   ∈ wcel 2175  {cab 2190  ∀wral 2483  ∩ cint 3884  (class class class)co 5934  ℝcr 7906  1c1 7908   + caddc 7910  ℕcn 9018

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186  ax-sep 4161  ax-cnex 7998  ax-resscn 7999  ax-1re 8001  ax-addrcl 8004

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ral 2488  df-rex 2489  df-v 2773  df-un 3169  df-in 3171  df-ss 3178  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-int 3885  df-br 4044  df-iota 5229  df-fv 5276  df-ov 5937  df-inn 9019

This theorem is referenced by:  peano2nnd  9033  nnind  9034  nnaddcl  9038  2nn  9180  3nn  9181  4nn  9182  5nn  9183  6nn  9184  7nn  9185  8nn  9186  9nn  9187  nneoor  9457  10nn  9501  nnsplit  10241  fzonn0p1p1  10323  expp1  10672  facp1  10856  resqrexlemfp1  11239  resqrexlemcalc3  11246  trireciplem  11730  trirecip  11731  cvgratnnlemnexp  11754  cvgratz  11762  nno  12136  nnoddm1d2  12140  rplpwr  12267  prmind2  12361  sqrt2irr  12403  pcmpt  12585  pockthi  12600  dec5nprm  12656  mulgnnp1  13384  2sqlem10  15520