This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in On \land \exists x \in On A +_{𝑜} x = B) \to A \subseteq B$

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