Metamath Proof Explorer

Theorem oaord

Description: Ordering property of ordinal addition. Proposition 8.4 of TakeutiZaring p. 58 and its converse. (Contributed by NM, 5-Dec-2004)

Ref Expression
Assertion oaord ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ∈ B ↔ C + 𝑜 A ∈ C + 𝑜 B

Proof

Step Hyp Ref Expression
1 oaordi ⊢ B ∈ On ∧ C ∈ On → A ∈ B → C + 𝑜 A ∈ C + 𝑜 B
2 1 3adant1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ∈ B → C + 𝑜 A ∈ C + 𝑜 B
3 oveq2 ⊢ A = B → C + 𝑜 A = C + 𝑜 B
4 3 a1i ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A = B → C + 𝑜 A = C + 𝑜 B
5 oaordi ⊢ A ∈ On ∧ C ∈ On → B ∈ A → C + 𝑜 B ∈ C + 𝑜 A
6 5 3adant2 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → B ∈ A → C + 𝑜 B ∈ C + 𝑜 A
7 4 6 orim12d ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A = B ∨ B ∈ A → C + 𝑜 A = C + 𝑜 B ∨ C + 𝑜 B ∈ C + 𝑜 A
8 7 con3d ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → ¬ C + 𝑜 A = C + 𝑜 B ∨ C + 𝑜 B ∈ C + 𝑜 A → ¬ A = B ∨ B ∈ A
9 df-3an ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ↔ A ∈ On ∧ B ∈ On ∧ C ∈ On
10 ancom ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ↔ C ∈ On ∧ A ∈ On ∧ B ∈ On
11 anandi ⊢ C ∈ On ∧ A ∈ On ∧ B ∈ On ↔ C ∈ On ∧ A ∈ On ∧ C ∈ On ∧ B ∈ On
12 9 10 11 3bitri ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ↔ C ∈ On ∧ A ∈ On ∧ C ∈ On ∧ B ∈ On
13 oacl ⊢ C ∈ On ∧ A ∈ On → C + 𝑜 A ∈ On
14 eloni ⊢ C + 𝑜 A ∈ On → Ord ⁡ C + 𝑜 A
15 13 14 syl ⊢ C ∈ On ∧ A ∈ On → Ord ⁡ C + 𝑜 A
16 oacl ⊢ C ∈ On ∧ B ∈ On → C + 𝑜 B ∈ On
17 eloni ⊢ C + 𝑜 B ∈ On → Ord ⁡ C + 𝑜 B
18 16 17 syl ⊢ C ∈ On ∧ B ∈ On → Ord ⁡ C + 𝑜 B
19 15 18 anim12i ⊢ C ∈ On ∧ A ∈ On ∧ C ∈ On ∧ B ∈ On → Ord ⁡ C + 𝑜 A ∧ Ord ⁡ C + 𝑜 B
20 12 19 sylbi ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → Ord ⁡ C + 𝑜 A ∧ Ord ⁡ C + 𝑜 B
21 ordtri2 ⊢ Ord ⁡ C + 𝑜 A ∧ Ord ⁡ C + 𝑜 B → C + 𝑜 A ∈ C + 𝑜 B ↔ ¬ C + 𝑜 A = C + 𝑜 B ∨ C + 𝑜 B ∈ C + 𝑜 A
22 20 21 syl ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → C + 𝑜 A ∈ C + 𝑜 B ↔ ¬ C + 𝑜 A = C + 𝑜 B ∨ C + 𝑜 B ∈ C + 𝑜 A
23 eloni ⊢ A ∈ On → Ord ⁡ A
24 eloni ⊢ B ∈ On → Ord ⁡ B
25 23 24 anim12i ⊢ A ∈ On ∧ B ∈ On → Ord ⁡ A ∧ Ord ⁡ B
26 25 3adant3 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → Ord ⁡ A ∧ Ord ⁡ B
27 ordtri2 ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ∈ B ↔ ¬ A = B ∨ B ∈ A
28 26 27 syl ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ∈ B ↔ ¬ A = B ∨ B ∈ A
29 8 22 28 3imtr4d ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → C + 𝑜 A ∈ C + 𝑜 B → A ∈ B
30 2 29 impbid ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ∈ B ↔ C + 𝑜 A ∈ C + 𝑜 B