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 𝐹 = { 𝑓 ∣ ( 𝑓 : 𝐴𝐵 ∧ ∃ 𝑏𝐵𝑧𝐴 ( 𝑓𝑧 ) = 𝑏 ) }
cfsetsnfsetfv.g 𝐺 = { 𝑥𝑥 : { 𝑌 } ⟶ 𝐵 }
cfsetsnfsetfv.h 𝐻 = ( 𝑔𝐺 ↦ ( 𝑎𝐴 ↦ ( 𝑔𝑌 ) ) )
Assertion cfsetsnfsetf1 ( ( 𝐴𝑉𝑌𝐴 ) → 𝐻 : 𝐺1-1𝐹 )

Proof

Step Hyp Ref Expression
1 cfsetsnfsetfv.f 𝐹 = { 𝑓 ∣ ( 𝑓 : 𝐴𝐵 ∧ ∃ 𝑏𝐵𝑧𝐴 ( 𝑓𝑧 ) = 𝑏 ) }
2 cfsetsnfsetfv.g 𝐺 = { 𝑥𝑥 : { 𝑌 } ⟶ 𝐵 }
3 cfsetsnfsetfv.h 𝐻 = ( 𝑔𝐺 ↦ ( 𝑎𝐴 ↦ ( 𝑔𝑌 ) ) )
4 1 2 3 cfsetsnfsetf ( ( 𝐴𝑉𝑌𝐴 ) → 𝐻 : 𝐺𝐹 )
5 1 2 3 cfsetsnfsetfv ( ( 𝐴𝑉𝑚𝐺 ) → ( 𝐻𝑚 ) = ( 𝑎𝐴 ↦ ( 𝑚𝑌 ) ) )
6 5 ad2ant2r ( ( ( 𝐴𝑉𝑌𝐴 ) ∧ ( 𝑚𝐺𝑛𝐺 ) ) → ( 𝐻𝑚 ) = ( 𝑎𝐴 ↦ ( 𝑚𝑌 ) ) )
7 1 2 3 cfsetsnfsetfv ( ( 𝐴𝑉𝑛𝐺 ) → ( 𝐻𝑛 ) = ( 𝑎𝐴 ↦ ( 𝑛𝑌 ) ) )
8 7 ad2ant2rl ( ( ( 𝐴𝑉𝑌𝐴 ) ∧ ( 𝑚𝐺𝑛𝐺 ) ) → ( 𝐻𝑛 ) = ( 𝑎𝐴 ↦ ( 𝑛𝑌 ) ) )
9 6 8 eqeq12d ( ( ( 𝐴𝑉𝑌𝐴 ) ∧ ( 𝑚𝐺𝑛𝐺 ) ) → ( ( 𝐻𝑚 ) = ( 𝐻𝑛 ) ↔ ( 𝑎𝐴 ↦ ( 𝑚𝑌 ) ) = ( 𝑎𝐴 ↦ ( 𝑛𝑌 ) ) ) )
10 fvexd ( ( ( ( 𝐴𝑉𝑌𝐴 ) ∧ ( 𝑚𝐺𝑛𝐺 ) ) ∧ 𝑎𝐴 ) → ( 𝑚𝑌 ) ∈ V )
11 10 ralrimiva ( ( ( 𝐴𝑉𝑌𝐴 ) ∧ ( 𝑚𝐺𝑛𝐺 ) ) → ∀ 𝑎𝐴 ( 𝑚𝑌 ) ∈ V )
12 mpteqb ( ∀ 𝑎𝐴 ( 𝑚𝑌 ) ∈ V → ( ( 𝑎𝐴 ↦ ( 𝑚𝑌 ) ) = ( 𝑎𝐴 ↦ ( 𝑛𝑌 ) ) ↔ ∀ 𝑎𝐴 ( 𝑚𝑌 ) = ( 𝑛𝑌 ) ) )
13 11 12 syl ( ( ( 𝐴𝑉𝑌𝐴 ) ∧ ( 𝑚𝐺𝑛𝐺 ) ) → ( ( 𝑎𝐴 ↦ ( 𝑚𝑌 ) ) = ( 𝑎𝐴 ↦ ( 𝑛𝑌 ) ) ↔ ∀ 𝑎𝐴 ( 𝑚𝑌 ) = ( 𝑛𝑌 ) ) )
14 simplr ( ( ( 𝐴𝑉𝑌𝐴 ) ∧ ( 𝑚𝐺𝑛𝐺 ) ) → 𝑌𝐴 )
15 idd ( ( ( ( 𝐴𝑉𝑌𝐴 ) ∧ ( 𝑚𝐺𝑛𝐺 ) ) ∧ 𝑎 = 𝑌 ) → ( ( 𝑚𝑌 ) = ( 𝑛𝑌 ) → ( 𝑚𝑌 ) = ( 𝑛𝑌 ) ) )
16 14 15 rspcimdv ( ( ( 𝐴𝑉𝑌𝐴 ) ∧ ( 𝑚𝐺𝑛𝐺 ) ) → ( ∀ 𝑎𝐴 ( 𝑚𝑌 ) = ( 𝑛𝑌 ) → ( 𝑚𝑌 ) = ( 𝑛𝑌 ) ) )
17 vex 𝑚 ∈ V
18 feq1 ( 𝑥 = 𝑚 → ( 𝑥 : { 𝑌 } ⟶ 𝐵𝑚 : { 𝑌 } ⟶ 𝐵 ) )
19 17 18 2 elab2 ( 𝑚𝐺𝑚 : { 𝑌 } ⟶ 𝐵 )
20 vex 𝑛 ∈ V
21 feq1 ( 𝑥 = 𝑛 → ( 𝑥 : { 𝑌 } ⟶ 𝐵𝑛 : { 𝑌 } ⟶ 𝐵 ) )
22 20 21 2 elab2 ( 𝑛𝐺𝑛 : { 𝑌 } ⟶ 𝐵 )
23 19 22 anbi12i ( ( 𝑚𝐺𝑛𝐺 ) ↔ ( 𝑚 : { 𝑌 } ⟶ 𝐵𝑛 : { 𝑌 } ⟶ 𝐵 ) )
24 simp3 ( ( ( 𝐴𝑉𝑌𝐴 ) ∧ ( 𝑚 : { 𝑌 } ⟶ 𝐵𝑛 : { 𝑌 } ⟶ 𝐵 ) ∧ ( 𝑚𝑌 ) = ( 𝑛𝑌 ) ) → ( 𝑚𝑌 ) = ( 𝑛𝑌 ) )
25 simp1r ( ( ( 𝐴𝑉𝑌𝐴 ) ∧ ( 𝑚 : { 𝑌 } ⟶ 𝐵𝑛 : { 𝑌 } ⟶ 𝐵 ) ∧ ( 𝑚𝑌 ) = ( 𝑛𝑌 ) ) → 𝑌𝐴 )
26 fveq2 ( 𝑦 = 𝑌 → ( 𝑚𝑦 ) = ( 𝑚𝑌 ) )
27 fveq2 ( 𝑦 = 𝑌 → ( 𝑛𝑦 ) = ( 𝑛𝑌 ) )
28 26 27 eqeq12d ( 𝑦 = 𝑌 → ( ( 𝑚𝑦 ) = ( 𝑛𝑦 ) ↔ ( 𝑚𝑌 ) = ( 𝑛𝑌 ) ) )
29 28 ralsng ( 𝑌𝐴 → ( ∀ 𝑦 ∈ { 𝑌 } ( 𝑚𝑦 ) = ( 𝑛𝑦 ) ↔ ( 𝑚𝑌 ) = ( 𝑛𝑌 ) ) )
30 25 29 syl ( ( ( 𝐴𝑉𝑌𝐴 ) ∧ ( 𝑚 : { 𝑌 } ⟶ 𝐵𝑛 : { 𝑌 } ⟶ 𝐵 ) ∧ ( 𝑚𝑌 ) = ( 𝑛𝑌 ) ) → ( ∀ 𝑦 ∈ { 𝑌 } ( 𝑚𝑦 ) = ( 𝑛𝑦 ) ↔ ( 𝑚𝑌 ) = ( 𝑛𝑌 ) ) )
31 24 30 mpbird ( ( ( 𝐴𝑉𝑌𝐴 ) ∧ ( 𝑚 : { 𝑌 } ⟶ 𝐵𝑛 : { 𝑌 } ⟶ 𝐵 ) ∧ ( 𝑚𝑌 ) = ( 𝑛𝑌 ) ) → ∀ 𝑦 ∈ { 𝑌 } ( 𝑚𝑦 ) = ( 𝑛𝑦 ) )
32 ffn ( 𝑚 : { 𝑌 } ⟶ 𝐵𝑚 Fn { 𝑌 } )
33 ffn ( 𝑛 : { 𝑌 } ⟶ 𝐵𝑛 Fn { 𝑌 } )
34 32 33 anim12i ( ( 𝑚 : { 𝑌 } ⟶ 𝐵𝑛 : { 𝑌 } ⟶ 𝐵 ) → ( 𝑚 Fn { 𝑌 } ∧ 𝑛 Fn { 𝑌 } ) )
35 34 3ad2ant2 ( ( ( 𝐴𝑉𝑌𝐴 ) ∧ ( 𝑚 : { 𝑌 } ⟶ 𝐵𝑛 : { 𝑌 } ⟶ 𝐵 ) ∧ ( 𝑚𝑌 ) = ( 𝑛𝑌 ) ) → ( 𝑚 Fn { 𝑌 } ∧ 𝑛 Fn { 𝑌 } ) )
36 eqfnfv ( ( 𝑚 Fn { 𝑌 } ∧ 𝑛 Fn { 𝑌 } ) → ( 𝑚 = 𝑛 ↔ ∀ 𝑦 ∈ { 𝑌 } ( 𝑚𝑦 ) = ( 𝑛𝑦 ) ) )
37 35 36 syl ( ( ( 𝐴𝑉𝑌𝐴 ) ∧ ( 𝑚 : { 𝑌 } ⟶ 𝐵𝑛 : { 𝑌 } ⟶ 𝐵 ) ∧ ( 𝑚𝑌 ) = ( 𝑛𝑌 ) ) → ( 𝑚 = 𝑛 ↔ ∀ 𝑦 ∈ { 𝑌 } ( 𝑚𝑦 ) = ( 𝑛𝑦 ) ) )
38 31 37 mpbird ( ( ( 𝐴𝑉𝑌𝐴 ) ∧ ( 𝑚 : { 𝑌 } ⟶ 𝐵𝑛 : { 𝑌 } ⟶ 𝐵 ) ∧ ( 𝑚𝑌 ) = ( 𝑛𝑌 ) ) → 𝑚 = 𝑛 )
39 38 3exp ( ( 𝐴𝑉𝑌𝐴 ) → ( ( 𝑚 : { 𝑌 } ⟶ 𝐵𝑛 : { 𝑌 } ⟶ 𝐵 ) → ( ( 𝑚𝑌 ) = ( 𝑛𝑌 ) → 𝑚 = 𝑛 ) ) )
40 23 39 syl5bi ( ( 𝐴𝑉𝑌𝐴 ) → ( ( 𝑚𝐺𝑛𝐺 ) → ( ( 𝑚𝑌 ) = ( 𝑛𝑌 ) → 𝑚 = 𝑛 ) ) )
41 40 imp ( ( ( 𝐴𝑉𝑌𝐴 ) ∧ ( 𝑚𝐺𝑛𝐺 ) ) → ( ( 𝑚𝑌 ) = ( 𝑛𝑌 ) → 𝑚 = 𝑛 ) )
42 16 41 syld ( ( ( 𝐴𝑉𝑌𝐴 ) ∧ ( 𝑚𝐺𝑛𝐺 ) ) → ( ∀ 𝑎𝐴 ( 𝑚𝑌 ) = ( 𝑛𝑌 ) → 𝑚 = 𝑛 ) )
43 13 42 sylbid ( ( ( 𝐴𝑉𝑌𝐴 ) ∧ ( 𝑚𝐺𝑛𝐺 ) ) → ( ( 𝑎𝐴 ↦ ( 𝑚𝑌 ) ) = ( 𝑎𝐴 ↦ ( 𝑛𝑌 ) ) → 𝑚 = 𝑛 ) )
44 9 43 sylbid ( ( ( 𝐴𝑉𝑌𝐴 ) ∧ ( 𝑚𝐺𝑛𝐺 ) ) → ( ( 𝐻𝑚 ) = ( 𝐻𝑛 ) → 𝑚 = 𝑛 ) )
45 44 ralrimivva ( ( 𝐴𝑉𝑌𝐴 ) → ∀ 𝑚𝐺𝑛𝐺 ( ( 𝐻𝑚 ) = ( 𝐻𝑛 ) → 𝑚 = 𝑛 ) )
46 dff13 ( 𝐻 : 𝐺1-1𝐹 ↔ ( 𝐻 : 𝐺𝐹 ∧ ∀ 𝑚𝐺𝑛𝐺 ( ( 𝐻𝑚 ) = ( 𝐻𝑛 ) → 𝑚 = 𝑛 ) ) )
47 4 45 46 sylanbrc ( ( 𝐴𝑉𝑌𝐴 ) → 𝐻 : 𝐺1-1𝐹 )