Metamath Proof Explorer


Theorem resf2nd

Description: Value of the functor restriction operator on morphisms. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses resf1st.f ( 𝜑𝐹𝑉 )
resf1st.h ( 𝜑𝐻𝑊 )
resf1st.s ( 𝜑𝐻 Fn ( 𝑆 × 𝑆 ) )
resf2nd.x ( 𝜑𝑋𝑆 )
resf2nd.y ( 𝜑𝑌𝑆 )
Assertion resf2nd ( 𝜑 → ( 𝑋 ( 2nd ‘ ( 𝐹f 𝐻 ) ) 𝑌 ) = ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ↾ ( 𝑋 𝐻 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 resf1st.f ( 𝜑𝐹𝑉 )
2 resf1st.h ( 𝜑𝐻𝑊 )
3 resf1st.s ( 𝜑𝐻 Fn ( 𝑆 × 𝑆 ) )
4 resf2nd.x ( 𝜑𝑋𝑆 )
5 resf2nd.y ( 𝜑𝑌𝑆 )
6 df-ov ( 𝑋 ( 2nd ‘ ( 𝐹f 𝐻 ) ) 𝑌 ) = ( ( 2nd ‘ ( 𝐹f 𝐻 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ )
7 1 2 resfval ( 𝜑 → ( 𝐹f 𝐻 ) = ⟨ ( ( 1st𝐹 ) ↾ dom dom 𝐻 ) , ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2nd𝐹 ) ‘ 𝑧 ) ↾ ( 𝐻𝑧 ) ) ) ⟩ )
8 7 fveq2d ( 𝜑 → ( 2nd ‘ ( 𝐹f 𝐻 ) ) = ( 2nd ‘ ⟨ ( ( 1st𝐹 ) ↾ dom dom 𝐻 ) , ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2nd𝐹 ) ‘ 𝑧 ) ↾ ( 𝐻𝑧 ) ) ) ⟩ ) )
9 fvex ( 1st𝐹 ) ∈ V
10 9 resex ( ( 1st𝐹 ) ↾ dom dom 𝐻 ) ∈ V
11 dmexg ( 𝐻𝑊 → dom 𝐻 ∈ V )
12 mptexg ( dom 𝐻 ∈ V → ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2nd𝐹 ) ‘ 𝑧 ) ↾ ( 𝐻𝑧 ) ) ) ∈ V )
13 2 11 12 3syl ( 𝜑 → ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2nd𝐹 ) ‘ 𝑧 ) ↾ ( 𝐻𝑧 ) ) ) ∈ V )
14 op2ndg ( ( ( ( 1st𝐹 ) ↾ dom dom 𝐻 ) ∈ V ∧ ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2nd𝐹 ) ‘ 𝑧 ) ↾ ( 𝐻𝑧 ) ) ) ∈ V ) → ( 2nd ‘ ⟨ ( ( 1st𝐹 ) ↾ dom dom 𝐻 ) , ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2nd𝐹 ) ‘ 𝑧 ) ↾ ( 𝐻𝑧 ) ) ) ⟩ ) = ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2nd𝐹 ) ‘ 𝑧 ) ↾ ( 𝐻𝑧 ) ) ) )
15 10 13 14 sylancr ( 𝜑 → ( 2nd ‘ ⟨ ( ( 1st𝐹 ) ↾ dom dom 𝐻 ) , ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2nd𝐹 ) ‘ 𝑧 ) ↾ ( 𝐻𝑧 ) ) ) ⟩ ) = ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2nd𝐹 ) ‘ 𝑧 ) ↾ ( 𝐻𝑧 ) ) ) )
16 8 15 eqtrd ( 𝜑 → ( 2nd ‘ ( 𝐹f 𝐻 ) ) = ( 𝑧 ∈ dom 𝐻 ↦ ( ( ( 2nd𝐹 ) ‘ 𝑧 ) ↾ ( 𝐻𝑧 ) ) ) )
17 simpr ( ( 𝜑𝑧 = ⟨ 𝑋 , 𝑌 ⟩ ) → 𝑧 = ⟨ 𝑋 , 𝑌 ⟩ )
18 17 fveq2d ( ( 𝜑𝑧 = ⟨ 𝑋 , 𝑌 ⟩ ) → ( ( 2nd𝐹 ) ‘ 𝑧 ) = ( ( 2nd𝐹 ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
19 df-ov ( 𝑋 ( 2nd𝐹 ) 𝑌 ) = ( ( 2nd𝐹 ) ‘ ⟨ 𝑋 , 𝑌 ⟩ )
20 18 19 eqtr4di ( ( 𝜑𝑧 = ⟨ 𝑋 , 𝑌 ⟩ ) → ( ( 2nd𝐹 ) ‘ 𝑧 ) = ( 𝑋 ( 2nd𝐹 ) 𝑌 ) )
21 17 fveq2d ( ( 𝜑𝑧 = ⟨ 𝑋 , 𝑌 ⟩ ) → ( 𝐻𝑧 ) = ( 𝐻 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
22 df-ov ( 𝑋 𝐻 𝑌 ) = ( 𝐻 ‘ ⟨ 𝑋 , 𝑌 ⟩ )
23 21 22 eqtr4di ( ( 𝜑𝑧 = ⟨ 𝑋 , 𝑌 ⟩ ) → ( 𝐻𝑧 ) = ( 𝑋 𝐻 𝑌 ) )
24 20 23 reseq12d ( ( 𝜑𝑧 = ⟨ 𝑋 , 𝑌 ⟩ ) → ( ( ( 2nd𝐹 ) ‘ 𝑧 ) ↾ ( 𝐻𝑧 ) ) = ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ↾ ( 𝑋 𝐻 𝑌 ) ) )
25 4 5 opelxpd ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝑆 × 𝑆 ) )
26 3 fndmd ( 𝜑 → dom 𝐻 = ( 𝑆 × 𝑆 ) )
27 25 26 eleqtrrd ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ dom 𝐻 )
28 ovex ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ∈ V
29 28 resex ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ↾ ( 𝑋 𝐻 𝑌 ) ) ∈ V
30 29 a1i ( 𝜑 → ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ↾ ( 𝑋 𝐻 𝑌 ) ) ∈ V )
31 16 24 27 30 fvmptd ( 𝜑 → ( ( 2nd ‘ ( 𝐹f 𝐻 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ↾ ( 𝑋 𝐻 𝑌 ) ) )
32 6 31 eqtrid ( 𝜑 → ( 𝑋 ( 2nd ‘ ( 𝐹f 𝐻 ) ) 𝑌 ) = ( ( 𝑋 ( 2nd𝐹 ) 𝑌 ) ↾ ( 𝑋 𝐻 𝑌 ) ) )