This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∅ ∈ ( 𝐴 ·o 𝐵 ) ↔ ( ∅ ∈ 𝐴 ∧ ∅ ∈ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 om00 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 ·o 𝐵 ) = ∅ ↔ ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) ) )
2 1 necon3abid ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 ·o 𝐵 ) ≠ ∅ ↔ ¬ ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) ) )
3 omcl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·o 𝐵 ) ∈ On )
4 on0eln0 ⊢ ( ( 𝐴 ·o 𝐵 ) ∈ On → ( ∅ ∈ ( 𝐴 ·o 𝐵 ) ↔ ( 𝐴 ·o 𝐵 ) ≠ ∅ ) )
5 3 4 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∅ ∈ ( 𝐴 ·o 𝐵 ) ↔ ( 𝐴 ·o 𝐵 ) ≠ ∅ ) )
6 on0eln0 ⊢ ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅ ) )
7 on0eln0 ⊢ ( 𝐵 ∈ On → ( ∅ ∈ 𝐵 ↔ 𝐵 ≠ ∅ ) )
8 6 7 bi2anan9 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( ∅ ∈ 𝐴 ∧ ∅ ∈ 𝐵 ) ↔ ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ) )
9 neanior ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ↔ ¬ ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) )
10 8 9 bitrdi ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( ∅ ∈ 𝐴 ∧ ∅ ∈ 𝐵 ) ↔ ¬ ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) ) )
11 2 5 10 3bitr4d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∅ ∈ ( 𝐴 ·o 𝐵 ) ↔ ( ∅ ∈ 𝐴 ∧ ∅ ∈ 𝐵 ) ) )