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

Metamath Proof Explorer

Theorem oprabco

Description: Composition of a function with an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 26-Sep-2015)

Ref Expression
Hypotheses oprabco.1 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝐶 ∈ 𝐷 )
oprabco.2 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
oprabco.3 ⊢ 𝐺 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝐻 ‘ 𝐶 ) )
Assertion oprabco ( 𝐻 Fn 𝐷 → 𝐺 = ( 𝐻 ∘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 oprabco.1 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝐶 ∈ 𝐷 )
2 oprabco.2 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
3 oprabco.3 ⊢ 𝐺 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝐻 ‘ 𝐶 ) )
4 1 adantl ⊢ ( ( 𝐻 Fn 𝐷 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐶 ∈ 𝐷 )
5 2 a1i ⊢ ( 𝐻 Fn 𝐷 → 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) )
6 dffn5 ⊢ ( 𝐻 Fn 𝐷 ↔ 𝐻 = ( 𝑧 ∈ 𝐷 ↦ ( 𝐻 ‘ 𝑧 ) ) )
7 6 biimpi ⊢ ( 𝐻 Fn 𝐷 → 𝐻 = ( 𝑧 ∈ 𝐷 ↦ ( 𝐻 ‘ 𝑧 ) ) )
8 fveq2 ⊢ ( 𝑧 = 𝐶 → ( 𝐻 ‘ 𝑧 ) = ( 𝐻 ‘ 𝐶 ) )
9 4 5 7 8 fmpoco ⊢ ( 𝐻 Fn 𝐷 → ( 𝐻 ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝐻 ‘ 𝐶 ) ) )
10 3 9 eqtr4id ⊢ ( 𝐻 Fn 𝐷 → 𝐺 = ( 𝐻 ∘ 𝐹 ) )