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 𝐷𝐺 = ( 𝐻𝐹 ) )