This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑆 = ( 𝑥 ∈ 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