Metamath Proof Explorer

Theorem fsetsnf1

Description: The mapping of an element of a class to a singleton function is an injection. (Contributed by AV, 13-Sep-2024)

Ref Expression
Hypotheses fsetsnf.a ⊢ A = y | ∃ b ∈ B y = S b
fsetsnf.f ⊢ F = x ∈ B ⟼ S x
Assertion fsetsnf1 ⊢ S ∈ V → F : B ⟶ 1-1 A

Proof

Step Hyp Ref Expression
1 fsetsnf.a ⊢ A = y | ∃ b ∈ B y = S b
2 fsetsnf.f ⊢ F = x ∈ B ⟼ S x
3 1 2 fsetsnf ⊢ S ∈ V → F : B ⟶ A
4 2 a1i ⊢ m ∈ B ∧ n ∈ B → F = x ∈ B ⟼ S x
5 opeq2 ⊢ x = m → S x = S m
6 5 sneqd ⊢ x = m → S x = S m
7 6 adantl ⊢ m ∈ B ∧ n ∈ B ∧ x = m → S x = S m
8 simpl ⊢ m ∈ B ∧ n ∈ B → m ∈ B
9 snex ⊢ S m ∈ V
10 9 a1i ⊢ m ∈ B ∧ n ∈ B → S m ∈ V
11 4 7 8 10 fvmptd ⊢ m ∈ B ∧ n ∈ B → F ⁡ m = S m
12 opeq2 ⊢ x = n → S x = S n
13 12 sneqd ⊢ x = n → S x = S n
14 13 adantl ⊢ m ∈ B ∧ n ∈ B ∧ x = n → S x = S n
15 simpr ⊢ m ∈ B ∧ n ∈ B → n ∈ B
16 snex ⊢ S n ∈ V
17 16 a1i ⊢ m ∈ B ∧ n ∈ B → S n ∈ V
18 4 14 15 17 fvmptd ⊢ m ∈ B ∧ n ∈ B → F ⁡ n = S n
19 11 18 eqeq12d ⊢ m ∈ B ∧ n ∈ B → F ⁡ m = F ⁡ n ↔ S m = S n
20 19 adantl ⊢ S ∈ V ∧ m ∈ B ∧ n ∈ B → F ⁡ m = F ⁡ n ↔ S m = S n
21 opex ⊢ S m ∈ V
22 21 sneqr ⊢ S m = S n → S m = S n
23 opthg ⊢ S ∈ V ∧ m ∈ B → S m = S n ↔ S = S ∧ m = n
24 23 adantrr ⊢ S ∈ V ∧ m ∈ B ∧ n ∈ B → S m = S n ↔ S = S ∧ m = n
25 simpr ⊢ S = S ∧ m = n → m = n
26 24 25 biimtrdi ⊢ S ∈ V ∧ m ∈ B ∧ n ∈ B → S m = S n → m = n
27 22 26 syl5 ⊢ S ∈ V ∧ m ∈ B ∧ n ∈ B → S m = S n → m = n
28 20 27 sylbid ⊢ S ∈ V ∧ m ∈ B ∧ n ∈ B → F ⁡ m = F ⁡ n → m = n
29 28 ralrimivva ⊢ S ∈ V → ∀ m ∈ B ∀ n ∈ B F ⁡ m = F ⁡ n → m = n
30 dff13 ⊢ F : B ⟶ 1-1 A ↔ F : B ⟶ A ∧ ∀ m ∈ B ∀ n ∈ B F ⁡ m = F ⁡ n → m = n
31 3 29 30 sylanbrc ⊢ S ∈ V → F : B ⟶ 1-1 A