nnawordexg

Description: If an ordinal, B , is in a half-open interval between some A and the next limit ordinal, B is the sum of the A and some natural number. This weakens the antecedent of nnawordex . (Contributed by RP, 7-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \in On \land A \subseteq B \land B \in (A +_{𝑜} ω)) \to A \in On$
2		omelon	$⊢ ω \in On$
3	2	a1i	$⊢ (A \in On \land A \subseteq B \land B \in (A +_{𝑜} ω)) \to ω \in On$
4		3simpc	$⊢ (A \in On \land A \subseteq B \land B \in (A +_{𝑜} ω)) \to (A \subseteq B \land B \in (A +_{𝑜} ω))$
5		oawordex2	$⊢ ((A \in On \land ω \in On) \land (A \subseteq B \land B \in (A +_{𝑜} ω))) \to \exists x \in ω A +_{𝑜} x = B$
6	1 3 4 5	syl21anc	$⊢ (A \in On \land A \subseteq B \land B \in (A +_{𝑜} ω)) \to \exists x \in ω A +_{𝑜} x = B$

Metamath Proof Explorer

Theorem nnawordexg

Proof