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	⊢ 𝑆 = ( 𝑥 ∈ On ↦ suc 𝑥 )
Assertion	fin1a2lem2	⊢ 𝑆 : On –1-1→ On

Proof

Step	Hyp	Ref	Expression
1		fin1a2lem.a	⊢ 𝑆 = ( 𝑥 ∈ On ↦ suc 𝑥 )
2		onsuc	⊢ ( 𝑥 ∈ On → suc 𝑥 ∈ On )
3	1 2	fmpti	⊢ 𝑆 : On ⟶ On
4	1	fin1a2lem1	⊢ ( 𝑎 ∈ On → ( 𝑆 ‘ 𝑎 ) = suc 𝑎 )
5	1	fin1a2lem1	⊢ ( 𝑏 ∈ On → ( 𝑆 ‘ 𝑏 ) = suc 𝑏 )
6	4 5	eqeqan12d	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) ↔ suc 𝑎 = suc 𝑏 ) )
7		suc11	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( suc 𝑎 = suc 𝑏 ↔ 𝑎 = 𝑏 ) )
8	6 7	bitrd	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) ↔ 𝑎 = 𝑏 ) )
9	8	biimpd	⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ On ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → 𝑎 = 𝑏 ) )
10	9	rgen2	⊢ ∀ 𝑎 ∈ On ∀ 𝑏 ∈ On ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → 𝑎 = 𝑏 )
11		dff13	⊢ ( 𝑆 : On –1-1→ On ↔ ( 𝑆 : On ⟶ On ∧ ∀ 𝑎 ∈ On ∀ 𝑏 ∈ On ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → 𝑎 = 𝑏 ) ) )
12	3 10 11	mpbir2an	⊢ 𝑆 : On –1-1→ On