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

Theorem evenoddnnnul 4514
 Description: Every nonempty finite cardinal is either even or odd. Theorem X.1.35 of [Rosser] p. 529. (Contributed by SF, 20-Jan-2015.)
Assertion
Ref Expression
evenoddnnnul ( EvenfinOddfin ) = ( Nn {})

Proof of Theorem evenoddnnnul
Dummy variables x k n m are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 evennn 4506 . . . . . 6 (x Evenfinx Nn )
2 evennnul 4508 . . . . . 6 (x Evenfinx)
3 eldifsn 3839 . . . . . 6 (x ( Nn {}) ↔ (x Nn x))
41, 2, 3sylanbrc 645 . . . . 5 (x Evenfinx ( Nn {}))
54ssriv 3277 . . . 4 Evenfin ( Nn {})
6 oddnn 4507 . . . . . 6 (x Oddfinx Nn )
7 oddnnul 4509 . . . . . 6 (x Oddfinx)
86, 7, 3sylanbrc 645 . . . . 5 (x Oddfinx ( Nn {}))
98ssriv 3277 . . . 4 Oddfin ( Nn {})
105, 9pm3.2i 441 . . 3 ( Evenfin ( Nn {}) Oddfin ( Nn {}))
11 unss 3437 . . 3 (( Evenfin ( Nn {}) Oddfin ( Nn {})) ↔ ( EvenfinOddfin ) ( Nn {}))
1210, 11mpbi 199 . 2 ( EvenfinOddfin ) ( Nn {})
13 eldifsn 3839 . . . 4 (n ( Nn {}) ↔ (n Nn n))
14 vex 2862 . . . . . . . . . . . 12 m V
1514elsnc 3756 . . . . . . . . . . 11 (m {} ↔ m = )
16 df-ne 2518 . . . . . . . . . . . 12 (m ↔ ¬ m = )
1716con2bii 322 . . . . . . . . . . 11 (m = ↔ ¬ m)
1815, 17bitri 240 . . . . . . . . . 10 (m {} ↔ ¬ m)
1918orbi1i 506 . . . . . . . . 9 ((m {} m ( EvenfinOddfin )) ↔ (¬ m m ( EvenfinOddfin )))
20 elun 3220 . . . . . . . . 9 (m ({} ∪ ( EvenfinOddfin )) ↔ (m {} m ( EvenfinOddfin )))
21 imor 401 . . . . . . . . 9 ((mm ( EvenfinOddfin )) ↔ (¬ m m ( EvenfinOddfin )))
2219, 20, 213bitr4i 268 . . . . . . . 8 (m ({} ∪ ( EvenfinOddfin )) ↔ (mm ( EvenfinOddfin )))
2322abbi2i 2464 . . . . . . 7 ({} ∪ ( EvenfinOddfin )) = {m (mm ( EvenfinOddfin ))}
24 snex 4111 . . . . . . . 8 {} V
25 evenfinex 4503 . . . . . . . . 9 Evenfin V
26 oddfinex 4504 . . . . . . . . 9 Oddfin V
2725, 26unex 4106 . . . . . . . 8 ( EvenfinOddfin ) V
2824, 27unex 4106 . . . . . . 7 ({} ∪ ( EvenfinOddfin )) V
2923, 28eqeltrri 2424 . . . . . 6 {m (mm ( EvenfinOddfin ))} V
30 neeq1 2524 . . . . . . 7 (m = 0c → (m ↔ 0c))
31 eleq1 2413 . . . . . . 7 (m = 0c → (m ( EvenfinOddfin ) ↔ 0c ( EvenfinOddfin )))
3230, 31imbi12d 311 . . . . . 6 (m = 0c → ((mm ( EvenfinOddfin )) ↔ (0c → 0c ( EvenfinOddfin ))))
33 neeq1 2524 . . . . . . 7 (m = k → (mk))
34 eleq1 2413 . . . . . . 7 (m = k → (m ( EvenfinOddfin ) ↔ k ( EvenfinOddfin )))
3533, 34imbi12d 311 . . . . . 6 (m = k → ((mm ( EvenfinOddfin )) ↔ (kk ( EvenfinOddfin ))))
36 neeq1 2524 . . . . . . 7 (m = (k +c 1c) → (m ↔ (k +c 1c) ≠ ))
37 eleq1 2413 . . . . . . 7 (m = (k +c 1c) → (m ( EvenfinOddfin ) ↔ (k +c 1c) ( EvenfinOddfin )))
3836, 37imbi12d 311 . . . . . 6 (m = (k +c 1c) → ((mm ( EvenfinOddfin )) ↔ ((k +c 1c) ≠ → (k +c 1c) ( EvenfinOddfin ))))
39 neeq1 2524 . . . . . . 7 (m = n → (mn))
40 eleq1 2413 . . . . . . 7 (m = n → (m ( EvenfinOddfin ) ↔ n ( EvenfinOddfin )))
4139, 40imbi12d 311 . . . . . 6 (m = n → ((mm ( EvenfinOddfin )) ↔ (nn ( EvenfinOddfin ))))
42 ssun1 3426 . . . . . . . 8 Evenfin ( EvenfinOddfin )
43 0ceven 4505 . . . . . . . 8 0c Evenfin
4442, 43sselii 3270 . . . . . . 7 0c ( EvenfinOddfin )
4544a1i 10 . . . . . 6 (0c → 0c ( EvenfinOddfin ))
46 addcnnul 4453 . . . . . . . . . 10 ((k +c 1c) ≠ → (k 1c))
4746simpld 445 . . . . . . . . 9 ((k +c 1c) ≠ k)
48 sucevenodd 4510 . . . . . . . . . . . 12 ((k Evenfin (k +c 1c) ≠ ) → (k +c 1c) Oddfin )
4948expcom 424 . . . . . . . . . . 11 ((k +c 1c) ≠ → (k Evenfin → (k +c 1c) Oddfin ))
50 sucoddeven 4511 . . . . . . . . . . . 12 ((k Oddfin (k +c 1c) ≠ ) → (k +c 1c) Evenfin )
5150expcom 424 . . . . . . . . . . 11 ((k +c 1c) ≠ → (k Oddfin → (k +c 1c) Evenfin ))
5249, 51orim12d 811 . . . . . . . . . 10 ((k +c 1c) ≠ → ((k Evenfin k Oddfin ) → ((k +c 1c) Oddfin (k +c 1c) Evenfin )))
53 elun 3220 . . . . . . . . . 10 (k ( EvenfinOddfin ) ↔ (k Evenfin k Oddfin ))
54 elun 3220 . . . . . . . . . . 11 ((k +c 1c) ( EvenfinOddfin ) ↔ ((k +c 1c) Evenfin (k +c 1c) Oddfin ))
55 orcom 376 . . . . . . . . . . 11 (((k +c 1c) Evenfin (k +c 1c) Oddfin ) ↔ ((k +c 1c) Oddfin (k +c 1c) Evenfin ))
5654, 55bitri 240 . . . . . . . . . 10 ((k +c 1c) ( EvenfinOddfin ) ↔ ((k +c 1c) Oddfin (k +c 1c) Evenfin ))
5752, 53, 563imtr4g 261 . . . . . . . . 9 ((k +c 1c) ≠ → (k ( EvenfinOddfin ) → (k +c 1c) ( EvenfinOddfin )))
5847, 57embantd 50 . . . . . . . 8 ((k +c 1c) ≠ → ((kk ( EvenfinOddfin )) → (k +c 1c) ( EvenfinOddfin )))
5958com12 27 . . . . . . 7 ((kk ( EvenfinOddfin )) → ((k +c 1c) ≠ → (k +c 1c) ( EvenfinOddfin )))
6059a1i 10 . . . . . 6 (k Nn → ((kk ( EvenfinOddfin )) → ((k +c 1c) ≠ → (k +c 1c) ( EvenfinOddfin ))))
6129, 32, 35, 38, 41, 45, 60finds 4411 . . . . 5 (n Nn → (nn ( EvenfinOddfin )))
6261imp 418 . . . 4 ((n Nn n) → n ( EvenfinOddfin ))
6313, 62sylbi 187 . . 3 (n ( Nn {}) → n ( EvenfinOddfin ))
6463ssriv 3277 . 2 ( Nn {}) ( EvenfinOddfin )
6512, 64eqssi 3288 1 ( EvenfinOddfin ) = ( Nn {})
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 357   ∧ wa 358   = wceq 1642   ∈ wcel 1710  {cab 2339   ≠ wne 2516  Vcvv 2859   ∖ cdif 3206   ∪ cun 3207   ⊆ wss 3257  ∅c0 3550  {csn 3737  1cc1c 4134   Nn cnnc 4373  0cc0c 4374   +c cplc 4375   Evenfin cevenfin 4436   Oddfin coddfin 4437 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-idk 4195  df-0c 4377  df-addc 4378  df-nnc 4379  df-evenfin 4444  df-oddfin 4445 This theorem is referenced by:  vinf  4555
 Copyright terms: Public domain W3C validator