onsucf1olem

Description: The successor operation is bijective between the ordinals and the class of successor ordinals. Lemma 1.17 of Schloeder p. 2. (Contributed by RP, 18-Jan-2025)

		Ref	Expression
	Assertion	onsucf1olem	$⊢ (A \in On \land A \neq \emptyset \land \neg Lim A) \to \exists! b \in On A = suc b$

Proof

Step	Hyp	Ref	Expression
1		onuni	$⊢ A \in On \to ⋃ A \in On$
2	1	3ad2ant1	$⊢ (A \in On \land A \neq \emptyset \land \neg Lim A) \to ⋃ A \in On$
3		eloni	$⊢ A \in On \to Ord A$
4		unizlim	$⊢ Ord A \to (A = ⋃ A \leftrightarrow (A = \emptyset \lor Lim A))$
5		oran	$⊢ (A = \emptyset \lor Lim A) \leftrightarrow \neg (\neg A = \emptyset \land \neg Lim A)$
6		df-ne	$⊢ A \neq \emptyset \leftrightarrow \neg A = \emptyset$
7	6	anbi1i	$⊢ (A \neq \emptyset \land \neg Lim A) \leftrightarrow (\neg A = \emptyset \land \neg Lim A)$
8	5 7	xchbinxr	$⊢ (A = \emptyset \lor Lim A) \leftrightarrow \neg (A \neq \emptyset \land \neg Lim A)$
9	4 8	bitrdi	$⊢ Ord A \to (A = ⋃ A \leftrightarrow \neg (A \neq \emptyset \land \neg Lim A))$
10	3 9	syl	$⊢ A \in On \to (A = ⋃ A \leftrightarrow \neg (A \neq \emptyset \land \neg Lim A))$
11		pm2.21	$⊢ \neg (A \neq \emptyset \land \neg Lim A) \to ((A \neq \emptyset \land \neg Lim A) \to A = suc ⋃ A)$
12	10 11	biimtrdi	$⊢ A \in On \to (A = ⋃ A \to ((A \neq \emptyset \land \neg Lim A) \to A = suc ⋃ A))$
13	12	com23	$⊢ A \in On \to ((A \neq \emptyset \land \neg Lim A) \to (A = ⋃ A \to A = suc ⋃ A))$
14	13	3impib	$⊢ (A \in On \land A \neq \emptyset \land \neg Lim A) \to (A = ⋃ A \to A = suc ⋃ A)$
15		idd	$⊢ (A \in On \land A \neq \emptyset \land \neg Lim A) \to (A = suc ⋃ A \to A = suc ⋃ A)$
16		onuniorsuc	$⊢ A \in On \to (A = ⋃ A \lor A = suc ⋃ A)$
17	16	3ad2ant1	$⊢ (A \in On \land A \neq \emptyset \land \neg Lim A) \to (A = ⋃ A \lor A = suc ⋃ A)$
18	14 15 17	mpjaod	$⊢ (A \in On \land A \neq \emptyset \land \neg Lim A) \to A = suc ⋃ A$
19	2 18	jca	$⊢ (A \in On \land A \neq \emptyset \land \neg Lim A) \to (⋃ A \in On \land A = suc ⋃ A)$
20		eleq1	$⊢ b = ⋃ A \to (b \in On \leftrightarrow ⋃ A \in On)$
21		suceq	$⊢ b = ⋃ A \to suc b = suc ⋃ A$
22	21	eqeq2d	$⊢ b = ⋃ A \to (A = suc b \leftrightarrow A = suc ⋃ A)$
23	20 22	anbi12d	$⊢ b = ⋃ A \to ((b \in On \land A = suc b) \leftrightarrow (⋃ A \in On \land A = suc ⋃ A))$
24	2 19 23	spcedv	$⊢ (A \in On \land A \neq \emptyset \land \neg Lim A) \to \exists b (b \in On \land A = suc b)$
25		onsucf1lem	$⊢ A \in On \to \exists^{*} b \in On A = suc b$
26	25	3ad2ant1	$⊢ (A \in On \land A \neq \emptyset \land \neg Lim A) \to \exists^{*} b \in On A = suc b$
27		df-eu	$⊢ \exists! b (b \in On \land A = suc b) \leftrightarrow (\exists b (b \in On \land A = suc b) \land \exists^{*} b (b \in On \land A = suc b))$
28		df-reu	$⊢ \exists! b \in On A = suc b \leftrightarrow \exists! b (b \in On \land A = suc b)$
29		df-rmo	$⊢ \exists^{} b \in On A = suc b \leftrightarrow \exists^{} b (b \in On \land A = suc b)$
30	29	anbi2i	$⊢ (\exists b (b \in On \land A = suc b) \land \exists^{} b \in On A = suc b) \leftrightarrow (\exists b (b \in On \land A = suc b) \land \exists^{} b (b \in On \land A = suc b))$
31	27 28 30	3bitr4i	$⊢ \exists! b \in On A = suc b \leftrightarrow (\exists b (b \in On \land A = suc b) \land \exists^{*} b \in On A = suc b)$
32	24 26 31	sylanbrc	$⊢ (A \in On \land A \neq \emptyset \land \neg Lim A) \to \exists! b \in On A = suc b$

Metamath Proof Explorer

Theorem onsucf1olem

Proof