Metamath Proof Explorer


Theorem oawordex

Description: Existence theorem for weak ordering of ordinal sum. Proposition 8.8 of TakeutiZaring p. 59 and its converse. See oawordeu for uniqueness. (Contributed by NM, 12-Dec-2004)

Ref Expression
Assertion oawordex A On B On A B x On A + 𝑜 x = B

Proof

Step Hyp Ref Expression
1 oawordeu A On B On A B ∃! x On A + 𝑜 x = B
2 1 ex A On B On A B ∃! x On A + 𝑜 x = B
3 reurex ∃! x On A + 𝑜 x = B x On A + 𝑜 x = B
4 2 3 syl6 A On B On A B x On A + 𝑜 x = B
5 oawordexr A On x On A + 𝑜 x = B A B
6 5 ex A On x On A + 𝑜 x = B A B
7 6 adantr A On B On x On A + 𝑜 x = B A B
8 4 7 impbid A On B On A B x On A + 𝑜 x = B