Theorem oneo

Description: If an ordinal number is even, its successor is odd. (Contributed by NM, 26-Jan-2006)

	Ref	Expression
Assertion	oneo	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 = ( 2o ·o 𝐴 ) ) → ¬ suc 𝐶 = ( 2o ·o 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		onnbtwn	⊢ ( 𝐴 ∈ On → ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴 ) )
2	1	3ad2ant1	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 = ( 2o ·o 𝐴 ) ) → ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴 ) )
3		suceq	⊢ ( 𝐶 = ( 2o ·o 𝐴 ) → suc 𝐶 = suc ( 2o ·o 𝐴 ) )
4	3	eqeq1d	⊢ ( 𝐶 = ( 2o ·o 𝐴 ) → ( suc 𝐶 = ( 2o ·o 𝐵 ) ↔ suc ( 2o ·o 𝐴 ) = ( 2o ·o 𝐵 ) ) )
5	4	3ad2ant3	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 = ( 2o ·o 𝐴 ) ) → ( suc 𝐶 = ( 2o ·o 𝐵 ) ↔ suc ( 2o ·o 𝐴 ) = ( 2o ·o 𝐵 ) ) )
6		ovex	⊢ ( 2o ·o 𝐴 ) ∈ V
7	6	sucid	⊢ ( 2o ·o 𝐴 ) ∈ suc ( 2o ·o 𝐴 )
8		eleq2	⊢ ( suc ( 2o ·o 𝐴 ) = ( 2o ·o 𝐵 ) → ( ( 2o ·o 𝐴 ) ∈ suc ( 2o ·o 𝐴 ) ↔ ( 2o ·o 𝐴 ) ∈ ( 2o ·o 𝐵 ) ) )
9	7 8	mpbii	⊢ ( suc ( 2o ·o 𝐴 ) = ( 2o ·o 𝐵 ) → ( 2o ·o 𝐴 ) ∈ ( 2o ·o 𝐵 ) )
10		2on	⊢ 2o ∈ On
11		omord	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 2o ∈ On ) → ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 2o ) ↔ ( 2o ·o 𝐴 ) ∈ ( 2o ·o 𝐵 ) ) )
12	10 11	mp3an3	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 2o ) ↔ ( 2o ·o 𝐴 ) ∈ ( 2o ·o 𝐵 ) ) )
13		simpl	⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 2o ) → 𝐴 ∈ 𝐵 )
14	12 13	syl6bir	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 2o ·o 𝐴 ) ∈ ( 2o ·o 𝐵 ) → 𝐴 ∈ 𝐵 ) )
15	9 14	syl5	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( suc ( 2o ·o 𝐴 ) = ( 2o ·o 𝐵 ) → 𝐴 ∈ 𝐵 ) )
16		simpr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ suc ( 2o ·o 𝐴 ) = ( 2o ·o 𝐵 ) ) → suc ( 2o ·o 𝐴 ) = ( 2o ·o 𝐵 ) )
17		omcl	⊢ ( ( 2o ∈ On ∧ 𝐴 ∈ On ) → ( 2o ·o 𝐴 ) ∈ On )
18	10 17	mpan	⊢ ( 𝐴 ∈ On → ( 2o ·o 𝐴 ) ∈ On )
19		oa1suc	⊢ ( ( 2o ·o 𝐴 ) ∈ On → ( ( 2o ·o 𝐴 ) +o 1o ) = suc ( 2o ·o 𝐴 ) )
20	18 19	syl	⊢ ( 𝐴 ∈ On → ( ( 2o ·o 𝐴 ) +o 1o ) = suc ( 2o ·o 𝐴 ) )
21		1oex	⊢ 1o ∈ V
22	21	sucid	⊢ 1o ∈ suc 1o
23		df-2o	⊢ 2o = suc 1o
24	22 23	eleqtrri	⊢ 1o ∈ 2o
25		1on	⊢ 1o ∈ On
26		oaord	⊢ ( ( 1o ∈ On ∧ 2o ∈ On ∧ ( 2o ·o 𝐴 ) ∈ On ) → ( 1o ∈ 2o ↔ ( ( 2o ·o 𝐴 ) +o 1o ) ∈ ( ( 2o ·o 𝐴 ) +o 2o ) ) )
27	25 10 18 26	mp3an12i	⊢ ( 𝐴 ∈ On → ( 1o ∈ 2o ↔ ( ( 2o ·o 𝐴 ) +o 1o ) ∈ ( ( 2o ·o 𝐴 ) +o 2o ) ) )
28	24 27	mpbii	⊢ ( 𝐴 ∈ On → ( ( 2o ·o 𝐴 ) +o 1o ) ∈ ( ( 2o ·o 𝐴 ) +o 2o ) )
29		omsuc	⊢ ( ( 2o ∈ On ∧ 𝐴 ∈ On ) → ( 2o ·o suc 𝐴 ) = ( ( 2o ·o 𝐴 ) +o 2o ) )
30	10 29	mpan	⊢ ( 𝐴 ∈ On → ( 2o ·o suc 𝐴 ) = ( ( 2o ·o 𝐴 ) +o 2o ) )
31	28 30	eleqtrrd	⊢ ( 𝐴 ∈ On → ( ( 2o ·o 𝐴 ) +o 1o ) ∈ ( 2o ·o suc 𝐴 ) )
32	20 31	eqeltrrd	⊢ ( 𝐴 ∈ On → suc ( 2o ·o 𝐴 ) ∈ ( 2o ·o suc 𝐴 ) )
33	32	ad2antrr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ suc ( 2o ·o 𝐴 ) = ( 2o ·o 𝐵 ) ) → suc ( 2o ·o 𝐴 ) ∈ ( 2o ·o suc 𝐴 ) )
34	16 33	eqeltrrd	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ suc ( 2o ·o 𝐴 ) = ( 2o ·o 𝐵 ) ) → ( 2o ·o 𝐵 ) ∈ ( 2o ·o suc 𝐴 ) )
35		suceloni	⊢ ( 𝐴 ∈ On → suc 𝐴 ∈ On )
36		omord	⊢ ( ( 𝐵 ∈ On ∧ suc 𝐴 ∈ On ∧ 2o ∈ On ) → ( ( 𝐵 ∈ suc 𝐴 ∧ ∅ ∈ 2o ) ↔ ( 2o ·o 𝐵 ) ∈ ( 2o ·o suc 𝐴 ) ) )
37	10 36	mp3an3	⊢ ( ( 𝐵 ∈ On ∧ suc 𝐴 ∈ On ) → ( ( 𝐵 ∈ suc 𝐴 ∧ ∅ ∈ 2o ) ↔ ( 2o ·o 𝐵 ) ∈ ( 2o ·o suc 𝐴 ) ) )
38	35 37	sylan2	⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( ( 𝐵 ∈ suc 𝐴 ∧ ∅ ∈ 2o ) ↔ ( 2o ·o 𝐵 ) ∈ ( 2o ·o suc 𝐴 ) ) )
39	38	ancoms	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐵 ∈ suc 𝐴 ∧ ∅ ∈ 2o ) ↔ ( 2o ·o 𝐵 ) ∈ ( 2o ·o suc 𝐴 ) ) )
40	39	adantr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ suc ( 2o ·o 𝐴 ) = ( 2o ·o 𝐵 ) ) → ( ( 𝐵 ∈ suc 𝐴 ∧ ∅ ∈ 2o ) ↔ ( 2o ·o 𝐵 ) ∈ ( 2o ·o suc 𝐴 ) ) )
41	34 40	mpbird	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ suc ( 2o ·o 𝐴 ) = ( 2o ·o 𝐵 ) ) → ( 𝐵 ∈ suc 𝐴 ∧ ∅ ∈ 2o ) )
42	41	simpld	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ suc ( 2o ·o 𝐴 ) = ( 2o ·o 𝐵 ) ) → 𝐵 ∈ suc 𝐴 )
43	42	ex	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( suc ( 2o ·o 𝐴 ) = ( 2o ·o 𝐵 ) → 𝐵 ∈ suc 𝐴 ) )
44	15 43	jcad	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( suc ( 2o ·o 𝐴 ) = ( 2o ·o 𝐵 ) → ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴 ) ) )
45	44	3adant3	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 = ( 2o ·o 𝐴 ) ) → ( suc ( 2o ·o 𝐴 ) = ( 2o ·o 𝐵 ) → ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴 ) ) )
46	5 45	sylbid	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 = ( 2o ·o 𝐴 ) ) → ( suc 𝐶 = ( 2o ·o 𝐵 ) → ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴 ) ) )
47	2 46	mtod	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 = ( 2o ·o 𝐴 ) ) → ¬ suc 𝐶 = ( 2o ·o 𝐵 ) )