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 
|- ( ( x e. A /\ y e. B ) -> C e. D )
oprabco.2 
|- F = ( x e. A , y e. B |-> C )
oprabco.3 
|- G = ( x e. A , y e. B |-> ( H ` C ) )
Assertion oprabco 
|- ( H Fn D -> G = ( H o. F ) )

Proof

Step Hyp Ref Expression
1 oprabco.1 
 |-  ( ( x e. A /\ y e. B ) -> C e. D )
2 oprabco.2 
 |-  F = ( x e. A , y e. B |-> C )
3 oprabco.3 
 |-  G = ( x e. A , y e. B |-> ( H ` C ) )
4 1 adantl 
 |-  ( ( H Fn D /\ ( x e. A /\ y e. B ) ) -> C e. D )
5 2 a1i 
 |-  ( H Fn D -> F = ( x e. A , y e. B |-> C ) )
6 dffn5 
 |-  ( H Fn D <-> H = ( z e. D |-> ( H ` z ) ) )
7 6 biimpi 
 |-  ( H Fn D -> H = ( z e. D |-> ( H ` z ) ) )
8 fveq2 
 |-  ( z = C -> ( H ` z ) = ( H ` C ) )
9 4 5 7 8 fmpoco 
 |-  ( H Fn D -> ( H o. F ) = ( x e. A , y e. B |-> ( H ` C ) ) )
10 3 9 eqtr4id 
 |-  ( H Fn D -> G = ( H o. F ) )