NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  peano5 GIF version

Theorem peano5 4409
Description: The principle of mathematical induction: a set containing cardinal zero and closed under the successor operator is a superset of the finite cardinals. Theorem X.1.6 of [Rosser] p. 276. (Contributed by SF, 14-Jan-2015.)
Assertion
Ref Expression
peano5 ((A V 0c A x Nn (x A → (x +c 1c) A)) → Nn A)
Distinct variable group:   x,A
Allowed substitution hint:   V(x)

Proof of Theorem peano5
Dummy variable y is distinct from all other variables.
StepHypRef Expression
1 nncex 4396 . . 3 Nn V
2 inexg 4100 . . 3 (( Nn V A V) → ( NnA) V)
31, 2mpan 651 . 2 (A V → ( NnA) V)
4 peano1 4402 . . 3 0c Nn
5 elin 3219 . . . 4 (0c ( NnA) ↔ (0c Nn 0c A))
65biimpri 197 . . 3 ((0c Nn 0c A) → 0c ( NnA))
74, 6mpan 651 . 2 (0c A → 0c ( NnA))
8 elin 3219 . . . . . 6 (x ( NnA) ↔ (x Nn x A))
98imbi1i 315 . . . . 5 ((x ( NnA) → (x +c 1c) A) ↔ ((x Nn x A) → (x +c 1c) A))
10 impexp 433 . . . . 5 (((x Nn x A) → (x +c 1c) A) ↔ (x Nn → (x A → (x +c 1c) A)))
119, 10bitri 240 . . . 4 ((x ( NnA) → (x +c 1c) A) ↔ (x Nn → (x A → (x +c 1c) A)))
12 inss1 3475 . . . . . . . 8 ( NnA) Nn
1312sseli 3269 . . . . . . 7 (x ( NnA) → x Nn )
14 peano2 4403 . . . . . . 7 (x Nn → (x +c 1c) Nn )
1513, 14syl 15 . . . . . 6 (x ( NnA) → (x +c 1c) Nn )
16 elin 3219 . . . . . . . 8 ((x +c 1c) ( NnA) ↔ ((x +c 1c) Nn (x +c 1c) A))
1716biimpri 197 . . . . . . 7 (((x +c 1c) Nn (x +c 1c) A) → (x +c 1c) ( NnA))
1817a1i 10 . . . . . 6 (x ( NnA) → (((x +c 1c) Nn (x +c 1c) A) → (x +c 1c) ( NnA)))
1915, 18mpand 656 . . . . 5 (x ( NnA) → ((x +c 1c) A → (x +c 1c) ( NnA)))
2019a2i 12 . . . 4 ((x ( NnA) → (x +c 1c) A) → (x ( NnA) → (x +c 1c) ( NnA)))
2111, 20sylbir 204 . . 3 ((x Nn → (x A → (x +c 1c) A)) → (x ( NnA) → (x +c 1c) ( NnA)))
2221ralimi2 2686 . 2 (x Nn (x A → (x +c 1c) A) → x ( NnA)(x +c 1c) ( NnA))
23 df-nnc 4379 . . . 4 Nn = {y (0c y x y (x +c 1c) y)}
24 eleq2 2414 . . . . . . . . 9 (y = ( NnA) → (0c y ↔ 0c ( NnA)))
25 eleq2 2414 . . . . . . . . . 10 (y = ( NnA) → ((x +c 1c) y ↔ (x +c 1c) ( NnA)))
2625raleqbi1dv 2815 . . . . . . . . 9 (y = ( NnA) → (x y (x +c 1c) yx ( NnA)(x +c 1c) ( NnA)))
2724, 26anbi12d 691 . . . . . . . 8 (y = ( NnA) → ((0c y x y (x +c 1c) y) ↔ (0c ( NnA) x ( NnA)(x +c 1c) ( NnA))))
2827elabg 2986 . . . . . . 7 (( NnA) V → (( NnA) {y (0c y x y (x +c 1c) y)} ↔ (0c ( NnA) x ( NnA)(x +c 1c) ( NnA))))
2928biimprd 214 . . . . . 6 (( NnA) V → ((0c ( NnA) x ( NnA)(x +c 1c) ( NnA)) → ( NnA) {y (0c y x y (x +c 1c) y)}))
30293impib 1149 . . . . 5 ((( NnA) V 0c ( NnA) x ( NnA)(x +c 1c) ( NnA)) → ( NnA) {y (0c y x y (x +c 1c) y)})
31 intss1 3941 . . . . 5 (( NnA) {y (0c y x y (x +c 1c) y)} → {y (0c y x y (x +c 1c) y)} ( NnA))
3230, 31syl 15 . . . 4 ((( NnA) V 0c ( NnA) x ( NnA)(x +c 1c) ( NnA)) → {y (0c y x y (x +c 1c) y)} ( NnA))
3323, 32syl5eqss 3315 . . 3 ((( NnA) V 0c ( NnA) x ( NnA)(x +c 1c) ( NnA)) → Nn ( NnA))
34 inss2 3476 . . 3 ( NnA) A
3533, 34syl6ss 3284 . 2 ((( NnA) V 0c ( NnA) x ( NnA)(x +c 1c) ( NnA)) → Nn A)
363, 7, 22, 35syl3an 1224 1 ((A V 0c A x Nn (x A → (x +c 1c) A)) → Nn A)
Colors of variables: wff setvar class
Syntax hints:  wi 4   wa 358   w3a 934   = wceq 1642   wcel 1710  {cab 2339  wral 2614  Vcvv 2859  cin 3208   wss 3257  cint 3926  1cc1c 4134   Nn cnnc 4373  0cc0c 4374   +c cplc 4375
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-0c 4377  df-addc 4378  df-nnc 4379
This theorem is referenced by:  findsd  4410  dmfrec  6316
  Copyright terms: Public domain W3C validator