nnasmo

Description: Finite ordinal subtraction cancels on the left. (Contributed by Scott Fenton, 17-Oct-2024)

		Ref	Expression
	Assertion	nnasmo	$⊢ A \in ω \to \exists^{*} x \in ω A +_{𝑜} x = B$

Step	Hyp	Ref	Expression
1		eqtr3	$⊢ (A +_{𝑜} x = B \land A +_{𝑜} y = B) \to A +_{𝑜} x = A +_{𝑜} y$
2		nnacan	$⊢ (A \in ω \land x \in ω \land y \in ω) \to (A +_{𝑜} x = A +_{𝑜} y \leftrightarrow x = y)$
3	1 2	syl5ib	$⊢ (A \in ω \land x \in ω \land y \in ω) \to ((A +_{𝑜} x = B \land A +_{𝑜} y = B) \to x = y)$
4	3	3expb	$⊢ (A \in ω \land (x \in ω \land y \in ω)) \to ((A +_{𝑜} x = B \land A +_{𝑜} y = B) \to x = y)$
5	4	ralrimivva	$⊢ A \in ω \to \forall x \in ω \forall y \in ω ((A +_{𝑜} x = B \land A +_{𝑜} y = B) \to x = y)$
6		oveq2	$⊢ x = y \to A +_{𝑜} x = A +_{𝑜} y$
7	6	eqeq1d	$⊢ x = y \to (A +_{𝑜} x = B \leftrightarrow A +_{𝑜} y = B)$
8	7	rmo4	$⊢ \exists^{*} x \in ω A +_{𝑜} x = B \leftrightarrow \forall x \in ω \forall y \in ω ((A +_{𝑜} x = B \land A +_{𝑜} y = B) \to x = y)$
9	5 8	sylibr	$⊢ A \in ω \to \exists^{*} x \in ω A +_{𝑜} x = B$

Metamath Proof Explorer