Theorem om00

Description: The product of two ordinal numbers is zero iff at least one of them is zero. Proposition 8.22 of TakeutiZaring p. 64. (Contributed by NM, 21-Dec-2004)

	Ref	Expression
Assertion	om00	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 ·o 𝐵 ) = ∅ ↔ ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) ) )

Proof

Step	Hyp	Ref	Expression
1		neanior	⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ↔ ¬ ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) )
2		eloni	⊢ ( 𝐴 ∈ On → Ord 𝐴 )
3		ordge1n0	⊢ ( Ord 𝐴 → ( 1o ⊆ 𝐴 ↔ 𝐴 ≠ ∅ ) )
4	2 3	syl	⊢ ( 𝐴 ∈ On → ( 1o ⊆ 𝐴 ↔ 𝐴 ≠ ∅ ) )
5	4	biimprd	⊢ ( 𝐴 ∈ On → ( 𝐴 ≠ ∅ → 1o ⊆ 𝐴 ) )
6	5	adantr	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ≠ ∅ → 1o ⊆ 𝐴 ) )
7		on0eln0	⊢ ( 𝐵 ∈ On → ( ∅ ∈ 𝐵 ↔ 𝐵 ≠ ∅ ) )
8	7	adantl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∅ ∈ 𝐵 ↔ 𝐵 ≠ ∅ ) )
9		omword1	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∅ ∈ 𝐵 ) → 𝐴 ⊆ ( 𝐴 ·o 𝐵 ) )
10	9	ex	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∅ ∈ 𝐵 → 𝐴 ⊆ ( 𝐴 ·o 𝐵 ) ) )
11	8 10	sylbird	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐵 ≠ ∅ → 𝐴 ⊆ ( 𝐴 ·o 𝐵 ) ) )
12	6 11	anim12d	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) → ( 1o ⊆ 𝐴 ∧ 𝐴 ⊆ ( 𝐴 ·o 𝐵 ) ) ) )
13		sstr	⊢ ( ( 1o ⊆ 𝐴 ∧ 𝐴 ⊆ ( 𝐴 ·o 𝐵 ) ) → 1o ⊆ ( 𝐴 ·o 𝐵 ) )
14	12 13	syl6	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) → 1o ⊆ ( 𝐴 ·o 𝐵 ) ) )
15	1 14	biimtrrid	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ¬ ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) → 1o ⊆ ( 𝐴 ·o 𝐵 ) ) )
16		omcl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·o 𝐵 ) ∈ On )
17		eloni	⊢ ( ( 𝐴 ·o 𝐵 ) ∈ On → Ord ( 𝐴 ·o 𝐵 ) )
18		ordge1n0	⊢ ( Ord ( 𝐴 ·o 𝐵 ) → ( 1o ⊆ ( 𝐴 ·o 𝐵 ) ↔ ( 𝐴 ·o 𝐵 ) ≠ ∅ ) )
19	16 17 18	3syl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 1o ⊆ ( 𝐴 ·o 𝐵 ) ↔ ( 𝐴 ·o 𝐵 ) ≠ ∅ ) )
20	15 19	sylibd	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ¬ ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) → ( 𝐴 ·o 𝐵 ) ≠ ∅ ) )
21	20	necon4bd	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 ·o 𝐵 ) = ∅ → ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) ) )
22		oveq1	⊢ ( 𝐴 = ∅ → ( 𝐴 ·o 𝐵 ) = ( ∅ ·o 𝐵 ) )
23		om0r	⊢ ( 𝐵 ∈ On → ( ∅ ·o 𝐵 ) = ∅ )
24	22 23	sylan9eqr	⊢ ( ( 𝐵 ∈ On ∧ 𝐴 = ∅ ) → ( 𝐴 ·o 𝐵 ) = ∅ )
25	24	ex	⊢ ( 𝐵 ∈ On → ( 𝐴 = ∅ → ( 𝐴 ·o 𝐵 ) = ∅ ) )
26	25	adantl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 = ∅ → ( 𝐴 ·o 𝐵 ) = ∅ ) )
27		oveq2	⊢ ( 𝐵 = ∅ → ( 𝐴 ·o 𝐵 ) = ( 𝐴 ·o ∅ ) )
28		om0	⊢ ( 𝐴 ∈ On → ( 𝐴 ·o ∅ ) = ∅ )
29	27 28	sylan9eqr	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 = ∅ ) → ( 𝐴 ·o 𝐵 ) = ∅ )
30	29	ex	⊢ ( 𝐴 ∈ On → ( 𝐵 = ∅ → ( 𝐴 ·o 𝐵 ) = ∅ ) )
31	30	adantr	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐵 = ∅ → ( 𝐴 ·o 𝐵 ) = ∅ ) )
32	26 31	jaod	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) → ( 𝐴 ·o 𝐵 ) = ∅ ) )
33	21 32	impbid	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 ·o 𝐵 ) = ∅ ↔ ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) ) )