Metamath Proof Explorer

Theorem onsucf1o

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

		Ref	Expression
	Hypothesis	onsucf1o.f	$⊢ F = (x \in On ⟼ suc x)$
	Assertion	onsucf1o	$⊢ F : On \underset{1-1 onto}{⟶} \{a \in On \| \exists b \in On a = suc b\}$

Proof

Step	Hyp	Ref	Expression
1		onsucf1o.f	$⊢ F = (x \in On ⟼ suc x)$
2	1	fin1a2lem2	$⊢ F : On \underset{1-1}{⟶} On$
3		f1fn	$⊢ F : On \underset{1-1}{⟶} On \to F Fn On$
4	2 3	ax-mp	$⊢ F Fn On$
5	1	onsucrn	$⊢ ran F = \{a \in On \| \exists b \in On a = suc b\}$
6	1	fin1a2lem1	$⊢ a \in On \to F (a) = suc a$
7	1	fin1a2lem1	$⊢ b \in On \to F (b) = suc b$
8	6 7	eqeqan12d	$⊢ (a \in On \land b \in On) \to (F (a) = F (b) \leftrightarrow suc a = suc b)$
9		suc11	$⊢ (a \in On \land b \in On) \to (suc a = suc b \leftrightarrow a = b)$
10	8 9	bitrd	$⊢ (a \in On \land b \in On) \to (F (a) = F (b) \leftrightarrow a = b)$
11	10	biimpd	$⊢ (a \in On \land b \in On) \to (F (a) = F (b) \to a = b)$
12	11	rgen2	$⊢ \forall a \in On \forall b \in On (F (a) = F (b) \to a = b)$
13		dff1o6	$⊢ F : On \underset{1-1 onto}{⟶} \{a \in On \| \exists b \in On a = suc b\} \leftrightarrow (F Fn On \land ran F = \{a \in On \| \exists b \in On a = suc b\} \land \forall a \in On \forall b \in On (F (a) = F (b) \to a = b))$
14	4 5 12 13	mpbir3an	$⊢ F : On \underset{1-1 onto}{⟶} \{a \in On \| \exists b \in On a = suc b\}$