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

Proof

Step	Hyp	Ref	Expression
1		oawordeu	$⊢ ((A \in On \land B \in On) \land A \subseteq B) \to \exists! x \in On A +_{𝑜} x = B$
2	1	ex	$⊢ (A \in On \land B \in On) \to (A \subseteq B \to \exists! x \in On A +_{𝑜} x = B)$
3		reurex	$⊢ \exists! x \in On A +_{𝑜} x = B \to \exists x \in On A +_{𝑜} x = B$
4	2 3	syl6	$⊢ (A \in On \land B \in On) \to (A \subseteq B \to \exists x \in On A +_{𝑜} x = B)$
5		oawordexr	$⊢ (A \in On \land \exists x \in On A +_{𝑜} x = B) \to A \subseteq B$
6	5	ex	$⊢ A \in On \to (\exists x \in On A +_{𝑜} x = B \to A \subseteq B)$
7	6	adantr	$⊢ (A \in On \land B \in On) \to (\exists x \in On A +_{𝑜} x = B \to A \subseteq B)$
8	4 7	impbid	$⊢ (A \in On \land B \in On) \to (A \subseteq B \leftrightarrow \exists x \in On A +_{𝑜} x = B)$