This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrrdi ⊢ ( ( 𝐴 ∈ 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 onsuc ⊢ ( 𝐴 ∈ 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 𝐵 ) )