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