oawordex2

Description: If C is between A (inclusive) and ( A +o B ) (exclusive), there is an ordinal which equals C when summed to A . This is a slightly different statement than oawordex or oawordeu . (Contributed by RP, 7-Jan-2025)

		Ref	Expression
	Assertion	oawordex2	$⊢ ((A \in On \land B \in On) \land (A \subseteq C \land C \in (A +_{𝑜} B))) \to \exists x \in B A +_{𝑜} x = C$

Proof

Step	Hyp	Ref	Expression
1		simprl	$⊢ ((A \in On \land B \in On) \land (A \subseteq C \land C \in (A +_{𝑜} B))) \to A \subseteq C$
2		simpll	$⊢ ((A \in On \land B \in On) \land (A \subseteq C \land C \in (A +_{𝑜} B))) \to A \in On$
3		oacl	$⊢ (A \in On \land B \in On) \to A +_{𝑜} B \in On$
4		simpr	$⊢ (A \subseteq C \land C \in (A +_{𝑜} B)) \to C \in (A +_{𝑜} B)$
5		onelon	$⊢ (A +_{𝑜} B \in On \land C \in (A +_{𝑜} B)) \to C \in On$
6	3 4 5	syl2an	$⊢ ((A \in On \land B \in On) \land (A \subseteq C \land C \in (A +_{𝑜} B))) \to C \in On$
7		oawordex	$⊢ (A \in On \land C \in On) \to (A \subseteq C \leftrightarrow \exists x \in On A +_{𝑜} x = C)$
8	2 6 7	syl2anc	$⊢ ((A \in On \land B \in On) \land (A \subseteq C \land C \in (A +_{𝑜} B))) \to (A \subseteq C \leftrightarrow \exists x \in On A +_{𝑜} x = C)$
9	1 8	mpbid	$⊢ ((A \in On \land B \in On) \land (A \subseteq C \land C \in (A +_{𝑜} B))) \to \exists x \in On A +_{𝑜} x = C$
10		simprr	$⊢ (((A \in On \land B \in On) \land (A \subseteq C \land C \in (A +_{𝑜} B))) \land (x \in On \land A +_{𝑜} x = C)) \to A +_{𝑜} x = C$
11		simprr	$⊢ ((A \in On \land B \in On) \land (A \subseteq C \land C \in (A +_{𝑜} B))) \to C \in (A +_{𝑜} B)$
12	11	adantr	$⊢ (((A \in On \land B \in On) \land (A \subseteq C \land C \in (A +_{𝑜} B))) \land (x \in On \land A +_{𝑜} x = C)) \to C \in (A +_{𝑜} B)$
13	10 12	eqeltrd	$⊢ (((A \in On \land B \in On) \land (A \subseteq C \land C \in (A +_{𝑜} B))) \land (x \in On \land A +_{𝑜} x = C)) \to A +_{𝑜} x \in (A +_{𝑜} B)$
14		simprl	$⊢ (((A \in On \land B \in On) \land (A \subseteq C \land C \in (A +_{𝑜} B))) \land (x \in On \land A +_{𝑜} x = C)) \to x \in On$
15		simpllr	$⊢ (((A \in On \land B \in On) \land (A \subseteq C \land C \in (A +_{𝑜} B))) \land (x \in On \land A +_{𝑜} x = C)) \to B \in On$
16	2	adantr	$⊢ (((A \in On \land B \in On) \land (A \subseteq C \land C \in (A +_{𝑜} B))) \land (x \in On \land A +_{𝑜} x = C)) \to A \in On$
17		oaord	$⊢ (x \in On \land B \in On \land A \in On) \to (x \in B \leftrightarrow A +_{𝑜} x \in (A +_{𝑜} B))$
18	14 15 16 17	syl3anc	$⊢ (((A \in On \land B \in On) \land (A \subseteq C \land C \in (A +_{𝑜} B))) \land (x \in On \land A +_{𝑜} x = C)) \to (x \in B \leftrightarrow A +_{𝑜} x \in (A +_{𝑜} B))$
19	13 18	mpbird	$⊢ (((A \in On \land B \in On) \land (A \subseteq C \land C \in (A +_{𝑜} B))) \land (x \in On \land A +_{𝑜} x = C)) \to x \in B$
20	9 19 10	reximssdv	$⊢ ((A \in On \land B \in On) \land (A \subseteq C \land C \in (A +_{𝑜} B))) \to \exists x \in B A +_{𝑜} x = C$

Metamath Proof Explorer

Theorem oawordex2

Proof