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 ( ( 𝐴 ∈ 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 syl5bir ⊢ ( ( 𝐴 ∈ 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 𝐵 ) = ∅ ↔ ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) ) )