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