Metamath Proof Explorer


Theorem oawordexr

Description: Existence theorem for weak ordering of ordinal sum. (Contributed by NM, 12-Dec-2004)

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

Proof

Step Hyp Ref Expression
1 oaword1 A On x On A A + 𝑜 x
2 sseq2 A + 𝑜 x = B A A + 𝑜 x A B
3 1 2 syl5ibcom A On x On A + 𝑜 x = B A B
4 3 rexlimdva A On x On A + 𝑜 x = B A B
5 4 imp A On x On A + 𝑜 x = B A B