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