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 ⊢ S = x ∈ On ⟼ suc ⁡ x
Assertion fin1a2lem2 ⊢ S : On ⟶ 1-1 On

Proof

Step Hyp Ref Expression
1 fin1a2lem.a ⊢ S = x ∈ On ⟼ suc ⁡ x
2 onsuc ⊢ x ∈ On → suc ⁡ x ∈ On
3 1 2 fmpti ⊢ S : On ⟶ On
4 1 fin1a2lem1 ⊢ a ∈ On → S ⁡ a = suc ⁡ a
5 1 fin1a2lem1 ⊢ b ∈ On → S ⁡ b = suc ⁡ b
6 4 5 eqeqan12d ⊢ a ∈ On ∧ b ∈ On → S ⁡ a = S ⁡ b ↔ suc ⁡ a = suc ⁡ b
7 suc11 ⊢ a ∈ On ∧ b ∈ On → suc ⁡ a = suc ⁡ b ↔ a = b
8 6 7 bitrd ⊢ a ∈ On ∧ b ∈ On → S ⁡ a = S ⁡ b ↔ a = b
9 8 biimpd ⊢ a ∈ On ∧ b ∈ On → S ⁡ a = S ⁡ b → a = b
10 9 rgen2 ⊢ ∀ a ∈ On ∀ b ∈ On S ⁡ a = S ⁡ b → a = b
11 dff13 ⊢ S : On ⟶ 1-1 On ↔ S : On ⟶ On ∧ ∀ a ∈ On ∀ b ∈ On S ⁡ a = S ⁡ b → a = b
12 3 10 11 mpbir2an ⊢ S : On ⟶ 1-1 On