dfsucon

Description: A is called a successor ordinal if it is not a limit ordinal and not the empty set. (Contributed by RP, 11-Nov-2023)

		Ref	Expression
	Assertion	dfsucon	$⊢ (Ord A \land \neg Lim A \land A \neq \emptyset) \leftrightarrow \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$
15		eloni	$⊢ x \in On \to Ord x$
16		ordsuc	$⊢ Ord x \leftrightarrow Ord suc x$
17	15 16	sylib	$⊢ x \in On \to Ord suc x$
18		nlimsuc	$⊢ x \in On \to \neg Lim suc x$
19		nsuceq0	$⊢ suc x \neq \emptyset$
20	19	a1i	$⊢ x \in On \to suc x \neq \emptyset$
21	17 18 20	3jca	$⊢ x \in On \to (Ord suc x \land \neg Lim suc x \land suc x \neq \emptyset)$
22		ordeq	$⊢ A = suc x \to (Ord A \leftrightarrow Ord suc x)$
23		limeq	$⊢ A = suc x \to (Lim A \leftrightarrow Lim suc x)$
24	23	notbid	$⊢ A = suc x \to (\neg Lim A \leftrightarrow \neg Lim suc x)$
25		neeq1	$⊢ A = suc x \to (A \neq \emptyset \leftrightarrow suc x \neq \emptyset)$
26	22 24 25	3anbi123d	$⊢ A = suc x \to ((Ord A \land \neg Lim A \land A \neq \emptyset) \leftrightarrow (Ord suc x \land \neg Lim suc x \land suc x \neq \emptyset))$
27	21 26	syl5ibrcom	$⊢ x \in On \to (A = suc x \to (Ord A \land \neg Lim A \land A \neq \emptyset))$
28	27	rexlimiv	$⊢ \exists x \in On A = suc x \to (Ord A \land \neg Lim A \land A \neq \emptyset)$
29	14 28	impbii	$⊢ (Ord A \land \neg Lim A \land A \neq \emptyset) \leftrightarrow \exists x \in On A = suc x$

Metamath Proof Explorer

Theorem dfsucon

Proof