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 syl6bi 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