Theorem cofmpt2

Description: Express composition of a maps-to function with another function in a maps-to notation. (Contributed by Thierry Arnoux, 15-Jul-2023)

	Ref	Expression
Hypotheses	cofmpt2.1	⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → 𝐶 = 𝐷 )
	cofmpt2.2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝐶 ∈ 𝐸 )
	cofmpt2.3	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	cofmpt2.4	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
Assertion	cofmpt2	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		cofmpt2.1	⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → 𝐶 = 𝐷 )
2		cofmpt2.2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝐶 ∈ 𝐸 )
3		cofmpt2.3	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
4		cofmpt2.4	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
5	2	fmpttd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) : 𝐵 ⟶ 𝐸 )
6		fcompt	⊢ ( ( ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) : 𝐵 ⟶ 𝐸 ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
7	5 3 6	syl2anc	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
8		eqid	⊢ ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑦 ∈ 𝐵 ↦ 𝐶 )
9	1	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → 𝐶 = 𝐷 )
10	3	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
11	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐷 ∈ 𝑉 )
12	8 9 10 11	fvmptd2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝐷 )
13	12	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ 𝐷 ) )
14	7 13	eqtrd	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐷 ) )