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	biimpi	⊢ ( 𝑔 ∈ 𝐺 → 𝑔 : { 𝑌 } ⟶ 𝐵 )
11	10	adantl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐺 ) → 𝑔 : { 𝑌 } ⟶ 𝐵 )
12		snidg	⊢ ( 𝑌 ∈ 𝐴 → 𝑌 ∈ { 𝑌 } )
13	12	adantl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → 𝑌 ∈ { 𝑌 } )
14	13	adantr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐺 ) → 𝑌 ∈ { 𝑌 } )
15	11 14	ffvelrnd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐺 ) → ( 𝑔 ‘ 𝑌 ) ∈ 𝐵 )
16	15	adantr	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐺 ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑌 ) ∈ 𝐵 )
17	16	fmpttd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐺 ) → ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) : 𝐴 ⟶ 𝐵 )
18		eqeq2	⊢ ( 𝑏 = ( 𝑔 ‘ 𝑌 ) → ( ( 𝑔 ‘ 𝑌 ) = 𝑏 ↔ ( 𝑔 ‘ 𝑌 ) = ( 𝑔 ‘ 𝑌 ) ) )
19	18	ralbidv	⊢ ( 𝑏 = ( 𝑔 ‘ 𝑌 ) → ( ∀ 𝑧 ∈ 𝐴 ( 𝑔 ‘ 𝑌 ) = 𝑏 ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑔 ‘ 𝑌 ) = ( 𝑔 ‘ 𝑌 ) ) )
20	19	adantl	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐺 ) ∧ 𝑏 = ( 𝑔 ‘ 𝑌 ) ) → ( ∀ 𝑧 ∈ 𝐴 ( 𝑔 ‘ 𝑌 ) = 𝑏 ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑔 ‘ 𝑌 ) = ( 𝑔 ‘ 𝑌 ) ) )
21		eqidd	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐺 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑌 ) = ( 𝑔 ‘ 𝑌 ) )
22	21	ralrimiva	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐺 ) → ∀ 𝑧 ∈ 𝐴 ( 𝑔 ‘ 𝑌 ) = ( 𝑔 ‘ 𝑌 ) )
23	15 20 22	rspcedvd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐺 ) → ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑔 ‘ 𝑌 ) = 𝑏 )
24	17 23	jca	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐺 ) → ( ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑔 ‘ 𝑌 ) = 𝑏 ) )
25		feq1	⊢ ( 𝑓 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) → ( 𝑓 : 𝐴 ⟶ 𝐵 ↔ ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) : 𝐴 ⟶ 𝐵 ) )
26		simpl	⊢ ( ( 𝑓 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝑓 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) )
27		eqidd	⊢ ( ( ( 𝑓 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑎 = 𝑧 ) → ( 𝑔 ‘ 𝑌 ) = ( 𝑔 ‘ 𝑌 ) )
28		simpr	⊢ ( ( 𝑓 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 )
29		fvexd	⊢ ( ( 𝑓 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑌 ) ∈ V )
30		nfcv	⊢ Ⅎ 𝑎 𝑓
31		nfmpt1	⊢ Ⅎ 𝑎 ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) )
32	30 31	nfeq	⊢ Ⅎ 𝑎 𝑓 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) )
33		nfv	⊢ Ⅎ 𝑎 𝑧 ∈ 𝐴
34	32 33	nfan	⊢ Ⅎ 𝑎 ( 𝑓 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) ∧ 𝑧 ∈ 𝐴 )
35		nfcv	⊢ Ⅎ 𝑎 𝑧
36		nfcv	⊢ Ⅎ 𝑎 ( 𝑔 ‘ 𝑌 )
37	26 27 28 29 34 35 36	fvmptdf	⊢ ( ( 𝑓 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑧 ) = ( 𝑔 ‘ 𝑌 ) )
38	37	eqeq1d	⊢ ( ( 𝑓 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑓 ‘ 𝑧 ) = 𝑏 ↔ ( 𝑔 ‘ 𝑌 ) = 𝑏 ) )
39	38	ralbidva	⊢ ( 𝑓 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) → ( ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑔 ‘ 𝑌 ) = 𝑏 ) )
40	39	rexbidv	⊢ ( 𝑓 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) → ( ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ↔ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑔 ‘ 𝑌 ) = 𝑏 ) )
41	25 40	anbi12d	⊢ ( 𝑓 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) → ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) ↔ ( ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑔 ‘ 𝑌 ) = 𝑏 ) ) )
42	6 24 41	elabd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐺 ) → ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) ∈ { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) } )
43	42 1	eleqtrrdi	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐺 ) → ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) ∈ 𝐹 )
44	43 3	fmptd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → 𝐻 : 𝐺 ⟶ 𝐹 )