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 biimtrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ( ( 𝑚 ∈ 𝐺 ∧ 𝑛 ∈ 𝐺 ) → ( ( 𝑚 ‘ 𝑌 ) = ( 𝑛 ‘ 𝑌 ) → 𝑚 = 𝑛 ) ) )
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→ 𝐹 )