This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
11 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐷 ∈ 𝑉 )
12 8 9 10 11 fvmptd2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) ‘ ( 𝐹 ‘ 𝑥 ) ) = 𝐷 )
13 12 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ 𝐷 ) )
14 7 13 eqtrd ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐷 ) )