Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Ordinal arithmetic
omword
Next ⟩
omwordi
Metamath Proof Explorer
Ascii
Unicode
Theorem
omword
Description:
Weak ordering property of ordinal multiplication.
(Contributed by
NM
, 21-Dec-2004)
Ref
Expression
Assertion
omword
⊢
A
∈
On
∧
B
∈
On
∧
C
∈
On
∧
∅
∈
C
→
A
⊆
B
↔
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
3anrot
⊢
C
∈
On
∧
A
∈
On
∧
B
∈
On
↔
A
∈
On
∧
B
∈
On
∧
C
∈
On
3
omcan
⊢
C
∈
On
∧
A
∈
On
∧
B
∈
On
∧
∅
∈
C
→
C
⋅
𝑜
A
=
C
⋅
𝑜
B
↔
A
=
B
4
2
3
sylanbr
⊢
A
∈
On
∧
B
∈
On
∧
C
∈
On
∧
∅
∈
C
→
C
⋅
𝑜
A
=
C
⋅
𝑜
B
↔
A
=
B
5
4
bicomd
⊢
A
∈
On
∧
B
∈
On
∧
C
∈
On
∧
∅
∈
C
→
A
=
B
↔
C
⋅
𝑜
A
=
C
⋅
𝑜
B
6
1
5
orbi12d
⊢
A
∈
On
∧
B
∈
On
∧
C
∈
On
∧
∅
∈
C
→
A
∈
B
∨
A
=
B
↔
C
⋅
𝑜
A
∈
C
⋅
𝑜
B
∨
C
⋅
𝑜
A
=
C
⋅
𝑜
B
7
onsseleq
⊢
A
∈
On
∧
B
∈
On
→
A
⊆
B
↔
A
∈
B
∨
A
=
B
8
7
3adant3
⊢
A
∈
On
∧
B
∈
On
∧
C
∈
On
→
A
⊆
B
↔
A
∈
B
∨
A
=
B
9
8
adantr
⊢
A
∈
On
∧
B
∈
On
∧
C
∈
On
∧
∅
∈
C
→
A
⊆
B
↔
A
∈
B
∨
A
=
B
10
omcl
⊢
C
∈
On
∧
A
∈
On
→
C
⋅
𝑜
A
∈
On
11
omcl
⊢
C
∈
On
∧
B
∈
On
→
C
⋅
𝑜
B
∈
On
12
10
11
anim12dan
⊢
C
∈
On
∧
A
∈
On
∧
B
∈
On
→
C
⋅
𝑜
A
∈
On
∧
C
⋅
𝑜
B
∈
On
13
12
ancoms
⊢
A
∈
On
∧
B
∈
On
∧
C
∈
On
→
C
⋅
𝑜
A
∈
On
∧
C
⋅
𝑜
B
∈
On
14
13
3impa
⊢
A
∈
On
∧
B
∈
On
∧
C
∈
On
→
C
⋅
𝑜
A
∈
On
∧
C
⋅
𝑜
B
∈
On
15
onsseleq
⊢
C
⋅
𝑜
A
∈
On
∧
C
⋅
𝑜
B
∈
On
→
C
⋅
𝑜
A
⊆
C
⋅
𝑜
B
↔
C
⋅
𝑜
A
∈
C
⋅
𝑜
B
∨
C
⋅
𝑜
A
=
C
⋅
𝑜
B
16
14
15
syl
⊢
A
∈
On
∧
B
∈
On
∧
C
∈
On
→
C
⋅
𝑜
A
⊆
C
⋅
𝑜
B
↔
C
⋅
𝑜
A
∈
C
⋅
𝑜
B
∨
C
⋅
𝑜
A
=
C
⋅
𝑜
B
17
16
adantr
⊢
A
∈
On
∧
B
∈
On
∧
C
∈
On
∧
∅
∈
C
→
C
⋅
𝑜
A
⊆
C
⋅
𝑜
B
↔
C
⋅
𝑜
A
∈
C
⋅
𝑜
B
∨
C
⋅
𝑜
A
=
C
⋅
𝑜
B
18
6
9
17
3bitr4d
⊢
A
∈
On
∧
B
∈
On
∧
C
∈
On
∧
∅
∈
C
→
A
⊆
B
↔
C
⋅
𝑜
A
⊆
C
⋅
𝑜
B