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

Theorem nnc0suc 4412
Description: All naturals are either zero or a successor. Theorem X.1.7 of [Rosser] p. 276. (Contributed by SF, 14-Jan-2015.)
Assertion
Ref Expression
nnc0suc (A Nn ↔ (A = 0c x Nn A = (x +c 1c)))
Distinct variable group:   x,A

Proof of Theorem nnc0suc
Dummy variables n m are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-sn 3741 . . . . . 6 {0c} = {n n = 0c}
2 vex 2862 . . . . . . . . 9 n V
32elimak 4259 . . . . . . . 8 (n (Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) “k Nn ) ↔ x Nnx, n Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c))
4 vex 2862 . . . . . . . . . . 11 x V
5 opkelimagekg 4271 . . . . . . . . . . 11 ((x V n V) → (⟪x, n Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ↔ n = ((( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) “k x)))
64, 2, 5mp2an 653 . . . . . . . . . 10 (⟪x, n Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ↔ n = ((( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) “k x))
7 dfaddc2 4381 . . . . . . . . . . 11 (x +c 1c) = ((( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) “k x)
87eqeq2i 2363 . . . . . . . . . 10 (n = (x +c 1c) ↔ n = ((( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) “k x))
96, 8bitr4i 243 . . . . . . . . 9 (⟪x, n Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ↔ n = (x +c 1c))
109rexbii 2639 . . . . . . . 8 (x Nnx, n Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ↔ x Nn n = (x +c 1c))
113, 10bitri 240 . . . . . . 7 (n (Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) “k Nn ) ↔ x Nn n = (x +c 1c))
1211abbi2i 2464 . . . . . 6 (Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) “k Nn ) = {n x Nn n = (x +c 1c)}
131, 12uneq12i 3416 . . . . 5 ({0c} ∪ (Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) “k Nn )) = ({n n = 0c} ∪ {n x Nn n = (x +c 1c)})
14 unab 3521 . . . . 5 ({n n = 0c} ∪ {n x Nn n = (x +c 1c)}) = {n (n = 0c x Nn n = (x +c 1c))}
1513, 14eqtri 2373 . . . 4 ({0c} ∪ (Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) “k Nn )) = {n (n = 0c x Nn n = (x +c 1c))}
16 snex 4111 . . . . 5 {0c} V
17 addcexlem 4382 . . . . . . . 8 ( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) V
18 1cex 4142 . . . . . . . . . 10 1c V
1918pw1ex 4303 . . . . . . . . 9 11c V
2019pw1ex 4303 . . . . . . . 8 111c V
2117, 20imakex 4300 . . . . . . 7 (( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) V
2221imagekex 4312 . . . . . 6 Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) V
23 nncex 4396 . . . . . 6 Nn V
2422, 23imakex 4300 . . . . 5 (Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) “k Nn ) V
2516, 24unex 4106 . . . 4 ({0c} ∪ (Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) “k Nn )) V
2615, 25eqeltrri 2424 . . 3 {n (n = 0c x Nn n = (x +c 1c))} V
27 eqeq1 2359 . . . 4 (n = 0c → (n = 0c ↔ 0c = 0c))
28 eqeq1 2359 . . . . 5 (n = 0c → (n = (x +c 1c) ↔ 0c = (x +c 1c)))
2928rexbidv 2635 . . . 4 (n = 0c → (x Nn n = (x +c 1c) ↔ x Nn 0c = (x +c 1c)))
3027, 29orbi12d 690 . . 3 (n = 0c → ((n = 0c x Nn n = (x +c 1c)) ↔ (0c = 0c x Nn 0c = (x +c 1c))))
31 eqeq1 2359 . . . 4 (n = m → (n = 0cm = 0c))
32 eqeq1 2359 . . . . 5 (n = m → (n = (x +c 1c) ↔ m = (x +c 1c)))
3332rexbidv 2635 . . . 4 (n = m → (x Nn n = (x +c 1c) ↔ x Nn m = (x +c 1c)))
3431, 33orbi12d 690 . . 3 (n = m → ((n = 0c x Nn n = (x +c 1c)) ↔ (m = 0c x Nn m = (x +c 1c))))
35 eqeq1 2359 . . . 4 (n = (m +c 1c) → (n = 0c ↔ (m +c 1c) = 0c))
36 eqeq1 2359 . . . . 5 (n = (m +c 1c) → (n = (x +c 1c) ↔ (m +c 1c) = (x +c 1c)))
3736rexbidv 2635 . . . 4 (n = (m +c 1c) → (x Nn n = (x +c 1c) ↔ x Nn (m +c 1c) = (x +c 1c)))
3835, 37orbi12d 690 . . 3 (n = (m +c 1c) → ((n = 0c x Nn n = (x +c 1c)) ↔ ((m +c 1c) = 0c x Nn (m +c 1c) = (x +c 1c))))
39 eqeq1 2359 . . . 4 (n = A → (n = 0cA = 0c))
40 eqeq1 2359 . . . . 5 (n = A → (n = (x +c 1c) ↔ A = (x +c 1c)))
4140rexbidv 2635 . . . 4 (n = A → (x Nn n = (x +c 1c) ↔ x Nn A = (x +c 1c)))
4239, 41orbi12d 690 . . 3 (n = A → ((n = 0c x Nn n = (x +c 1c)) ↔ (A = 0c x Nn A = (x +c 1c))))
43 eqid 2353 . . . 4 0c = 0c
4443orci 379 . . 3 (0c = 0c x Nn 0c = (x +c 1c))
45 eqid 2353 . . . . . 6 (m +c 1c) = (m +c 1c)
46 addceq1 4383 . . . . . . . 8 (x = m → (x +c 1c) = (m +c 1c))
4746eqeq2d 2364 . . . . . . 7 (x = m → ((m +c 1c) = (x +c 1c) ↔ (m +c 1c) = (m +c 1c)))
4847rspcev 2955 . . . . . 6 ((m Nn (m +c 1c) = (m +c 1c)) → x Nn (m +c 1c) = (x +c 1c))
4945, 48mpan2 652 . . . . 5 (m Nnx Nn (m +c 1c) = (x +c 1c))
5049olcd 382 . . . 4 (m Nn → ((m +c 1c) = 0c x Nn (m +c 1c) = (x +c 1c)))
5150a1d 22 . . 3 (m Nn → ((m = 0c x Nn m = (x +c 1c)) → ((m +c 1c) = 0c x Nn (m +c 1c) = (x +c 1c))))
5226, 30, 34, 38, 42, 44, 51finds 4411 . 2 (A Nn → (A = 0c x Nn A = (x +c 1c)))
53 peano1 4402 . . . 4 0c Nn
54 eleq1 2413 . . . 4 (A = 0c → (A Nn ↔ 0c Nn ))
5553, 54mpbiri 224 . . 3 (A = 0cA Nn )
56 peano2 4403 . . . . 5 (x Nn → (x +c 1c) Nn )
57 eleq1 2413 . . . . 5 (A = (x +c 1c) → (A Nn ↔ (x +c 1c) Nn ))
5856, 57syl5ibrcom 213 . . . 4 (x Nn → (A = (x +c 1c) → A Nn ))
5958rexlimiv 2732 . . 3 (x Nn A = (x +c 1c) → A Nn )
6055, 59jaoi 368 . 2 ((A = 0c x Nn A = (x +c 1c)) → A Nn )
6152, 60impbii 180 1 (A Nn ↔ (A = 0c x Nn A = (x +c 1c)))
Colors of variables: wff setvar class
Syntax hints:  wb 176   wo 357   = wceq 1642   wcel 1710  {cab 2339  wrex 2615  Vcvv 2859  ccompl 3205   cdif 3206  cun 3207  cin 3208  csymdif 3209  {csn 3737  copk 4057  1cc1c 4134  1cpw1 4135   Ins2k cins2k 4176   Ins3k cins3k 4177  k cimak 4179   SIk csik 4181  Imagekcimagek 4182   Sk cssetk 4183   Nn cnnc 4373  0cc0c 4374   +c cplc 4375
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 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:  nndisjeq  4429  lefinlteq  4463  evenodddisj  4516  sfinltfin  4535  phialllem1  4616  nnc3n3p1  6278
  Copyright terms: Public domain W3C validator