Theorem cfsetsnfsetf

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

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

Proof

Step	Hyp	Ref	Expression
1		cfsetsnfsetfv.f	⊢ 𝐹 = { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) }
2		cfsetsnfsetfv.g	⊢ 𝐺 = { 𝑥 ∣ 𝑥 : { 𝑌 } ⟶ 𝐵 }
3		cfsetsnfsetfv.h	⊢ 𝐻 = ( 𝑔 ∈ 𝐺 ↦ ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) )
4		simpl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → 𝐴 ∈ 𝑉 )
5	4	adantr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐺 ) → 𝐴 ∈ 𝑉 )
6	5	mptexd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐺 ) → ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) ∈ V )
7		vex	⊢ 𝑔 ∈ V
8		feq1	⊢ ( 𝑥 = 𝑔 → ( 𝑥 : { 𝑌 } ⟶ 𝐵 ↔ 𝑔 : { 𝑌 } ⟶ 𝐵 ) )
9	7 8 2	elab2	⊢ ( 𝑔 ∈ 𝐺 ↔ 𝑔 : { 𝑌 } ⟶ 𝐵 )
10	9	bilani	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐺 ) → 𝑔 : { 𝑌 } ⟶ 𝐵 )
11		snidg	⊢ ( 𝑌 ∈ 𝐴 → 𝑌 ∈ { 𝑌 } )
12	11	adantl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → 𝑌 ∈ { 𝑌 } )
13	12	adantr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐺 ) → 𝑌 ∈ { 𝑌 } )
14	10 13	ffvelcdmd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐺 ) → ( 𝑔 ‘ 𝑌 ) ∈ 𝐵 )
15	14	adantr	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐺 ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑌 ) ∈ 𝐵 )
16	15	fmpttd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐺 ) → ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) : 𝐴 ⟶ 𝐵 )
17		eqeq2	⊢ ( 𝑏 = ( 𝑔 ‘ 𝑌 ) → ( ( 𝑔 ‘ 𝑌 ) = 𝑏 ↔ ( 𝑔 ‘ 𝑌 ) = ( 𝑔 ‘ 𝑌 ) ) )
18	17	ralbidv	⊢ ( 𝑏 = ( 𝑔 ‘ 𝑌 ) → ( ∀ 𝑧 ∈ 𝐴 ( 𝑔 ‘ 𝑌 ) = 𝑏 ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑔 ‘ 𝑌 ) = ( 𝑔 ‘ 𝑌 ) ) )
19	18	adantl	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐺 ) ∧ 𝑏 = ( 𝑔 ‘ 𝑌 ) ) → ( ∀ 𝑧 ∈ 𝐴 ( 𝑔 ‘ 𝑌 ) = 𝑏 ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑔 ‘ 𝑌 ) = ( 𝑔 ‘ 𝑌 ) ) )
20		eqidd	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐺 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑌 ) = ( 𝑔 ‘ 𝑌 ) )
21	20	ralrimiva	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐺 ) → ∀ 𝑧 ∈ 𝐴 ( 𝑔 ‘ 𝑌 ) = ( 𝑔 ‘ 𝑌 ) )
22	14 19 21	rspcedvd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐺 ) → ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑔 ‘ 𝑌 ) = 𝑏 )
23	16 22	jca	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐺 ) → ( ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑔 ‘ 𝑌 ) = 𝑏 ) )
24		feq1	⊢ ( 𝑓 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) → ( 𝑓 : 𝐴 ⟶ 𝐵 ↔ ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) : 𝐴 ⟶ 𝐵 ) )
25		simpl	⊢ ( ( 𝑓 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝑓 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) )
26		eqidd	⊢ ( ( ( 𝑓 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑎 = 𝑧 ) → ( 𝑔 ‘ 𝑌 ) = ( 𝑔 ‘ 𝑌 ) )
27		simpr	⊢ ( ( 𝑓 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 )
28		fvexd	⊢ ( ( 𝑓 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑌 ) ∈ V )
29		nfcv	⊢ Ⅎ 𝑎 𝑓
30		nfmpt1	⊢ Ⅎ 𝑎 ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) )
31	29 30	nfeq	⊢ Ⅎ 𝑎 𝑓 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) )
32		nfv	⊢ Ⅎ 𝑎 𝑧 ∈ 𝐴
33	31 32	nfan	⊢ Ⅎ 𝑎 ( 𝑓 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) ∧ 𝑧 ∈ 𝐴 )
34		nfcv	⊢ Ⅎ 𝑎 𝑧
35		nfcv	⊢ Ⅎ 𝑎 ( 𝑔 ‘ 𝑌 )
36	25 26 27 28 33 34 35	fvmptdf	⊢ ( ( 𝑓 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑧 ) = ( 𝑔 ‘ 𝑌 ) )
37	36	eqeq1d	⊢ ( ( 𝑓 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑓 ‘ 𝑧 ) = 𝑏 ↔ ( 𝑔 ‘ 𝑌 ) = 𝑏 ) )
38	37	ralbidva	⊢ ( 𝑓 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) → ( ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑔 ‘ 𝑌 ) = 𝑏 ) )
39	38	rexbidv	⊢ ( 𝑓 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) → ( ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ↔ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑔 ‘ 𝑌 ) = 𝑏 ) )
40	24 39	anbi12d	⊢ ( 𝑓 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) → ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) ↔ ( ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑔 ‘ 𝑌 ) = 𝑏 ) ) )
41	6 23 40	elabd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐺 ) → ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) ∈ { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) } )
42	41 1	eleqtrrdi	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐺 ) → ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) ∈ 𝐹 )
43	42 3	fmptd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → 𝐻 : 𝐺 ⟶ 𝐹 )