Theorem oawordexr

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

	Ref	Expression
Assertion	oawordexr	$$⊢\left(A\in \mathrm{On}\wedge \exists x\in \mathrm{On}A{+}_{𝑜}x=B\right)\to A\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		oaword1	$$⊢\left(A\in \mathrm{On}\wedge x\in \mathrm{On}\right)\to A\subseteq A{+}_{𝑜}x$$
2		sseq2	$$⊢A{+}_{𝑜}x=B\to \left(A\subseteq A{+}_{𝑜}x\leftrightarrow A\subseteq B\right)$$
3	1 2	syl5ibcom	$$⊢\left(A\in \mathrm{On}\wedge x\in \mathrm{On}\right)\to \left(A{+}_{𝑜}x=B\to A\subseteq B\right)$$
4	3	rexlimdva	$$⊢A\in \mathrm{On}\to \left(\exists x\in \mathrm{On}A{+}_{𝑜}x=B\to A\subseteq B\right)$$
5	4	imp	$$⊢\left(A\in \mathrm{On}\wedge \exists x\in \mathrm{On}A{+}_{𝑜}x=B\right)\to A\subseteq B$$