Metamath Proof Explorer

Theorem oawordeu

Description: Existence theorem for weak ordering of ordinal sum. Proposition 8.8 of TakeutiZaring p. 59. (Contributed by NM, 11-Dec-2004)

Ref Expression
Assertion oawordeu ⊢ A ∈ On ∧ B ∈ On ∧ A ⊆ B → ∃! x ∈ On A + 𝑜 x = B

Proof

Step Hyp Ref Expression
1 sseq1 ⊢ A = if A ∈ On A ∅ → A ⊆ B ↔ if A ∈ On A ∅ ⊆ B
2 oveq1 ⊢ A = if A ∈ On A ∅ → A + 𝑜 x = if A ∈ On A ∅ + 𝑜 x
3 2 eqeq1d ⊢ A = if A ∈ On A ∅ → A + 𝑜 x = B ↔ if A ∈ On A ∅ + 𝑜 x = B
4 3 reubidv ⊢ A = if A ∈ On A ∅ → ∃! x ∈ On A + 𝑜 x = B ↔ ∃! x ∈ On if A ∈ On A ∅ + 𝑜 x = B
5 1 4 imbi12d ⊢ A = if A ∈ On A ∅ → A ⊆ B → ∃! x ∈ On A + 𝑜 x = B ↔ if A ∈ On A ∅ ⊆ B → ∃! x ∈ On if A ∈ On A ∅ + 𝑜 x = B
6 sseq2 ⊢ B = if B ∈ On B ∅ → if A ∈ On A ∅ ⊆ B ↔ if A ∈ On A ∅ ⊆ if B ∈ On B ∅
7 eqeq2 ⊢ B = if B ∈ On B ∅ → if A ∈ On A ∅ + 𝑜 x = B ↔ if A ∈ On A ∅ + 𝑜 x = if B ∈ On B ∅
8 7 reubidv ⊢ B = if B ∈ On B ∅ → ∃! x ∈ On if A ∈ On A ∅ + 𝑜 x = B ↔ ∃! x ∈ On if A ∈ On A ∅ + 𝑜 x = if B ∈ On B ∅
9 6 8 imbi12d ⊢ B = if B ∈ On B ∅ → if A ∈ On A ∅ ⊆ B → ∃! x ∈ On if A ∈ On A ∅ + 𝑜 x = B ↔ if A ∈ On A ∅ ⊆ if B ∈ On B ∅ → ∃! x ∈ On if A ∈ On A ∅ + 𝑜 x = if B ∈ On B ∅
10 0elon ⊢ ∅ ∈ On
11 10 elimel ⊢ if A ∈ On A ∅ ∈ On
12 10 elimel ⊢ if B ∈ On B ∅ ∈ On
13 eqid ⊢ y ∈ On | if B ∈ On B ∅ ⊆ if A ∈ On A ∅ + 𝑜 y = y ∈ On | if B ∈ On B ∅ ⊆ if A ∈ On A ∅ + 𝑜 y
14 11 12 13 oawordeulem ⊢ if A ∈ On A ∅ ⊆ if B ∈ On B ∅ → ∃! x ∈ On if A ∈ On A ∅ + 𝑜 x = if B ∈ On B ∅
15 5 9 14 dedth2h ⊢ A ∈ On ∧ B ∈ On → A ⊆ B → ∃! x ∈ On A + 𝑜 x = B
16 15 imp ⊢ A ∈ On ∧ B ∈ On ∧ A ⊆ B → ∃! x ∈ On A + 𝑜 x = B