Metamath Proof Explorer


Theorem cfsetsnfsetf1

Description: The mapping of the class of singleton functions into the class of constant functions is an injection. (Contributed by AV, 14-Sep-2024)

Ref Expression
Hypotheses cfsetsnfsetfv.f F = f | f : A B b B z A f z = b
cfsetsnfsetfv.g G = x | x : Y B
cfsetsnfsetfv.h H = g G a A g Y
Assertion cfsetsnfsetf1 A V Y A H : G 1-1 F

Proof

Step Hyp Ref Expression
1 cfsetsnfsetfv.f F = f | f : A B b B z A f z = b
2 cfsetsnfsetfv.g G = x | x : Y B
3 cfsetsnfsetfv.h H = g G a A g Y
4 1 2 3 cfsetsnfsetf A V Y A H : G F
5 1 2 3 cfsetsnfsetfv A V m G H m = a A m Y
6 5 ad2ant2r A V Y A m G n G H m = a A m Y
7 1 2 3 cfsetsnfsetfv A V n G H n = a A n Y
8 7 ad2ant2rl A V Y A m G n G H n = a A n Y
9 6 8 eqeq12d A V Y A m G n G H m = H n a A m Y = a A n Y
10 fvexd A V Y A m G n G a A m Y V
11 10 ralrimiva A V Y A m G n G a A m Y V
12 mpteqb a A m Y V a A m Y = a A n Y a A m Y = n Y
13 11 12 syl A V Y A m G n G a A m Y = a A n Y a A m Y = n Y
14 simplr A V Y A m G n G Y A
15 idd A V Y A m G n G a = Y m Y = n Y m Y = n Y
16 14 15 rspcimdv A V Y A m G n G a A m Y = n Y m Y = n Y
17 vex m V
18 feq1 x = m x : Y B m : Y B
19 17 18 2 elab2 m G m : Y B
20 vex n V
21 feq1 x = n x : Y B n : Y B
22 20 21 2 elab2 n G n : Y B
23 19 22 anbi12i m G n G m : Y B n : Y B
24 simp3 A V Y A m : Y B n : Y B m Y = n Y m Y = n Y
25 simp1r A V Y A m : Y B n : Y B m Y = n Y Y A
26 fveq2 y = Y m y = m Y
27 fveq2 y = Y n y = n Y
28 26 27 eqeq12d y = Y m y = n y m Y = n Y
29 28 ralsng Y A y Y m y = n y m Y = n Y
30 25 29 syl A V Y A m : Y B n : Y B m Y = n Y y Y m y = n y m Y = n Y
31 24 30 mpbird A V Y A m : Y B n : Y B m Y = n Y y Y m y = n y
32 ffn m : Y B m Fn Y
33 ffn n : Y B n Fn Y
34 32 33 anim12i m : Y B n : Y B m Fn Y n Fn Y
35 34 3ad2ant2 A V Y A m : Y B n : Y B m Y = n Y m Fn Y n Fn Y
36 eqfnfv m Fn Y n Fn Y m = n y Y m y = n y
37 35 36 syl A V Y A m : Y B n : Y B m Y = n Y m = n y Y m y = n y
38 31 37 mpbird A V Y A m : Y B n : Y B m Y = n Y m = n
39 38 3exp A V Y A m : Y B n : Y B m Y = n Y m = n
40 23 39 syl5bi A V Y A m G n G m Y = n Y m = n
41 40 imp A V Y A m G n G m Y = n Y m = n
42 16 41 syld A V Y A m G n G a A m Y = n Y m = n
43 13 42 sylbid A V Y A m G n G a A m Y = a A n Y m = n
44 9 43 sylbid A V Y A m G n G H m = H n m = n
45 44 ralrimivva A V Y A m G n G H m = H n m = n
46 dff13 H : G 1-1 F H : G F m G n G H m = H n m = n
47 4 45 46 sylanbrc A V Y A H : G 1-1 F