Metamath Proof Explorer

Theorem cfsetsnfsetfo

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

Ref Expression
Hypotheses cfsetsnfsetfv.f ⊢ 𝐹 = { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) }
cfsetsnfsetfv.g ⊢ 𝐺 = { 𝑥 ∣ 𝑥 : { 𝑌 } ⟶ 𝐵 }
cfsetsnfsetfv.h ⊢ 𝐻 = ( 𝑔 ∈ 𝐺 ↦ ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) )
Assertion cfsetsnfsetfo ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → 𝐻 : 𝐺 –onto→ 𝐹 )

Proof

Step Hyp Ref Expression
1 cfsetsnfsetfv.f ⊢ 𝐹 = { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) }
2 cfsetsnfsetfv.g ⊢ 𝐺 = { 𝑥 ∣ 𝑥 : { 𝑌 } ⟶ 𝐵 }
3 cfsetsnfsetfv.h ⊢ 𝐻 = ( 𝑔 ∈ 𝐺 ↦ ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) )
4 1 2 3 cfsetsnfsetf ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → 𝐻 : 𝐺 ⟶ 𝐹 )
5 vex ⊢ 𝑚 ∈ V
6 feq1 ⊢ ( 𝑓 = 𝑚 → ( 𝑓 : 𝐴 ⟶ 𝐵 ↔ 𝑚 : 𝐴 ⟶ 𝐵 ) )
7 fveq1 ⊢ ( 𝑓 = 𝑚 → ( 𝑓 ‘ 𝑧 ) = ( 𝑚 ‘ 𝑧 ) )
8 7 adantr ⊢ ( ( 𝑓 = 𝑚 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑧 ) = ( 𝑚 ‘ 𝑧 ) )
9 8 eqeq1d ⊢ ( ( 𝑓 = 𝑚 ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑓 ‘ 𝑧 ) = 𝑏 ↔ ( 𝑚 ‘ 𝑧 ) = 𝑏 ) )
10 9 ralbidva ⊢ ( 𝑓 = 𝑚 → ( ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ‘ 𝑧 ) = 𝑏 ) )
11 10 rexbidv ⊢ ( 𝑓 = 𝑚 → ( ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ↔ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑚 ‘ 𝑧 ) = 𝑏 ) )
12 6 11 anbi12d ⊢ ( 𝑓 = 𝑚 → ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) ↔ ( 𝑚 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑚 ‘ 𝑧 ) = 𝑏 ) ) )
13 5 12 1 elab2 ⊢ ( 𝑚 ∈ 𝐹 ↔ ( 𝑚 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑚 ‘ 𝑧 ) = 𝑏 ) )
14 simpllr ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ‘ 𝑧 ) = 𝑏 ) ∧ 𝑦 ∈ { 𝑌 } ) → 𝑏 ∈ 𝐵 )
15 eqid ⊢ ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) = ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 )
16 14 15 fmptd ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ‘ 𝑧 ) = 𝑏 ) → ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) : { 𝑌 } ⟶ 𝐵 )
17 snex ⊢ { 𝑌 } ∈ V
18 17 mptex ⊢ ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) ∈ V
19 feq1 ⊢ ( 𝑥 = ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) → ( 𝑥 : { 𝑌 } ⟶ 𝐵 ↔ ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) : { 𝑌 } ⟶ 𝐵 ) )
20 18 19 2 elab2 ⊢ ( ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) ∈ 𝐺 ↔ ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) : { 𝑌 } ⟶ 𝐵 )
21 16 20 sylibr ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ‘ 𝑧 ) = 𝑏 ) → ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) ∈ 𝐺 )
22 fveq1 ⊢ ( 𝑛 = ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) → ( 𝑛 ‘ 𝑌 ) = ( ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) ‘ 𝑌 ) )
23 22 mpteq2dv ⊢ ( 𝑛 = ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) → ( 𝑎 ∈ 𝐴 ↦ ( 𝑛 ‘ 𝑌 ) ) = ( 𝑎 ∈ 𝐴 ↦ ( ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) ‘ 𝑌 ) ) )
24 23 eqeq2d ⊢ ( 𝑛 = ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) → ( 𝑚 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑛 ‘ 𝑌 ) ) ↔ 𝑚 = ( 𝑎 ∈ 𝐴 ↦ ( ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) ‘ 𝑌 ) ) ) )
25 24 adantl ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ‘ 𝑧 ) = 𝑏 ) ∧ 𝑛 = ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) ) → ( 𝑚 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑛 ‘ 𝑌 ) ) ↔ 𝑚 = ( 𝑎 ∈ 𝐴 ↦ ( ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) ‘ 𝑌 ) ) ) )
26 simpr ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑚 ‘ 𝑧 ) = 𝑏 ) → ( 𝑚 ‘ 𝑧 ) = 𝑏 )
27 eqidd ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑚 ‘ 𝑧 ) = 𝑏 ) → ( 𝑎 ∈ 𝐴 ↦ ( ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) ‘ 𝑌 ) ) = ( 𝑎 ∈ 𝐴 ↦ ( ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) ‘ 𝑌 ) ) )
28 eqidd ⊢ ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑚 ‘ 𝑧 ) = 𝑏 ) ∧ 𝑎 = 𝑧 ) → ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) = ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) )
29 eqidd ⊢ ( ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑚 ‘ 𝑧 ) = 𝑏 ) ∧ 𝑎 = 𝑧 ) ∧ 𝑦 = 𝑌 ) → 𝑏 = 𝑏 )
30 snidg ⊢ ( 𝑌 ∈ 𝐴 → 𝑌 ∈ { 𝑌 } )
31 30 ad6antlr ⊢ ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑚 ‘ 𝑧 ) = 𝑏 ) ∧ 𝑎 = 𝑧 ) → 𝑌 ∈ { 𝑌 } )
32 simpllr ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑚 ‘ 𝑧 ) = 𝑏 ) → 𝑏 ∈ 𝐵 )
33 32 adantr ⊢ ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑚 ‘ 𝑧 ) = 𝑏 ) ∧ 𝑎 = 𝑧 ) → 𝑏 ∈ 𝐵 )
34 28 29 31 33 fvmptd ⊢ ( ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑚 ‘ 𝑧 ) = 𝑏 ) ∧ 𝑎 = 𝑧 ) → ( ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) ‘ 𝑌 ) = 𝑏 )
35 simpr ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 )
36 35 adantr ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑚 ‘ 𝑧 ) = 𝑏 ) → 𝑧 ∈ 𝐴 )
37 27 34 36 32 fvmptd ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑚 ‘ 𝑧 ) = 𝑏 ) → ( ( 𝑎 ∈ 𝐴 ↦ ( ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) ‘ 𝑌 ) ) ‘ 𝑧 ) = 𝑏 )
38 26 37 eqtr4d ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑚 ‘ 𝑧 ) = 𝑏 ) → ( 𝑚 ‘ 𝑧 ) = ( ( 𝑎 ∈ 𝐴 ↦ ( ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) ‘ 𝑌 ) ) ‘ 𝑧 ) )
39 38 ex ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑚 ‘ 𝑧 ) = 𝑏 → ( 𝑚 ‘ 𝑧 ) = ( ( 𝑎 ∈ 𝐴 ↦ ( ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) ‘ 𝑌 ) ) ‘ 𝑧 ) ) )
40 39 ralimdva ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ( ∀ 𝑧 ∈ 𝐴 ( 𝑚 ‘ 𝑧 ) = 𝑏 → ∀ 𝑧 ∈ 𝐴 ( 𝑚 ‘ 𝑧 ) = ( ( 𝑎 ∈ 𝐴 ↦ ( ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) ‘ 𝑌 ) ) ‘ 𝑧 ) ) )
41 40 imp ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ‘ 𝑧 ) = 𝑏 ) → ∀ 𝑧 ∈ 𝐴 ( 𝑚 ‘ 𝑧 ) = ( ( 𝑎 ∈ 𝐴 ↦ ( ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) ‘ 𝑌 ) ) ‘ 𝑧 ) )
42 ffn ⊢ ( 𝑚 : 𝐴 ⟶ 𝐵 → 𝑚 Fn 𝐴 )
43 42 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) → 𝑚 Fn 𝐴 )
44 nfv ⊢ Ⅎ 𝑎 ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 )
45 fvexd ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) ‘ 𝑌 ) ∈ V )
46 eqid ⊢ ( 𝑎 ∈ 𝐴 ↦ ( ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) ‘ 𝑌 ) ) = ( 𝑎 ∈ 𝐴 ↦ ( ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) ‘ 𝑌 ) )
47 44 45 46 fnmptd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) → ( 𝑎 ∈ 𝐴 ↦ ( ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) ‘ 𝑌 ) ) Fn 𝐴 )
48 43 47 jca ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) → ( 𝑚 Fn 𝐴 ∧ ( 𝑎 ∈ 𝐴 ↦ ( ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) ‘ 𝑌 ) ) Fn 𝐴 ) )
49 48 adantr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝑚 Fn 𝐴 ∧ ( 𝑎 ∈ 𝐴 ↦ ( ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) ‘ 𝑌 ) ) Fn 𝐴 ) )
50 49 adantr ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ‘ 𝑧 ) = 𝑏 ) → ( 𝑚 Fn 𝐴 ∧ ( 𝑎 ∈ 𝐴 ↦ ( ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) ‘ 𝑌 ) ) Fn 𝐴 ) )
51 eqfnfv ⊢ ( ( 𝑚 Fn 𝐴 ∧ ( 𝑎 ∈ 𝐴 ↦ ( ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) ‘ 𝑌 ) ) Fn 𝐴 ) → ( 𝑚 = ( 𝑎 ∈ 𝐴 ↦ ( ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) ‘ 𝑌 ) ) ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ‘ 𝑧 ) = ( ( 𝑎 ∈ 𝐴 ↦ ( ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) ‘ 𝑌 ) ) ‘ 𝑧 ) ) )
52 50 51 syl ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ‘ 𝑧 ) = 𝑏 ) → ( 𝑚 = ( 𝑎 ∈ 𝐴 ↦ ( ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) ‘ 𝑌 ) ) ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ‘ 𝑧 ) = ( ( 𝑎 ∈ 𝐴 ↦ ( ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) ‘ 𝑌 ) ) ‘ 𝑧 ) ) )
53 41 52 mpbird ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ‘ 𝑧 ) = 𝑏 ) → 𝑚 = ( 𝑎 ∈ 𝐴 ↦ ( ( 𝑦 ∈ { 𝑌 } ↦ 𝑏 ) ‘ 𝑌 ) ) )
54 21 25 53 rspcedvd ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ‘ 𝑧 ) = 𝑏 ) → ∃ 𝑛 ∈ 𝐺 𝑚 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑛 ‘ 𝑌 ) ) )
55 simp-4l ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ‘ 𝑧 ) = 𝑏 ) → 𝐴 ∈ 𝑉 )
56 1 2 3 cfsetsnfsetfv ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑛 ∈ 𝐺 ) → ( 𝐻 ‘ 𝑛 ) = ( 𝑎 ∈ 𝐴 ↦ ( 𝑛 ‘ 𝑌 ) ) )
57 55 56 sylan ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ‘ 𝑧 ) = 𝑏 ) ∧ 𝑛 ∈ 𝐺 ) → ( 𝐻 ‘ 𝑛 ) = ( 𝑎 ∈ 𝐴 ↦ ( 𝑛 ‘ 𝑌 ) ) )
58 57 eqeq2d ⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ‘ 𝑧 ) = 𝑏 ) ∧ 𝑛 ∈ 𝐺 ) → ( 𝑚 = ( 𝐻 ‘ 𝑛 ) ↔ 𝑚 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑛 ‘ 𝑌 ) ) ) )
59 58 rexbidva ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ‘ 𝑧 ) = 𝑏 ) → ( ∃ 𝑛 ∈ 𝐺 𝑚 = ( 𝐻 ‘ 𝑛 ) ↔ ∃ 𝑛 ∈ 𝐺 𝑚 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑛 ‘ 𝑌 ) ) ) )
60 54 59 mpbird ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑚 ‘ 𝑧 ) = 𝑏 ) → ∃ 𝑛 ∈ 𝐺 𝑚 = ( 𝐻 ‘ 𝑛 ) )
61 60 ex ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ( ∀ 𝑧 ∈ 𝐴 ( 𝑚 ‘ 𝑧 ) = 𝑏 → ∃ 𝑛 ∈ 𝐺 𝑚 = ( 𝐻 ‘ 𝑛 ) ) )
62 61 rexlimdva ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) → ( ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑚 ‘ 𝑧 ) = 𝑏 → ∃ 𝑛 ∈ 𝐺 𝑚 = ( 𝐻 ‘ 𝑛 ) ) )
63 62 expimpd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ( ( 𝑚 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑚 ‘ 𝑧 ) = 𝑏 ) → ∃ 𝑛 ∈ 𝐺 𝑚 = ( 𝐻 ‘ 𝑛 ) ) )
64 13 63 syl5bi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑚 ∈ 𝐹 → ∃ 𝑛 ∈ 𝐺 𝑚 = ( 𝐻 ‘ 𝑛 ) ) )
65 64 ralrimiv ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ∀ 𝑚 ∈ 𝐹 ∃ 𝑛 ∈ 𝐺 𝑚 = ( 𝐻 ‘ 𝑛 ) )
66 dffo3 ⊢ ( 𝐻 : 𝐺 –onto→ 𝐹 ↔ ( 𝐻 : 𝐺 ⟶ 𝐹 ∧ ∀ 𝑚 ∈ 𝐹 ∃ 𝑛 ∈ 𝐺 𝑚 = ( 𝐻 ‘ 𝑛 ) ) )
67 4 65 66 sylanbrc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → 𝐻 : 𝐺 –onto→ 𝐹 )