Metamath Proof Explorer

Theorem fin1a2lem2

Description: Lemma for fin1a2 . The successor operation on the ordinal numbers is injective or one-to-one. Lemma 1.17 of Schloeder p. 2. (Contributed by Stefan O'Rear, 7-Nov-2014)

		Ref	Expression
	Hypothesis	fin1a2lem.a	$⊢ S = (x \in On ⟼ suc x)$
	Assertion	fin1a2lem2	$⊢ S : On \underset{1-1}{⟶} On$

Proof

Step	Hyp	Ref	Expression
1		fin1a2lem.a	$⊢ S = (x \in On ⟼ suc x)$
2		onsuc	$⊢ x \in On \to suc x \in On$
3	1 2	fmpti	$⊢ S : On ⟶ On$
4	1	fin1a2lem1	$⊢ a \in On \to S (a) = suc a$
5	1	fin1a2lem1	$⊢ b \in On \to S (b) = suc b$
6	4 5	eqeqan12d	$⊢ (a \in On \land b \in On) \to (S (a) = S (b) \leftrightarrow suc a = suc b)$
7		suc11	$⊢ (a \in On \land b \in On) \to (suc a = suc b \leftrightarrow a = b)$
8	6 7	bitrd	$⊢ (a \in On \land b \in On) \to (S (a) = S (b) \leftrightarrow a = b)$
9	8	biimpd	$⊢ (a \in On \land b \in On) \to (S (a) = S (b) \to a = b)$
10	9	rgen2	$⊢ \forall a \in On \forall b \in On (S (a) = S (b) \to a = b)$
11		dff13	$⊢ S : On \underset{1-1}{⟶} On \leftrightarrow (S : On ⟶ On \land \forall a \in On \forall b \in On (S (a) = S (b) \to a = b))$
12	3 10 11	mpbir2an	$⊢ S : On \underset{1-1}{⟶} On$