Metamath Proof Explorer

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 ⊢ A ∈ On ∧ B ∈ On → A ⋅ 𝑜 B = ∅ ↔ A = ∅ ∨ B = ∅

Proof

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