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 e. On /\ B e. On ) -> ( (/) e. ( A .o B ) <-> ( (/) e. A /\ (/) e. B ) ) )

Proof

Step Hyp Ref Expression
1 om00 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A .o B ) = (/) <-> ( A = (/) \/ B = (/) ) ) )
2 1 necon3abid 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A .o B ) =/= (/) <-> -. ( A = (/) \/ B = (/) ) ) )
3 omcl 
 |-  ( ( A e. On /\ B e. On ) -> ( A .o B ) e. On )
4 on0eln0 
 |-  ( ( A .o B ) e. On -> ( (/) e. ( A .o B ) <-> ( A .o B ) =/= (/) ) )
5 3 4 syl 
 |-  ( ( A e. On /\ B e. On ) -> ( (/) e. ( A .o B ) <-> ( A .o B ) =/= (/) ) )
6 on0eln0 
 |-  ( A e. On -> ( (/) e. A <-> A =/= (/) ) )
7 on0eln0 
 |-  ( B e. On -> ( (/) e. B <-> B =/= (/) ) )
8 6 7 bi2anan9 
 |-  ( ( A e. On /\ B e. On ) -> ( ( (/) e. A /\ (/) e. B ) <-> ( A =/= (/) /\ B =/= (/) ) ) )
9 neanior 
 |-  ( ( A =/= (/) /\ B =/= (/) ) <-> -. ( A = (/) \/ B = (/) ) )
10 8 9 bitrdi 
 |-  ( ( A e. On /\ B e. On ) -> ( ( (/) e. A /\ (/) e. B ) <-> -. ( A = (/) \/ B = (/) ) ) )
11 2 5 10 3bitr4d 
 |-  ( ( A e. On /\ B e. On ) -> ( (/) e. ( A .o B ) <-> ( (/) e. A /\ (/) e. B ) ) )