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

Metamath Proof Explorer

Theorem fvproj

Description: Value of a function on ordered pairs with values expressed as ordered pairs. Note that F and G are the projections of H to the first and second coordinate respectively. (Contributed by Thierry Arnoux, 30-Dec-2019)

Ref Expression
Hypotheses fvproj.h ⊢ H = x ∈ A , y ∈ B ⟼ F ⁡ x G ⁡ y
fvproj.x ⊢ φ → X ∈ A
fvproj.y ⊢ φ → Y ∈ B
Assertion fvproj ⊢ φ → H ⁡ X Y = F ⁡ X G ⁡ Y

Proof

Step Hyp Ref Expression
1 fvproj.h ⊢ H = x ∈ A , y ∈ B ⟼ F ⁡ x G ⁡ y
2 fvproj.x ⊢ φ → X ∈ A
3 fvproj.y ⊢ φ → Y ∈ B
4 df-ov ⊢ X H Y = H ⁡ X Y
5 fveq2 ⊢ a = X → F ⁡ a = F ⁡ X
6 5 opeq1d ⊢ a = X → F ⁡ a G ⁡ b = F ⁡ X G ⁡ b
7 fveq2 ⊢ b = Y → G ⁡ b = G ⁡ Y
8 7 opeq2d ⊢ b = Y → F ⁡ X G ⁡ b = F ⁡ X G ⁡ Y
9 fveq2 ⊢ x = a → F ⁡ x = F ⁡ a
10 9 opeq1d ⊢ x = a → F ⁡ x G ⁡ y = F ⁡ a G ⁡ y
11 fveq2 ⊢ y = b → G ⁡ y = G ⁡ b
12 11 opeq2d ⊢ y = b → F ⁡ a G ⁡ y = F ⁡ a G ⁡ b
13 10 12 cbvmpov ⊢ x ∈ A , y ∈ B ⟼ F ⁡ x G ⁡ y = a ∈ A , b ∈ B ⟼ F ⁡ a G ⁡ b
14 1 13 eqtri ⊢ H = a ∈ A , b ∈ B ⟼ F ⁡ a G ⁡ b
15 opex ⊢ F ⁡ X G ⁡ Y ∈ V
16 6 8 14 15 ovmpo ⊢ X ∈ A ∧ Y ∈ B → X H Y = F ⁡ X G ⁡ Y
17 2 3 16 syl2anc ⊢ φ → X H Y = F ⁡ X G ⁡ Y
18 4 17 eqtr3id ⊢ φ → H ⁡ X Y = F ⁡ X G ⁡ Y