faosnf0.11b

Description: B is called a non-limit ordinal if it is not a limit ordinal. (Contributed by RP, 27-Sep-2023)

Alling, Norman L. "Fundamentals of Analysis Over Surreal Numbers Fields." The Rocky Mountain Journal of Mathematics 19, no. 3 (1989): 565-73. http://www.jstor.org/stable/44237243.

		Ref	Expression
	Assertion	faosnf0.11b	$⊢ (Ord A \land \neg Lim A \land A \neq \emptyset) \to \exists x \in On A = suc x$

Proof

Step	Hyp	Ref	Expression
1		3ancomb	$⊢ (Ord A \land \neg Lim A \land A \neq \emptyset) \leftrightarrow (Ord A \land A \neq \emptyset \land \neg Lim A)$
2		df-3an	$⊢ (Ord A \land A \neq \emptyset \land \neg Lim A) \leftrightarrow ((Ord A \land A \neq \emptyset) \land \neg Lim A)$
3		df-ne	$⊢ A \neq \emptyset \leftrightarrow \neg A = \emptyset$
4	3	anbi2i	$⊢ (Ord A \land A \neq \emptyset) \leftrightarrow (Ord A \land \neg A = \emptyset)$
5	4	imbi1i	$⊢ ((Ord A \land A \neq \emptyset) \to \exists x \in On A = suc x) \leftrightarrow ((Ord A \land \neg A = \emptyset) \to \exists x \in On A = suc x)$
6		pm5.6	$⊢ ((Ord A \land \neg A = \emptyset) \to \exists x \in On A = suc x) \leftrightarrow (Ord A \to (A = \emptyset \lor \exists x \in On A = suc x))$
7		iman	$⊢ (Ord A \to (A = \emptyset \lor \exists x \in On A = suc x)) \leftrightarrow \neg (Ord A \land \neg (A = \emptyset \lor \exists x \in On A = suc x))$
8	5 6 7	3bitrri	$⊢ \neg (Ord A \land \neg (A = \emptyset \lor \exists x \in On A = suc x)) \leftrightarrow ((Ord A \land A \neq \emptyset) \to \exists x \in On A = suc x)$
9		dflim3	$⊢ Lim A \leftrightarrow (Ord A \land \neg (A = \emptyset \lor \exists x \in On A = suc x))$
10	8 9	xchnxbir	$⊢ \neg Lim A \leftrightarrow ((Ord A \land A \neq \emptyset) \to \exists x \in On A = suc x)$
11	10	anbi2i	$⊢ ((Ord A \land A \neq \emptyset) \land \neg Lim A) \leftrightarrow ((Ord A \land A \neq \emptyset) \land ((Ord A \land A \neq \emptyset) \to \exists x \in On A = suc x))$
12	1 2 11	3bitri	$⊢ (Ord A \land \neg Lim A \land A \neq \emptyset) \leftrightarrow ((Ord A \land A \neq \emptyset) \land ((Ord A \land A \neq \emptyset) \to \exists x \in On A = suc x))$
13		pm3.35	$⊢ ((Ord A \land A \neq \emptyset) \land ((Ord A \land A \neq \emptyset) \to \exists x \in On A = suc x)) \to \exists x \in On A = suc x$
14	12 13	sylbi	$⊢ (Ord A \land \neg Lim A \land A \neq \emptyset) \to \exists x \in On A = suc x$

Metamath Proof Explorer

Theorem faosnf0.11b

Proof