Theorem cfsetsnfsetfv

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

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

Proof

Step	Hyp	Ref	Expression
1		cfsetsnfsetfv.f	⊢ 𝐹 = { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) }
2		cfsetsnfsetfv.g	⊢ 𝐺 = { 𝑥 ∣ 𝑥 : { 𝑌 } ⟶ 𝐵 }
3		cfsetsnfsetfv.h	⊢ 𝐻 = ( 𝑔 ∈ 𝐺 ↦ ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) )
4	3	a1i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐺 ) → 𝐻 = ( 𝑔 ∈ 𝐺 ↦ ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) ) )
5		fveq1	⊢ ( 𝑔 = 𝑋 → ( 𝑔 ‘ 𝑌 ) = ( 𝑋 ‘ 𝑌 ) )
6	5	adantr	⊢ ( ( 𝑔 = 𝑋 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑌 ) = ( 𝑋 ‘ 𝑌 ) )
7	6	mpteq2dva	⊢ ( 𝑔 = 𝑋 → ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) = ( 𝑎 ∈ 𝐴 ↦ ( 𝑋 ‘ 𝑌 ) ) )
8	7	adantl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐺 ) ∧ 𝑔 = 𝑋 ) → ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) = ( 𝑎 ∈ 𝐴 ↦ ( 𝑋 ‘ 𝑌 ) ) )
9		simpr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐺 ) → 𝑋 ∈ 𝐺 )
10		simpl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐺 ) → 𝐴 ∈ 𝑉 )
11	10	mptexd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐺 ) → ( 𝑎 ∈ 𝐴 ↦ ( 𝑋 ‘ 𝑌 ) ) ∈ V )
12	4 8 9 11	fvmptd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐺 ) → ( 𝐻 ‘ 𝑋 ) = ( 𝑎 ∈ 𝐴 ↦ ( 𝑋 ‘ 𝑌 ) ) )