Metamath Proof Explorer

Theorem oa00

Description: An ordinal sum is zero iff both of its arguments are zero. (Contributed by NM, 6-Dec-2004)

Ref Expression
Assertion oa00 ⊢ A ∈ On ∧ B ∈ On → A + 𝑜 B = ∅ ↔ A = ∅ ∧ B = ∅

Proof

Step Hyp Ref Expression
1 on0eln0 ⊢ A ∈ On → ∅ ∈ A ↔ A ≠ ∅
2 1 adantr ⊢ A ∈ On ∧ B ∈ On → ∅ ∈ A ↔ A ≠ ∅
3 oaword1 ⊢ A ∈ On ∧ B ∈ On → A ⊆ A + 𝑜 B
4 3 sseld ⊢ A ∈ On ∧ B ∈ On → ∅ ∈ A → ∅ ∈ A + 𝑜 B
5 2 4 sylbird ⊢ A ∈ On ∧ B ∈ On → A ≠ ∅ → ∅ ∈ A + 𝑜 B
6 ne0i ⊢ ∅ ∈ A + 𝑜 B → A + 𝑜 B ≠ ∅
7 5 6 syl6 ⊢ A ∈ On ∧ B ∈ On → A ≠ ∅ → A + 𝑜 B ≠ ∅
8 7 necon4d ⊢ A ∈ On ∧ B ∈ On → A + 𝑜 B = ∅ → A = ∅
9 on0eln0 ⊢ B ∈ On → ∅ ∈ B ↔ B ≠ ∅
10 9 adantl ⊢ A ∈ On ∧ B ∈ On → ∅ ∈ B ↔ B ≠ ∅
11 0elon ⊢ ∅ ∈ On
12 oaord ⊢ ∅ ∈ On ∧ B ∈ On ∧ A ∈ On → ∅ ∈ B ↔ A + 𝑜 ∅ ∈ A + 𝑜 B
13 11 12 mp3an1 ⊢ B ∈ On ∧ A ∈ On → ∅ ∈ B ↔ A + 𝑜 ∅ ∈ A + 𝑜 B
14 13 ancoms ⊢ A ∈ On ∧ B ∈ On → ∅ ∈ B ↔ A + 𝑜 ∅ ∈ A + 𝑜 B
15 10 14 bitr3d ⊢ A ∈ On ∧ B ∈ On → B ≠ ∅ ↔ A + 𝑜 ∅ ∈ A + 𝑜 B
16 ne0i ⊢ A + 𝑜 ∅ ∈ A + 𝑜 B → A + 𝑜 B ≠ ∅
17 15 16 syl6bi ⊢ A ∈ On ∧ B ∈ On → B ≠ ∅ → A + 𝑜 B ≠ ∅
18 17 necon4d ⊢ A ∈ On ∧ B ∈ On → A + 𝑜 B = ∅ → B = ∅
19 8 18 jcad ⊢ A ∈ On ∧ B ∈ On → A + 𝑜 B = ∅ → A = ∅ ∧ B = ∅
20 oveq12 ⊢ A = ∅ ∧ B = ∅ → A + 𝑜 B = ∅ + 𝑜 ∅
21 oa0 ⊢ ∅ ∈ On → ∅ + 𝑜 ∅ = ∅
22 11 21 ax-mp ⊢ ∅ + 𝑜 ∅ = ∅
23 20 22 eqtrdi ⊢ A = ∅ ∧ B = ∅ → A + 𝑜 B = ∅
24 19 23 impbid1 ⊢ A ∈ On ∧ B ∈ On → A + 𝑜 B = ∅ ↔ A = ∅ ∧ B = ∅