Theorem evenodddisj 4517

Description: The even finite cardinals and the odd ones are disjoint. Theorem X.1.36 of [Rosser] p. 529. (Contributed by SF, 22-Jan-2015.)

Assertion

Ref	Expression
evenodddisj	⊢ ( Evenfin ∩ Oddfin ) = ∅

Proof of Theorem evenodddisj

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

Step	Hyp	Ref	Expression
1		dfevenfin2 4513	. . . 4 ⊢ Evenfin = {x ∣ ∃k ∈ Nn (x = (k +c k) ∧ (k +c k) ≠ ∅)}
2		dfoddfin2 4514	. . . 4 ⊢ Oddfin = {x ∣ ∃n ∈ Nn (x = ((n +c n) +c 1c) ∧ ((n +c n) +c 1c) ≠ ∅)}
3	1, 2	ineq12i 3456	. . 3 ⊢ ( Evenfin ∩ Oddfin ) = ({x ∣ ∃k ∈ Nn (x = (k +c k) ∧ (k +c k) ≠ ∅)} ∩ {x ∣ ∃n ∈ Nn (x = ((n +c n) +c 1c) ∧ ((n +c n) +c 1c) ≠ ∅)})
4		inab 3523	. . 3 ⊢ ({x ∣ ∃k ∈ Nn (x = (k +c k) ∧ (k +c k) ≠ ∅)} ∩ {x ∣ ∃n ∈ Nn (x = ((n +c n) +c 1c) ∧ ((n +c n) +c 1c) ≠ ∅)}) = {x ∣ (∃k ∈ Nn (x = (k +c k) ∧ (k +c k) ≠ ∅) ∧ ∃n ∈ Nn (x = ((n +c n) +c 1c) ∧ ((n +c n) +c 1c) ≠ ∅))}
5	3, 4	eqtri 2373	. 2 ⊢ ( Evenfin ∩ Oddfin ) = {x ∣ (∃k ∈ Nn (x = (k +c k) ∧ (k +c k) ≠ ∅) ∧ ∃n ∈ Nn (x = ((n +c n) +c 1c) ∧ ((n +c n) +c 1c) ≠ ∅))}
6		evenodddisjlem1 4516	. . . . . . . . 9 ⊢ {j ∣ ((j +c j) ≠ ∅ → ∀n ∈ Nn (((n +c n) +c 1c) ≠ ∅ → (j +c j) ≠ ((n +c n) +c 1c)))} ∈ V
7		addceq12 4386	. . . . . . . . . . . . 13 ⊢ ((j = 0c ∧ j = 0c) → (j +c j) = (0c +c 0c))
8	7	anidms 626	. . . . . . . . . . . 12 ⊢ (j = 0c → (j +c j) = (0c +c 0c))
9		addcid2 4408	. . . . . . . . . . . 12 ⊢ (0c +c 0c) = 0c
10	8, 9	syl6eq 2401	. . . . . . . . . . 11 ⊢ (j = 0c → (j +c j) = 0c)
11	10	neeq1d 2530	. . . . . . . . . 10 ⊢ (j = 0c → ((j +c j) ≠ ∅ ↔ 0c ≠ ∅))
12	10	neeq1d 2530	. . . . . . . . . . . 12 ⊢ (j = 0c → ((j +c j) ≠ ((n +c n) +c 1c) ↔ 0c ≠ ((n +c n) +c 1c)))
13	12	imbi2d 307	. . . . . . . . . . 11 ⊢ (j = 0c → ((((n +c n) +c 1c) ≠ ∅ → (j +c j) ≠ ((n +c n) +c 1c)) ↔ (((n +c n) +c 1c) ≠ ∅ → 0c ≠ ((n +c n) +c 1c))))
14	13	ralbidv 2635	. . . . . . . . . 10 ⊢ (j = 0c → (∀n ∈ Nn (((n +c n) +c 1c) ≠ ∅ → (j +c j) ≠ ((n +c n) +c 1c)) ↔ ∀n ∈ Nn (((n +c n) +c 1c) ≠ ∅ → 0c ≠ ((n +c n) +c 1c))))
15	11, 14	imbi12d 311	. . . . . . . . 9 ⊢ (j = 0c → (((j +c j) ≠ ∅ → ∀n ∈ Nn (((n +c n) +c 1c) ≠ ∅ → (j +c j) ≠ ((n +c n) +c 1c))) ↔ (0c ≠ ∅ → ∀n ∈ Nn (((n +c n) +c 1c) ≠ ∅ → 0c ≠ ((n +c n) +c 1c)))))
16		addceq12 4386	. . . . . . . . . . . 12 ⊢ ((j = m ∧ j = m) → (j +c j) = (m +c m))
17	16	anidms 626	. . . . . . . . . . 11 ⊢ (j = m → (j +c j) = (m +c m))
18	17	neeq1d 2530	. . . . . . . . . 10 ⊢ (j = m → ((j +c j) ≠ ∅ ↔ (m +c m) ≠ ∅))
19	17	neeq1d 2530	. . . . . . . . . . . . 13 ⊢ (j = m → ((j +c j) ≠ ((n +c n) +c 1c) ↔ (m +c m) ≠ ((n +c n) +c 1c)))
20	19	imbi2d 307	. . . . . . . . . . . 12 ⊢ (j = m → ((((n +c n) +c 1c) ≠ ∅ → (j +c j) ≠ ((n +c n) +c 1c)) ↔ (((n +c n) +c 1c) ≠ ∅ → (m +c m) ≠ ((n +c n) +c 1c))))
21	20	ralbidv 2635	. . . . . . . . . . 11 ⊢ (j = m → (∀n ∈ Nn (((n +c n) +c 1c) ≠ ∅ → (j +c j) ≠ ((n +c n) +c 1c)) ↔ ∀n ∈ Nn (((n +c n) +c 1c) ≠ ∅ → (m +c m) ≠ ((n +c n) +c 1c))))
22		addceq12 4386	. . . . . . . . . . . . . . . 16 ⊢ ((n = p ∧ n = p) → (n +c n) = (p +c p))
23	22	anidms 626	. . . . . . . . . . . . . . 15 ⊢ (n = p → (n +c n) = (p +c p))
24	23	addceq1d 4390	. . . . . . . . . . . . . 14 ⊢ (n = p → ((n +c n) +c 1c) = ((p +c p) +c 1c))
25	24	neeq1d 2530	. . . . . . . . . . . . 13 ⊢ (n = p → (((n +c n) +c 1c) ≠ ∅ ↔ ((p +c p) +c 1c) ≠ ∅))
26	24	neeq2d 2531	. . . . . . . . . . . . 13 ⊢ (n = p → ((m +c m) ≠ ((n +c n) +c 1c) ↔ (m +c m) ≠ ((p +c p) +c 1c)))
27	25, 26	imbi12d 311	. . . . . . . . . . . 12 ⊢ (n = p → ((((n +c n) +c 1c) ≠ ∅ → (m +c m) ≠ ((n +c n) +c 1c)) ↔ (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))))
28	27	cbvralv 2836	. . . . . . . . . . 11 ⊢ (∀n ∈ Nn (((n +c n) +c 1c) ≠ ∅ → (m +c m) ≠ ((n +c n) +c 1c)) ↔ ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c)))
29	21, 28	syl6bb 252	. . . . . . . . . 10 ⊢ (j = m → (∀n ∈ Nn (((n +c n) +c 1c) ≠ ∅ → (j +c j) ≠ ((n +c n) +c 1c)) ↔ ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))))
30	18, 29	imbi12d 311	. . . . . . . . 9 ⊢ (j = m → (((j +c j) ≠ ∅ → ∀n ∈ Nn (((n +c n) +c 1c) ≠ ∅ → (j +c j) ≠ ((n +c n) +c 1c))) ↔ ((m +c m) ≠ ∅ → ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c)))))
31		addceq12 4386	. . . . . . . . . . . . 13 ⊢ ((j = (m +c 1c) ∧ j = (m +c 1c)) → (j +c j) = ((m +c 1c) +c (m +c 1c)))
32	31	anidms 626	. . . . . . . . . . . 12 ⊢ (j = (m +c 1c) → (j +c j) = ((m +c 1c) +c (m +c 1c)))
33		addcass 4416	. . . . . . . . . . . . 13 ⊢ (((m +c 1c) +c m) +c 1c) = ((m +c 1c) +c (m +c 1c))
34		addc32 4417	. . . . . . . . . . . . . 14 ⊢ ((m +c 1c) +c m) = ((m +c m) +c 1c)
35	34	addceq1i 4387	. . . . . . . . . . . . 13 ⊢ (((m +c 1c) +c m) +c 1c) = (((m +c m) +c 1c) +c 1c)
36	33, 35	eqtr3i 2375	. . . . . . . . . . . 12 ⊢ ((m +c 1c) +c (m +c 1c)) = (((m +c m) +c 1c) +c 1c)
37	32, 36	syl6eq 2401	. . . . . . . . . . 11 ⊢ (j = (m +c 1c) → (j +c j) = (((m +c m) +c 1c) +c 1c))
38	37	neeq1d 2530	. . . . . . . . . 10 ⊢ (j = (m +c 1c) → ((j +c j) ≠ ∅ ↔ (((m +c m) +c 1c) +c 1c) ≠ ∅))
39	37	neeq1d 2530	. . . . . . . . . . . 12 ⊢ (j = (m +c 1c) → ((j +c j) ≠ ((n +c n) +c 1c) ↔ (((m +c m) +c 1c) +c 1c) ≠ ((n +c n) +c 1c)))
40	39	imbi2d 307	. . . . . . . . . . 11 ⊢ (j = (m +c 1c) → ((((n +c n) +c 1c) ≠ ∅ → (j +c j) ≠ ((n +c n) +c 1c)) ↔ (((n +c n) +c 1c) ≠ ∅ → (((m +c m) +c 1c) +c 1c) ≠ ((n +c n) +c 1c))))
41	40	ralbidv 2635	. . . . . . . . . 10 ⊢ (j = (m +c 1c) → (∀n ∈ Nn (((n +c n) +c 1c) ≠ ∅ → (j +c j) ≠ ((n +c n) +c 1c)) ↔ ∀n ∈ Nn (((n +c n) +c 1c) ≠ ∅ → (((m +c m) +c 1c) +c 1c) ≠ ((n +c n) +c 1c))))
42	38, 41	imbi12d 311	. . . . . . . . 9 ⊢ (j = (m +c 1c) → (((j +c j) ≠ ∅ → ∀n ∈ Nn (((n +c n) +c 1c) ≠ ∅ → (j +c j) ≠ ((n +c n) +c 1c))) ↔ ((((m +c m) +c 1c) +c 1c) ≠ ∅ → ∀n ∈ Nn (((n +c n) +c 1c) ≠ ∅ → (((m +c m) +c 1c) +c 1c) ≠ ((n +c n) +c 1c)))))
43		addceq12 4386	. . . . . . . . . . . 12 ⊢ ((j = k ∧ j = k) → (j +c j) = (k +c k))
44	43	anidms 626	. . . . . . . . . . 11 ⊢ (j = k → (j +c j) = (k +c k))
45	44	neeq1d 2530	. . . . . . . . . 10 ⊢ (j = k → ((j +c j) ≠ ∅ ↔ (k +c k) ≠ ∅))
46	44	neeq1d 2530	. . . . . . . . . . . 12 ⊢ (j = k → ((j +c j) ≠ ((n +c n) +c 1c) ↔ (k +c k) ≠ ((n +c n) +c 1c)))
47	46	imbi2d 307	. . . . . . . . . . 11 ⊢ (j = k → ((((n +c n) +c 1c) ≠ ∅ → (j +c j) ≠ ((n +c n) +c 1c)) ↔ (((n +c n) +c 1c) ≠ ∅ → (k +c k) ≠ ((n +c n) +c 1c))))
48	47	ralbidv 2635	. . . . . . . . . 10 ⊢ (j = k → (∀n ∈ Nn (((n +c n) +c 1c) ≠ ∅ → (j +c j) ≠ ((n +c n) +c 1c)) ↔ ∀n ∈ Nn (((n +c n) +c 1c) ≠ ∅ → (k +c k) ≠ ((n +c n) +c 1c))))
49	45, 48	imbi12d 311	. . . . . . . . 9 ⊢ (j = k → (((j +c j) ≠ ∅ → ∀n ∈ Nn (((n +c n) +c 1c) ≠ ∅ → (j +c j) ≠ ((n +c n) +c 1c))) ↔ ((k +c k) ≠ ∅ → ∀n ∈ Nn (((n +c n) +c 1c) ≠ ∅ → (k +c k) ≠ ((n +c n) +c 1c)))))
50		0cnsuc 4402	. . . . . . . . . . . . 13 ⊢ ((n +c n) +c 1c) ≠ 0c
51	50	necomi 2599	. . . . . . . . . . . 12 ⊢ 0c ≠ ((n +c n) +c 1c)
52	51	a1i 10	. . . . . . . . . . 11 ⊢ (((n +c n) +c 1c) ≠ ∅ → 0c ≠ ((n +c n) +c 1c))
53	52	rgenw 2682	. . . . . . . . . 10 ⊢ ∀n ∈ Nn (((n +c n) +c 1c) ≠ ∅ → 0c ≠ ((n +c n) +c 1c))
54	53	a1i 10	. . . . . . . . 9 ⊢ (0c ≠ ∅ → ∀n ∈ Nn (((n +c n) +c 1c) ≠ ∅ → 0c ≠ ((n +c n) +c 1c)))
55		addcass 4416	. . . . . . . . . . . . . . 15 ⊢ (((m +c m) +c 1c) +c 1c) = ((m +c m) +c (1c +c 1c))
56	55	neeq1i 2527	. . . . . . . . . . . . . 14 ⊢ ((((m +c m) +c 1c) +c 1c) ≠ ∅ ↔ ((m +c m) +c (1c +c 1c)) ≠ ∅)
57		addcnnul 4454	. . . . . . . . . . . . . . 15 ⊢ (((m +c m) +c (1c +c 1c)) ≠ ∅ → ((m +c m) ≠ ∅ ∧ (1c +c 1c) ≠ ∅))
58	57	simpld 445	. . . . . . . . . . . . . 14 ⊢ (((m +c m) +c (1c +c 1c)) ≠ ∅ → (m +c m) ≠ ∅)
59	56, 58	sylbi 187	. . . . . . . . . . . . 13 ⊢ ((((m +c m) +c 1c) +c 1c) ≠ ∅ → (m +c m) ≠ ∅)
60	59	adantl 452	. . . . . . . . . . . 12 ⊢ ((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) → (m +c m) ≠ ∅)
61		simprl 732	. . . . . . . . . . . . . . . . . 18 ⊢ ((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))) ∧ (n ∈ Nn ∧ ((n +c n) +c 1c) ≠ ∅)) → n ∈ Nn )
62		nnc0suc 4413	. . . . . . . . . . . . . . . . . 18 ⊢ (n ∈ Nn ↔ (n = 0c ∨ ∃q ∈ Nn n = (q +c 1c)))
63	61, 62	sylib 188	. . . . . . . . . . . . . . . . 17 ⊢ ((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))) ∧ (n ∈ Nn ∧ ((n +c n) +c 1c) ≠ ∅)) → (n = 0c ∨ ∃q ∈ Nn n = (q +c 1c)))
64		0cnsuc 4402	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((m +c m) +c 1c) ≠ 0c
65		addceq12 4386	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((n = 0c ∧ n = 0c) → (n +c n) = (0c +c 0c))
66	65	anidms 626	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (n = 0c → (n +c n) = (0c +c 0c))
67	66, 9	syl6eq 2401	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (n = 0c → (n +c n) = 0c)
68	67	neeq2d 2531	. . . . . . . . . . . . . . . . . . . 20 ⊢ (n = 0c → (((m +c m) +c 1c) ≠ (n +c n) ↔ ((m +c m) +c 1c) ≠ 0c))
69	64, 68	mpbiri 224	. . . . . . . . . . . . . . . . . . 19 ⊢ (n = 0c → ((m +c m) +c 1c) ≠ (n +c n))
70	69	a1i 10	. . . . . . . . . . . . . . . . . 18 ⊢ ((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))) ∧ (n ∈ Nn ∧ ((n +c n) +c 1c) ≠ ∅)) → (n = 0c → ((m +c m) +c 1c) ≠ (n +c n)))
71		simpr 447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ∅ ∧ q ∈ Nn ) → q ∈ Nn )
72	71	adantl 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ∅ ∧ q ∈ Nn )) → q ∈ Nn )
73		addceq12 4386	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((p = q ∧ p = q) → (p +c p) = (q +c q))
74	73	anidms 626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (p = q → (p +c p) = (q +c q))
75	74	addceq1d 4390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (p = q → ((p +c p) +c 1c) = ((q +c q) +c 1c))
76	75	neeq1d 2530	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (p = q → (((p +c p) +c 1c) ≠ ∅ ↔ ((q +c q) +c 1c) ≠ ∅))
77	75	neeq2d 2531	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (p = q → ((m +c m) ≠ ((p +c p) +c 1c) ↔ (m +c m) ≠ ((q +c q) +c 1c)))
78	76, 77	imbi12d 311	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (p = q → ((((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c)) ↔ (((q +c q) +c 1c) ≠ ∅ → (m +c m) ≠ ((q +c q) +c 1c))))
79	78	rspcv 2952	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (q ∈ Nn → (∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c)) → (((q +c q) +c 1c) ≠ ∅ → (m +c m) ≠ ((q +c q) +c 1c))))
80	72, 79	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ∅ ∧ q ∈ Nn )) → (∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c)) → (((q +c q) +c 1c) ≠ ∅ → (m +c m) ≠ ((q +c q) +c 1c))))
81		addc4 4418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((q +c 1c) +c (q +c 1c)) = ((q +c q) +c (1c +c 1c))
82	81	addceq1i 4387	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((q +c 1c) +c (q +c 1c)) +c 1c) = (((q +c q) +c (1c +c 1c)) +c 1c)
83		addc32 4417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((q +c q) +c (1c +c 1c)) +c 1c) = (((q +c q) +c 1c) +c (1c +c 1c))
84	82, 83	eqtri 2373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((q +c 1c) +c (q +c 1c)) +c 1c) = (((q +c q) +c 1c) +c (1c +c 1c))
85	84	neeq1i 2527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ∅ ↔ (((q +c q) +c 1c) +c (1c +c 1c)) ≠ ∅)
86		addcnnul 4454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((q +c q) +c 1c) +c (1c +c 1c)) ≠ ∅ → (((q +c q) +c 1c) ≠ ∅ ∧ (1c +c 1c) ≠ ∅))
87	86	simpld 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((q +c q) +c 1c) +c (1c +c 1c)) ≠ ∅ → ((q +c q) +c 1c) ≠ ∅)
88	85, 87	sylbi 187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ∅ → ((q +c q) +c 1c) ≠ ∅)
89	88	adantr 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ∅ ∧ q ∈ Nn ) → ((q +c q) +c 1c) ≠ ∅)
90	89	adantl 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ∅ ∧ q ∈ Nn )) → ((q +c q) +c 1c) ≠ ∅)
91		addc32 4417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((q +c q) +c 1c) = ((q +c 1c) +c q)
92	91	addceq1i 4387	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((q +c q) +c 1c) +c 1c) = (((q +c 1c) +c q) +c 1c)
93		addcass 4416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((q +c 1c) +c q) +c 1c) = ((q +c 1c) +c (q +c 1c))
94	92, 93	eqtri 2373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((q +c q) +c 1c) +c 1c) = ((q +c 1c) +c (q +c 1c))
95	94	eqeq2i 2363	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((m +c m) +c 1c) = (((q +c q) +c 1c) +c 1c) ↔ ((m +c m) +c 1c) = ((q +c 1c) +c (q +c 1c)))
96		simplll 734	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ∅ ∧ q ∈ Nn )) ∧ ((m +c m) +c 1c) = (((q +c q) +c 1c) +c 1c)) → m ∈ Nn )
97		nncaddccl 4420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((m ∈ Nn ∧ m ∈ Nn ) → (m +c m) ∈ Nn )
98	97	anidms 626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (m ∈ Nn → (m +c m) ∈ Nn )
99	96, 98	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ∅ ∧ q ∈ Nn )) ∧ ((m +c m) +c 1c) = (((q +c q) +c 1c) +c 1c)) → (m +c m) ∈ Nn )
100		simplrr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ∅ ∧ q ∈ Nn )) ∧ ((m +c m) +c 1c) = (((q +c q) +c 1c) +c 1c)) → q ∈ Nn )
101		nncaddccl 4420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((q ∈ Nn ∧ q ∈ Nn ) → (q +c q) ∈ Nn )
102	101	anidms 626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (q ∈ Nn → (q +c q) ∈ Nn )
103		peano2 4404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((q +c q) ∈ Nn → ((q +c q) +c 1c) ∈ Nn )
104	100, 102, 103	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ∅ ∧ q ∈ Nn )) ∧ ((m +c m) +c 1c) = (((q +c q) +c 1c) +c 1c)) → ((q +c q) +c 1c) ∈ Nn )
105		simpr 447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ∅ ∧ q ∈ Nn )) ∧ ((m +c m) +c 1c) = (((q +c q) +c 1c) +c 1c)) → ((m +c m) +c 1c) = (((q +c q) +c 1c) +c 1c))
106		simpllr 735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ∅ ∧ q ∈ Nn )) ∧ ((m +c m) +c 1c) = (((q +c q) +c 1c) +c 1c)) → (((m +c m) +c 1c) +c 1c) ≠ ∅)
107		addcnnul 4454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((m +c m) +c 1c) +c 1c) ≠ ∅ → (((m +c m) +c 1c) ≠ ∅ ∧ 1c ≠ ∅))
108	107	simpld 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((m +c m) +c 1c) +c 1c) ≠ ∅ → ((m +c m) +c 1c) ≠ ∅)
109	106, 108	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ∅ ∧ q ∈ Nn )) ∧ ((m +c m) +c 1c) = (((q +c q) +c 1c) +c 1c)) → ((m +c m) +c 1c) ≠ ∅)
110		prepeano4 4452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((m +c m) ∈ Nn ∧ ((q +c q) +c 1c) ∈ Nn ) ∧ (((m +c m) +c 1c) = (((q +c q) +c 1c) +c 1c) ∧ ((m +c m) +c 1c) ≠ ∅)) → (m +c m) = ((q +c q) +c 1c))
111	99, 104, 105, 109, 110	syl22anc 1183	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ∅ ∧ q ∈ Nn )) ∧ ((m +c m) +c 1c) = (((q +c q) +c 1c) +c 1c)) → (m +c m) = ((q +c q) +c 1c))
112	111	ex 423	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ∅ ∧ q ∈ Nn )) → (((m +c m) +c 1c) = (((q +c q) +c 1c) +c 1c) → (m +c m) = ((q +c q) +c 1c)))
113	95, 112	syl5bir 209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ∅ ∧ q ∈ Nn )) → (((m +c m) +c 1c) = ((q +c 1c) +c (q +c 1c)) → (m +c m) = ((q +c q) +c 1c)))
114	113	necon3d 2555	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ∅ ∧ q ∈ Nn )) → ((m +c m) ≠ ((q +c q) +c 1c) → ((m +c m) +c 1c) ≠ ((q +c 1c) +c (q +c 1c))))
115	90, 114	embantd 50	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ∅ ∧ q ∈ Nn )) → ((((q +c q) +c 1c) ≠ ∅ → (m +c m) ≠ ((q +c q) +c 1c)) → ((m +c m) +c 1c) ≠ ((q +c 1c) +c (q +c 1c))))
116	80, 115	syld 40	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ∅ ∧ q ∈ Nn )) → (∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c)) → ((m +c m) +c 1c) ≠ ((q +c 1c) +c (q +c 1c))))
117	116	expr 598	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ (((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ∅) → (q ∈ Nn → (∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c)) → ((m +c m) +c 1c) ≠ ((q +c 1c) +c (q +c 1c)))))
118	117	com23 72	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ (((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ∅) → (∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c)) → (q ∈ Nn → ((m +c m) +c 1c) ≠ ((q +c 1c) +c (q +c 1c)))))
119	118	ex 423	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) → ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ∅ → (∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c)) → (q ∈ Nn → ((m +c m) +c 1c) ≠ ((q +c 1c) +c (q +c 1c))))))
120	119	com23 72	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) → (∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c)) → ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ∅ → (q ∈ Nn → ((m +c m) +c 1c) ≠ ((q +c 1c) +c (q +c 1c))))))
121	120	imp31 421	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))) ∧ (((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ∅) → (q ∈ Nn → ((m +c m) +c 1c) ≠ ((q +c 1c) +c (q +c 1c))))
122	121	com12 27	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (q ∈ Nn → ((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))) ∧ (((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ∅) → ((m +c m) +c 1c) ≠ ((q +c 1c) +c (q +c 1c))))
123		addceq12 4386	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((n = (q +c 1c) ∧ n = (q +c 1c)) → (n +c n) = ((q +c 1c) +c (q +c 1c)))
124	123	anidms 626	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (n = (q +c 1c) → (n +c n) = ((q +c 1c) +c (q +c 1c)))
125	124	addceq1d 4390	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (n = (q +c 1c) → ((n +c n) +c 1c) = (((q +c 1c) +c (q +c 1c)) +c 1c))
126	125	neeq1d 2530	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (n = (q +c 1c) → (((n +c n) +c 1c) ≠ ∅ ↔ (((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ∅))
127	126	anbi2d 684	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (n = (q +c 1c) → ((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))) ∧ ((n +c n) +c 1c) ≠ ∅) ↔ (((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))) ∧ (((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ∅)))
128	124	neeq2d 2531	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (n = (q +c 1c) → (((m +c m) +c 1c) ≠ (n +c n) ↔ ((m +c m) +c 1c) ≠ ((q +c 1c) +c (q +c 1c))))
129	127, 128	imbi12d 311	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (n = (q +c 1c) → (((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))) ∧ ((n +c n) +c 1c) ≠ ∅) → ((m +c m) +c 1c) ≠ (n +c n)) ↔ ((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))) ∧ (((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ∅) → ((m +c m) +c 1c) ≠ ((q +c 1c) +c (q +c 1c)))))
130	122, 129	syl5ibrcom 213	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (q ∈ Nn → (n = (q +c 1c) → ((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))) ∧ ((n +c n) +c 1c) ≠ ∅) → ((m +c m) +c 1c) ≠ (n +c n))))
131	130	rexlimiv 2733	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃q ∈ Nn n = (q +c 1c) → ((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))) ∧ ((n +c n) +c 1c) ≠ ∅) → ((m +c m) +c 1c) ≠ (n +c n)))
132	131	com12 27	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))) ∧ ((n +c n) +c 1c) ≠ ∅) → (∃q ∈ Nn n = (q +c 1c) → ((m +c m) +c 1c) ≠ (n +c n)))
133	132	adantrl 696	. . . . . . . . . . . . . . . . . 18 ⊢ ((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))) ∧ (n ∈ Nn ∧ ((n +c n) +c 1c) ≠ ∅)) → (∃q ∈ Nn n = (q +c 1c) → ((m +c m) +c 1c) ≠ (n +c n)))
134	70, 133	jaod 369	. . . . . . . . . . . . . . . . 17 ⊢ ((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))) ∧ (n ∈ Nn ∧ ((n +c n) +c 1c) ≠ ∅)) → ((n = 0c ∨ ∃q ∈ Nn n = (q +c 1c)) → ((m +c m) +c 1c) ≠ (n +c n)))
135	63, 134	mpd 14	. . . . . . . . . . . . . . . 16 ⊢ ((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))) ∧ (n ∈ Nn ∧ ((n +c n) +c 1c) ≠ ∅)) → ((m +c m) +c 1c) ≠ (n +c n))
136		simplll 734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))) ∧ (n ∈ Nn ∧ ((n +c n) +c 1c) ≠ ∅)) → m ∈ Nn )
137	136	adantr 451	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))) ∧ (n ∈ Nn ∧ ((n +c n) +c 1c) ≠ ∅)) ∧ (((m +c m) +c 1c) +c 1c) = ((n +c n) +c 1c)) → m ∈ Nn )
138		peano2 4404	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((m +c m) ∈ Nn → ((m +c m) +c 1c) ∈ Nn )
139	137, 98, 138	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))) ∧ (n ∈ Nn ∧ ((n +c n) +c 1c) ≠ ∅)) ∧ (((m +c m) +c 1c) +c 1c) = ((n +c n) +c 1c)) → ((m +c m) +c 1c) ∈ Nn )
140		simplrl 736	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))) ∧ (n ∈ Nn ∧ ((n +c n) +c 1c) ≠ ∅)) ∧ (((m +c m) +c 1c) +c 1c) = ((n +c n) +c 1c)) → n ∈ Nn )
141		nncaddccl 4420	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((n ∈ Nn ∧ n ∈ Nn ) → (n +c n) ∈ Nn )
142	141	anidms 626	. . . . . . . . . . . . . . . . . . . 20 ⊢ (n ∈ Nn → (n +c n) ∈ Nn )
143	140, 142	syl 15	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))) ∧ (n ∈ Nn ∧ ((n +c n) +c 1c) ≠ ∅)) ∧ (((m +c m) +c 1c) +c 1c) = ((n +c n) +c 1c)) → (n +c n) ∈ Nn )
144		simpr 447	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))) ∧ (n ∈ Nn ∧ ((n +c n) +c 1c) ≠ ∅)) ∧ (((m +c m) +c 1c) +c 1c) = ((n +c n) +c 1c)) → (((m +c m) +c 1c) +c 1c) = ((n +c n) +c 1c))
145		simpllr 735	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))) ∧ (n ∈ Nn ∧ ((n +c n) +c 1c) ≠ ∅)) → (((m +c m) +c 1c) +c 1c) ≠ ∅)
146	145	adantr 451	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))) ∧ (n ∈ Nn ∧ ((n +c n) +c 1c) ≠ ∅)) ∧ (((m +c m) +c 1c) +c 1c) = ((n +c n) +c 1c)) → (((m +c m) +c 1c) +c 1c) ≠ ∅)
147		prepeano4 4452	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((m +c m) +c 1c) ∈ Nn ∧ (n +c n) ∈ Nn ) ∧ ((((m +c m) +c 1c) +c 1c) = ((n +c n) +c 1c) ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅)) → ((m +c m) +c 1c) = (n +c n))
148	139, 143, 144, 146, 147	syl22anc 1183	. . . . . . . . . . . . . . . . . 18 ⊢ (((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))) ∧ (n ∈ Nn ∧ ((n +c n) +c 1c) ≠ ∅)) ∧ (((m +c m) +c 1c) +c 1c) = ((n +c n) +c 1c)) → ((m +c m) +c 1c) = (n +c n))
149	148	ex 423	. . . . . . . . . . . . . . . . 17 ⊢ ((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))) ∧ (n ∈ Nn ∧ ((n +c n) +c 1c) ≠ ∅)) → ((((m +c m) +c 1c) +c 1c) = ((n +c n) +c 1c) → ((m +c m) +c 1c) = (n +c n)))
150	149	necon3d 2555	. . . . . . . . . . . . . . . 16 ⊢ ((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))) ∧ (n ∈ Nn ∧ ((n +c n) +c 1c) ≠ ∅)) → (((m +c m) +c 1c) ≠ (n +c n) → (((m +c m) +c 1c) +c 1c) ≠ ((n +c n) +c 1c)))
151	135, 150	mpd 14	. . . . . . . . . . . . . . 15 ⊢ ((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))) ∧ (n ∈ Nn ∧ ((n +c n) +c 1c) ≠ ∅)) → (((m +c m) +c 1c) +c 1c) ≠ ((n +c n) +c 1c))
152	151	expr 598	. . . . . . . . . . . . . 14 ⊢ ((((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))) ∧ n ∈ Nn ) → (((n +c n) +c 1c) ≠ ∅ → (((m +c m) +c 1c) +c 1c) ≠ ((n +c n) +c 1c)))
153	152	ralrimiva 2698	. . . . . . . . . . . . 13 ⊢ (((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) ∧ ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))) → ∀n ∈ Nn (((n +c n) +c 1c) ≠ ∅ → (((m +c m) +c 1c) +c 1c) ≠ ((n +c n) +c 1c)))
154	153	ex 423	. . . . . . . . . . . 12 ⊢ ((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) → (∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c)) → ∀n ∈ Nn (((n +c n) +c 1c) ≠ ∅ → (((m +c m) +c 1c) +c 1c) ≠ ((n +c n) +c 1c))))
155	60, 154	embantd 50	. . . . . . . . . . 11 ⊢ ((m ∈ Nn ∧ (((m +c m) +c 1c) +c 1c) ≠ ∅) → (((m +c m) ≠ ∅ → ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))) → ∀n ∈ Nn (((n +c n) +c 1c) ≠ ∅ → (((m +c m) +c 1c) +c 1c) ≠ ((n +c n) +c 1c))))
156	155	ex 423	. . . . . . . . . 10 ⊢ (m ∈ Nn → ((((m +c m) +c 1c) +c 1c) ≠ ∅ → (((m +c m) ≠ ∅ → ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))) → ∀n ∈ Nn (((n +c n) +c 1c) ≠ ∅ → (((m +c m) +c 1c) +c 1c) ≠ ((n +c n) +c 1c)))))
157	156	com23 72	. . . . . . . . 9 ⊢ (m ∈ Nn → (((m +c m) ≠ ∅ → ∀p ∈ Nn (((p +c p) +c 1c) ≠ ∅ → (m +c m) ≠ ((p +c p) +c 1c))) → ((((m +c m) +c 1c) +c 1c) ≠ ∅ → ∀n ∈ Nn (((n +c n) +c 1c) ≠ ∅ → (((m +c m) +c 1c) +c 1c) ≠ ((n +c n) +c 1c)))))
158	6, 15, 30, 42, 49, 54, 157	finds 4412	. . . . . . . 8 ⊢ (k ∈ Nn → ((k +c k) ≠ ∅ → ∀n ∈ Nn (((n +c n) +c 1c) ≠ ∅ → (k +c k) ≠ ((n +c n) +c 1c))))
159		df-ne 2519	. . . . . . . . . . . . 13 ⊢ ((k +c k) ≠ ((n +c n) +c 1c) ↔ ¬ (k +c k) = ((n +c n) +c 1c))
160	159	imbi2i 303	. . . . . . . . . . . 12 ⊢ ((((n +c n) +c 1c) ≠ ∅ → (k +c k) ≠ ((n +c n) +c 1c)) ↔ (((n +c n) +c 1c) ≠ ∅ → ¬ (k +c k) = ((n +c n) +c 1c)))
161		con2b 324	. . . . . . . . . . . 12 ⊢ ((((n +c n) +c 1c) ≠ ∅ → ¬ (k +c k) = ((n +c n) +c 1c)) ↔ ((k +c k) = ((n +c n) +c 1c) → ¬ ((n +c n) +c 1c) ≠ ∅))
162	160, 161	bitri 240	. . . . . . . . . . 11 ⊢ ((((n +c n) +c 1c) ≠ ∅ → (k +c k) ≠ ((n +c n) +c 1c)) ↔ ((k +c k) = ((n +c n) +c 1c) → ¬ ((n +c n) +c 1c) ≠ ∅))
163		imnan 411	. . . . . . . . . . 11 ⊢ (((k +c k) = ((n +c n) +c 1c) → ¬ ((n +c n) +c 1c) ≠ ∅) ↔ ¬ ((k +c k) = ((n +c n) +c 1c) ∧ ((n +c n) +c 1c) ≠ ∅))
164	162, 163	bitri 240	. . . . . . . . . 10 ⊢ ((((n +c n) +c 1c) ≠ ∅ → (k +c k) ≠ ((n +c n) +c 1c)) ↔ ¬ ((k +c k) = ((n +c n) +c 1c) ∧ ((n +c n) +c 1c) ≠ ∅))
165	164	ralbii 2639	. . . . . . . . 9 ⊢ (∀n ∈ Nn (((n +c n) +c 1c) ≠ ∅ → (k +c k) ≠ ((n +c n) +c 1c)) ↔ ∀n ∈ Nn ¬ ((k +c k) = ((n +c n) +c 1c) ∧ ((n +c n) +c 1c) ≠ ∅))
166		ralnex 2625	. . . . . . . . 9 ⊢ (∀n ∈ Nn ¬ ((k +c k) = ((n +c n) +c 1c) ∧ ((n +c n) +c 1c) ≠ ∅) ↔ ¬ ∃n ∈ Nn ((k +c k) = ((n +c n) +c 1c) ∧ ((n +c n) +c 1c) ≠ ∅))
167	165, 166	bitri 240	. . . . . . . 8 ⊢ (∀n ∈ Nn (((n +c n) +c 1c) ≠ ∅ → (k +c k) ≠ ((n +c n) +c 1c)) ↔ ¬ ∃n ∈ Nn ((k +c k) = ((n +c n) +c 1c) ∧ ((n +c n) +c 1c) ≠ ∅))
168	158, 167	syl6ib 217	. . . . . . 7 ⊢ (k ∈ Nn → ((k +c k) ≠ ∅ → ¬ ∃n ∈ Nn ((k +c k) = ((n +c n) +c 1c) ∧ ((n +c n) +c 1c) ≠ ∅)))
169		eqeq1 2359	. . . . . . . . . . 11 ⊢ (x = (k +c k) → (x = ((n +c n) +c 1c) ↔ (k +c k) = ((n +c n) +c 1c)))
170	169	anbi1d 685	. . . . . . . . . 10 ⊢ (x = (k +c k) → ((x = ((n +c n) +c 1c) ∧ ((n +c n) +c 1c) ≠ ∅) ↔ ((k +c k) = ((n +c n) +c 1c) ∧ ((n +c n) +c 1c) ≠ ∅)))
171	170	rexbidv 2636	. . . . . . . . 9 ⊢ (x = (k +c k) → (∃n ∈ Nn (x = ((n +c n) +c 1c) ∧ ((n +c n) +c 1c) ≠ ∅) ↔ ∃n ∈ Nn ((k +c k) = ((n +c n) +c 1c) ∧ ((n +c n) +c 1c) ≠ ∅)))
172	171	notbid 285	. . . . . . . 8 ⊢ (x = (k +c k) → (¬ ∃n ∈ Nn (x = ((n +c n) +c 1c) ∧ ((n +c n) +c 1c) ≠ ∅) ↔ ¬ ∃n ∈ Nn ((k +c k) = ((n +c n) +c 1c) ∧ ((n +c n) +c 1c) ≠ ∅)))
173	172	imbi2d 307	. . . . . . 7 ⊢ (x = (k +c k) → (((k +c k) ≠ ∅ → ¬ ∃n ∈ Nn (x = ((n +c n) +c 1c) ∧ ((n +c n) +c 1c) ≠ ∅)) ↔ ((k +c k) ≠ ∅ → ¬ ∃n ∈ Nn ((k +c k) = ((n +c n) +c 1c) ∧ ((n +c n) +c 1c) ≠ ∅))))
174	168, 173	syl5ibrcom 213	. . . . . 6 ⊢ (k ∈ Nn → (x = (k +c k) → ((k +c k) ≠ ∅ → ¬ ∃n ∈ Nn (x = ((n +c n) +c 1c) ∧ ((n +c n) +c 1c) ≠ ∅))))
175	174	imp3a 420	. . . . 5 ⊢ (k ∈ Nn → ((x = (k +c k) ∧ (k +c k) ≠ ∅) → ¬ ∃n ∈ Nn (x = ((n +c n) +c 1c) ∧ ((n +c n) +c 1c) ≠ ∅)))
176	175	rexlimiv 2733	. . . 4 ⊢ (∃k ∈ Nn (x = (k +c k) ∧ (k +c k) ≠ ∅) → ¬ ∃n ∈ Nn (x = ((n +c n) +c 1c) ∧ ((n +c n) +c 1c) ≠ ∅))
177		imnan 411	. . . 4 ⊢ ((∃k ∈ Nn (x = (k +c k) ∧ (k +c k) ≠ ∅) → ¬ ∃n ∈ Nn (x = ((n +c n) +c 1c) ∧ ((n +c n) +c 1c) ≠ ∅)) ↔ ¬ (∃k ∈ Nn (x = (k +c k) ∧ (k +c k) ≠ ∅) ∧ ∃n ∈ Nn (x = ((n +c n) +c 1c) ∧ ((n +c n) +c 1c) ≠ ∅)))
178	176, 177	mpbi 199	. . 3 ⊢ ¬ (∃k ∈ Nn (x = (k +c k) ∧ (k +c k) ≠ ∅) ∧ ∃n ∈ Nn (x = ((n +c n) +c 1c) ∧ ((n +c n) +c 1c) ≠ ∅))
179	178	abf 3585	. 2 ⊢ {x ∣ (∃k ∈ Nn (x = (k +c k) ∧ (k +c k) ≠ ∅) ∧ ∃n ∈ Nn (x = ((n +c n) +c 1c) ∧ ((n +c n) +c 1c) ≠ ∅))} = ∅
180	5, 179	eqtri 2373	1 ⊢ ( Evenfin ∩ Oddfin ) = ∅

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∨ wo 357   ∧ wa 358   = wceq 1642   ∈ wcel 1710  {cab 2339   ≠ wne 2517  ∀wral 2615  ∃wrex 2616   ∩ cin 3209  ∅c0 3551  1_cc1c 4135   Nn cnnc 4374  0_cc0c 4375   +_c cplc 4376   Even_fin cevenfin 4437   Odd_fin coddfin 4438

This proof depends on 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 proof 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 used by:  vinf  4556