Metamath Proof Explorer

Theorem fin1a2lem2

Description: Lemma for fin1a2 . (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 suceloni ⊢ 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