onsucf1lem

Description: For ordinals, the successor operation is injective, so there is at most one ordinal that a given ordinal could be the succesor of. Lemma 1.17 of Schloeder p. 2. (Contributed by RP, 18-Jan-2025)

		Ref	Expression
	Assertion	onsucf1lem	$⊢ A \in On \to \exists^{*} b \in On A = suc b$

Proof

Step	Hyp	Ref	Expression
1		onuni	$⊢ A \in On \to ⋃ A \in On$
2		onsucuni2	$⊢ (A \in On \land A = suc b) \to suc ⋃ A = A$
3	2	adantlr	$⊢ ((A \in On \land b \in On) \land A = suc b) \to suc ⋃ A = A$
4		simpr	$⊢ ((A \in On \land b \in On) \land A = suc b) \to A = suc b$
5	3 4	eqtr2d	$⊢ ((A \in On \land b \in On) \land A = suc b) \to suc b = suc ⋃ A$
6	1	anim1i	$⊢ (A \in On \land b \in On) \to (⋃ A \in On \land b \in On)$
7	6	adantr	$⊢ ((A \in On \land b \in On) \land A = suc b) \to (⋃ A \in On \land b \in On)$
8	7	ancomd	$⊢ ((A \in On \land b \in On) \land A = suc b) \to (b \in On \land ⋃ A \in On)$
9		suc11	$⊢ (b \in On \land ⋃ A \in On) \to (suc b = suc ⋃ A \leftrightarrow b = ⋃ A)$
10	8 9	syl	$⊢ ((A \in On \land b \in On) \land A = suc b) \to (suc b = suc ⋃ A \leftrightarrow b = ⋃ A)$
11	5 10	mpbid	$⊢ ((A \in On \land b \in On) \land A = suc b) \to b = ⋃ A$
12	11	ex	$⊢ (A \in On \land b \in On) \to (A = suc b \to b = ⋃ A)$
13	12	ralrimiva	$⊢ A \in On \to \forall b \in On (A = suc b \to b = ⋃ A)$
14		eqeq2	$⊢ c = ⋃ A \to (b = c \leftrightarrow b = ⋃ A)$
15	14	imbi2d	$⊢ c = ⋃ A \to ((A = suc b \to b = c) \leftrightarrow (A = suc b \to b = ⋃ A))$
16	15	ralbidv	$⊢ c = ⋃ A \to (\forall b \in On (A = suc b \to b = c) \leftrightarrow \forall b \in On (A = suc b \to b = ⋃ A))$
17	1 13 16	spcedv	$⊢ A \in On \to \exists c \forall b \in On (A = suc b \to b = c)$
18		nfv	$⊢ Ⅎ c A = suc b$
19	18	rmo2	$⊢ \exists^{*} b \in On A = suc b \leftrightarrow \exists c \forall b \in On (A = suc b \to b = c)$
20	17 19	sylibr	$⊢ A \in On \to \exists^{*} b \in On A = suc b$

Metamath Proof Explorer

Theorem onsucf1lem

Proof