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 ⊢ A ∈ On ∧ B ∈ On ∧ C = 2 𝑜 ⋅ 𝑜 A → ¬ suc ⁡ C = 2 𝑜 ⋅ 𝑜 B

Proof

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