Theorem evenoddnnnul 4515

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	⊢ ( Evenfin ∪ Oddfin ) = ( Nn ∖ {∅})

Proof of Theorem evenoddnnnul

Dummy variables x k n m are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		evennn 4507	. . . . . 6 ⊢ (x ∈ Evenfin → x ∈ Nn )
2		evennnul 4509	. . . . . 6 ⊢ (x ∈ Evenfin → x ≠ ∅)
3		eldifsn 3840	. . . . . 6 ⊢ (x ∈ ( Nn ∖ {∅}) ↔ (x ∈ Nn ∧ x ≠ ∅))
4	1, 2, 3	sylanbrc 645	. . . . 5 ⊢ (x ∈ Evenfin → x ∈ ( Nn ∖ {∅}))
5	4	ssriv 3278	. . . 4 ⊢ Evenfin ⊆ ( Nn ∖ {∅})
6		oddnn 4508	. . . . . 6 ⊢ (x ∈ Oddfin → x ∈ Nn )
7		oddnnul 4510	. . . . . 6 ⊢ (x ∈ Oddfin → x ≠ ∅)
8	6, 7, 3	sylanbrc 645	. . . . 5 ⊢ (x ∈ Oddfin → x ∈ ( Nn ∖ {∅}))
9	8	ssriv 3278	. . . 4 ⊢ Oddfin ⊆ ( Nn ∖ {∅})
10	5, 9	pm3.2i 441	. . 3 ⊢ ( Evenfin ⊆ ( Nn ∖ {∅}) ∧ Oddfin ⊆ ( Nn ∖ {∅}))
11		unss 3438	. . 3 ⊢ (( Evenfin ⊆ ( Nn ∖ {∅}) ∧ Oddfin ⊆ ( Nn ∖ {∅})) ↔ ( Evenfin ∪ Oddfin ) ⊆ ( Nn ∖ {∅}))
12	10, 11	mpbi 199	. 2 ⊢ ( Evenfin ∪ Oddfin ) ⊆ ( Nn ∖ {∅})
13		eldifsn 3840	. . . 4 ⊢ (n ∈ ( Nn ∖ {∅}) ↔ (n ∈ Nn ∧ n ≠ ∅))
14		vex 2863	. . . . . . . . . . . 12 ⊢ m ∈ V
15	14	elsnc 3757	. . . . . . . . . . 11 ⊢ (m ∈ {∅} ↔ m = ∅)
16		df-ne 2519	. . . . . . . . . . . 12 ⊢ (m ≠ ∅ ↔ ¬ m = ∅)
17	16	con2bii 322	. . . . . . . . . . 11 ⊢ (m = ∅ ↔ ¬ m ≠ ∅)
18	15, 17	bitri 240	. . . . . . . . . 10 ⊢ (m ∈ {∅} ↔ ¬ m ≠ ∅)
19	18	orbi1i 506	. . . . . . . . 9 ⊢ ((m ∈ {∅} ∨ m ∈ ( Evenfin ∪ Oddfin )) ↔ (¬ m ≠ ∅ ∨ m ∈ ( Evenfin ∪ Oddfin )))
20		elun 3221	. . . . . . . . 9 ⊢ (m ∈ ({∅} ∪ ( Evenfin ∪ Oddfin )) ↔ (m ∈ {∅} ∨ m ∈ ( Evenfin ∪ Oddfin )))
21		imor 401	. . . . . . . . 9 ⊢ ((m ≠ ∅ → m ∈ ( Evenfin ∪ Oddfin )) ↔ (¬ m ≠ ∅ ∨ m ∈ ( Evenfin ∪ Oddfin )))
22	19, 20, 21	3bitr4i 268	. . . . . . . 8 ⊢ (m ∈ ({∅} ∪ ( Evenfin ∪ Oddfin )) ↔ (m ≠ ∅ → m ∈ ( Evenfin ∪ Oddfin )))
23	22	abbi2i 2465	. . . . . . 7 ⊢ ({∅} ∪ ( Evenfin ∪ Oddfin )) = {m ∣ (m ≠ ∅ → m ∈ ( Evenfin ∪ Oddfin ))}
24		snex 4112	. . . . . . . 8 ⊢ {∅} ∈ V
25		evenfinex 4504	. . . . . . . . 9 ⊢ Evenfin ∈ V
26		oddfinex 4505	. . . . . . . . 9 ⊢ Oddfin ∈ V
27	25, 26	unex 4107	. . . . . . . 8 ⊢ ( Evenfin ∪ Oddfin ) ∈ V
28	24, 27	unex 4107	. . . . . . 7 ⊢ ({∅} ∪ ( Evenfin ∪ Oddfin )) ∈ V
29	23, 28	eqeltrri 2424	. . . . . 6 ⊢ {m ∣ (m ≠ ∅ → m ∈ ( Evenfin ∪ Oddfin ))} ∈ V
30		neeq1 2525	. . . . . . 7 ⊢ (m = 0c → (m ≠ ∅ ↔ 0c ≠ ∅))
31		eleq1 2413	. . . . . . 7 ⊢ (m = 0c → (m ∈ ( Evenfin ∪ Oddfin ) ↔ 0c ∈ ( Evenfin ∪ Oddfin )))
32	30, 31	imbi12d 311	. . . . . 6 ⊢ (m = 0c → ((m ≠ ∅ → m ∈ ( Evenfin ∪ Oddfin )) ↔ (0c ≠ ∅ → 0c ∈ ( Evenfin ∪ Oddfin ))))
33		neeq1 2525	. . . . . . 7 ⊢ (m = k → (m ≠ ∅ ↔ k ≠ ∅))
34		eleq1 2413	. . . . . . 7 ⊢ (m = k → (m ∈ ( Evenfin ∪ Oddfin ) ↔ k ∈ ( Evenfin ∪ Oddfin )))
35	33, 34	imbi12d 311	. . . . . 6 ⊢ (m = k → ((m ≠ ∅ → m ∈ ( Evenfin ∪ Oddfin )) ↔ (k ≠ ∅ → k ∈ ( Evenfin ∪ Oddfin ))))
36		neeq1 2525	. . . . . . 7 ⊢ (m = (k +c 1c) → (m ≠ ∅ ↔ (k +c 1c) ≠ ∅))
37		eleq1 2413	. . . . . . 7 ⊢ (m = (k +c 1c) → (m ∈ ( Evenfin ∪ Oddfin ) ↔ (k +c 1c) ∈ ( Evenfin ∪ Oddfin )))
38	36, 37	imbi12d 311	. . . . . 6 ⊢ (m = (k +c 1c) → ((m ≠ ∅ → m ∈ ( Evenfin ∪ Oddfin )) ↔ ((k +c 1c) ≠ ∅ → (k +c 1c) ∈ ( Evenfin ∪ Oddfin ))))
39		neeq1 2525	. . . . . . 7 ⊢ (m = n → (m ≠ ∅ ↔ n ≠ ∅))
40		eleq1 2413	. . . . . . 7 ⊢ (m = n → (m ∈ ( Evenfin ∪ Oddfin ) ↔ n ∈ ( Evenfin ∪ Oddfin )))
41	39, 40	imbi12d 311	. . . . . 6 ⊢ (m = n → ((m ≠ ∅ → m ∈ ( Evenfin ∪ Oddfin )) ↔ (n ≠ ∅ → n ∈ ( Evenfin ∪ Oddfin ))))
42		ssun1 3427	. . . . . . . 8 ⊢ Evenfin ⊆ ( Evenfin ∪ Oddfin )
43		0ceven 4506	. . . . . . . 8 ⊢ 0c ∈ Evenfin
44	42, 43	sselii 3271	. . . . . . 7 ⊢ 0c ∈ ( Evenfin ∪ Oddfin )
45	44	a1i 10	. . . . . 6 ⊢ (0c ≠ ∅ → 0c ∈ ( Evenfin ∪ Oddfin ))
46		addcnnul 4454	. . . . . . . . . 10 ⊢ ((k +c 1c) ≠ ∅ → (k ≠ ∅ ∧ 1c ≠ ∅))
47	46	simpld 445	. . . . . . . . 9 ⊢ ((k +c 1c) ≠ ∅ → k ≠ ∅)
48		sucevenodd 4511	. . . . . . . . . . . 12 ⊢ ((k ∈ Evenfin ∧ (k +c 1c) ≠ ∅) → (k +c 1c) ∈ Oddfin )
49	48	expcom 424	. . . . . . . . . . 11 ⊢ ((k +c 1c) ≠ ∅ → (k ∈ Evenfin → (k +c 1c) ∈ Oddfin ))
50		sucoddeven 4512	. . . . . . . . . . . 12 ⊢ ((k ∈ Oddfin ∧ (k +c 1c) ≠ ∅) → (k +c 1c) ∈ Evenfin )
51	50	expcom 424	. . . . . . . . . . 11 ⊢ ((k +c 1c) ≠ ∅ → (k ∈ Oddfin → (k +c 1c) ∈ Evenfin ))
52	49, 51	orim12d 811	. . . . . . . . . 10 ⊢ ((k +c 1c) ≠ ∅ → ((k ∈ Evenfin ∨ k ∈ Oddfin ) → ((k +c 1c) ∈ Oddfin ∨ (k +c 1c) ∈ Evenfin )))
53		elun 3221	. . . . . . . . . 10 ⊢ (k ∈ ( Evenfin ∪ Oddfin ) ↔ (k ∈ Evenfin ∨ k ∈ Oddfin ))
54		elun 3221	. . . . . . . . . . 11 ⊢ ((k +c 1c) ∈ ( Evenfin ∪ Oddfin ) ↔ ((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 ))
56	54, 55	bitri 240	. . . . . . . . . 10 ⊢ ((k +c 1c) ∈ ( Evenfin ∪ Oddfin ) ↔ ((k +c 1c) ∈ Oddfin ∨ (k +c 1c) ∈ Evenfin ))
57	52, 53, 56	3imtr4g 261	. . . . . . . . 9 ⊢ ((k +c 1c) ≠ ∅ → (k ∈ ( Evenfin ∪ Oddfin ) → (k +c 1c) ∈ ( Evenfin ∪ Oddfin )))
58	47, 57	embantd 50	. . . . . . . 8 ⊢ ((k +c 1c) ≠ ∅ → ((k ≠ ∅ → k ∈ ( Evenfin ∪ Oddfin )) → (k +c 1c) ∈ ( Evenfin ∪ Oddfin )))
59	58	com12 27	. . . . . . 7 ⊢ ((k ≠ ∅ → k ∈ ( Evenfin ∪ Oddfin )) → ((k +c 1c) ≠ ∅ → (k +c 1c) ∈ ( Evenfin ∪ Oddfin )))
60	59	a1i 10	. . . . . 6 ⊢ (k ∈ Nn → ((k ≠ ∅ → k ∈ ( Evenfin ∪ Oddfin )) → ((k +c 1c) ≠ ∅ → (k +c 1c) ∈ ( Evenfin ∪ Oddfin ))))
61	29, 32, 35, 38, 41, 45, 60	finds 4412	. . . . 5 ⊢ (n ∈ Nn → (n ≠ ∅ → n ∈ ( Evenfin ∪ Oddfin )))
62	61	imp 418	. . . 4 ⊢ ((n ∈ Nn ∧ n ≠ ∅) → n ∈ ( Evenfin ∪ Oddfin ))
63	13, 62	sylbi 187	. . 3 ⊢ (n ∈ ( Nn ∖ {∅}) → n ∈ ( Evenfin ∪ Oddfin ))
64	63	ssriv 3278	. 2 ⊢ ( Nn ∖ {∅}) ⊆ ( Evenfin ∪ Oddfin )
65	12, 64	eqssi 3289	1 ⊢ ( Evenfin ∪ Oddfin ) = ( Nn ∖ {∅})

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 357   ∧ wa 358   = wceq 1642   ∈ wcel 1710  {cab 2339   ≠ wne 2517  Vcvv 2860   ∖ cdif 3207   ∪ cun 3208   ⊆ wss 3258  ∅c0 3551  {csn 3738  1_cc1c 4135   Nn cnnc 4374  0_cc0c 4375   +_c cplc 4376   Even_fin cevenfin 4437   Odd_fin coddfin 4438

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 4079  ax-xp 4080  ax-cnv 4081  ax-1c 4082  ax-sset 4083  ax-si 4084  ax-ins2 4085  ax-ins3 4086  ax-typlower 4087  ax-sn 4088

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 2479  df-ne 2519  df-ral 2620  df-rex 2621  df-v 2862  df-sbc 3048  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-symdif 3217  df-ss 3260  df-nul 3552  df-if 3664  df-pw 3725  df-sn 3742  df-pr 3743  df-uni 3893  df-int 3928  df-opk 4059  df-1c 4137  df-pw1 4138  df-uni1 4139  df-xpk 4186  df-cnvk 4187  df-ins2k 4188  df-ins3k 4189  df-imak 4190  df-cok 4191  df-p6 4192  df-sik 4193  df-ssetk 4194  df-imagek 4195  df-idk 4196  df-0c 4378  df-addc 4379  df-nnc 4380  df-evenfin 4445  df-oddfin 4446

This theorem is referenced by:  vinf  4556