Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Ordinal arithmetic
om00el
Next ⟩
omordlim
Metamath Proof Explorer
Ascii
Unicode
Theorem
om00el
Description:
The product of two nonzero ordinal numbers is nonzero.
(Contributed by
NM
, 28-Dec-2004)
Ref
Expression
Assertion
om00el
⊢
A
∈
On
∧
B
∈
On
→
∅
∈
A
⋅
𝑜
B
↔
∅
∈
A
∧
∅
∈
B
Proof
Step
Hyp
Ref
Expression
1
om00
⊢
A
∈
On
∧
B
∈
On
→
A
⋅
𝑜
B
=
∅
↔
A
=
∅
∨
B
=
∅
2
1
necon3abid
⊢
A
∈
On
∧
B
∈
On
→
A
⋅
𝑜
B
≠
∅
↔
¬
A
=
∅
∨
B
=
∅
3
omcl
⊢
A
∈
On
∧
B
∈
On
→
A
⋅
𝑜
B
∈
On
4
on0eln0
⊢
A
⋅
𝑜
B
∈
On
→
∅
∈
A
⋅
𝑜
B
↔
A
⋅
𝑜
B
≠
∅
5
3
4
syl
⊢
A
∈
On
∧
B
∈
On
→
∅
∈
A
⋅
𝑜
B
↔
A
⋅
𝑜
B
≠
∅
6
on0eln0
⊢
A
∈
On
→
∅
∈
A
↔
A
≠
∅
7
on0eln0
⊢
B
∈
On
→
∅
∈
B
↔
B
≠
∅
8
6
7
bi2anan9
⊢
A
∈
On
∧
B
∈
On
→
∅
∈
A
∧
∅
∈
B
↔
A
≠
∅
∧
B
≠
∅
9
neanior
⊢
A
≠
∅
∧
B
≠
∅
↔
¬
A
=
∅
∨
B
=
∅
10
8
9
bitrdi
⊢
A
∈
On
∧
B
∈
On
→
∅
∈
A
∧
∅
∈
B
↔
¬
A
=
∅
∨
B
=
∅
11
2
5
10
3bitr4d
⊢
A
∈
On
∧
B
∈
On
→
∅
∈
A
⋅
𝑜
B
↔
∅
∈
A
∧
∅
∈
B