Metamath Proof Explorer

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