Metamath Proof Explorer

Theorem omord

Description: Ordering property of ordinal multiplication. Proposition 8.19 of TakeutiZaring p. 63. Theorem 3.16 of Schloeder p. 9. (Contributed by NM, 14-Dec-2004)

Ref Expression
Assertion omord ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ∈ B ∧ ∅ ∈ C ↔ C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B

Proof

Step Hyp Ref Expression
1 omord2 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ ∅ ∈ C → A ∈ B ↔ C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B
2 1 ex ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → ∅ ∈ C → A ∈ B ↔ C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B
3 2 pm5.32rd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ∈ B ∧ ∅ ∈ C ↔ C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B ∧ ∅ ∈ C
4 simpl ⊢ C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B ∧ ∅ ∈ C → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B
5 ne0i ⊢ C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B → C ⋅ 𝑜 B ≠ ∅
6 om0r ⊢ B ∈ On → ∅ ⋅ 𝑜 B = ∅
7 oveq1 ⊢ C = ∅ → C ⋅ 𝑜 B = ∅ ⋅ 𝑜 B
8 7 eqeq1d ⊢ C = ∅ → C ⋅ 𝑜 B = ∅ ↔ ∅ ⋅ 𝑜 B = ∅
9 6 8 syl5ibrcom ⊢ B ∈ On → C = ∅ → C ⋅ 𝑜 B = ∅
10 9 necon3d ⊢ B ∈ On → C ⋅ 𝑜 B ≠ ∅ → C ≠ ∅
11 5 10 syl5 ⊢ B ∈ On → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B → C ≠ ∅
12 11 adantr ⊢ B ∈ On ∧ C ∈ On → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B → C ≠ ∅
13 on0eln0 ⊢ C ∈ On → ∅ ∈ C ↔ C ≠ ∅
14 13 adantl ⊢ B ∈ On ∧ C ∈ On → ∅ ∈ C ↔ C ≠ ∅
15 12 14 sylibrd ⊢ B ∈ On ∧ C ∈ On → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B → ∅ ∈ C
16 15 3adant1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B → ∅ ∈ C
17 16 ancld ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B ∧ ∅ ∈ C
18 4 17 impbid2 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B ∧ ∅ ∈ C ↔ C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B
19 3 18 bitrd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ∈ B ∧ ∅ ∈ C ↔ C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B