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 ∈ A ∧ y ∈ B → C ∈ D
oprabco.2 ⊢ F = x ∈ A , y ∈ B ⟼ C
oprabco.3 ⊢ G = x ∈ A , y ∈ B ⟼ H ⁡ C
Assertion oprabco ⊢ H Fn D → G = H ∘ F

Proof

Step Hyp Ref Expression
1 oprabco.1 ⊢ x ∈ A ∧ y ∈ B → C ∈ D
2 oprabco.2 ⊢ F = x ∈ A , y ∈ B ⟼ C
3 oprabco.3 ⊢ G = x ∈ A , y ∈ B ⟼ H ⁡ C
4 1 adantl ⊢ H Fn D ∧ x ∈ A ∧ y ∈ B → C ∈ D
5 2 a1i ⊢ H Fn D → F = x ∈ A , y ∈ B ⟼ C
6 dffn5 ⊢ H Fn D ↔ H = z ∈ D ⟼ H ⁡ z
7 6 biimpi ⊢ H Fn D → H = z ∈ D ⟼ H ⁡ z
8 fveq2 ⊢ z = C → H ⁡ z = H ⁡ C
9 4 5 7 8 fmpoco ⊢ H Fn D → H ∘ F = x ∈ A , y ∈ B ⟼ H ⁡ C
10 3 9 eqtr4id ⊢ H Fn D → G = H ∘ F