Metamath Proof Explorer


Theorem resfval2

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

Ref Expression
Hypotheses resfval.c φ F V
resfval.d φ H W
resfval2.g φ G X
resfval2.d φ H Fn S × S
Assertion resfval2 φ F G f H = F S x S , y S x G y x H y

Proof

Step Hyp Ref Expression
1 resfval.c φ F V
2 resfval.d φ H W
3 resfval2.g φ G X
4 resfval2.d φ H Fn S × S
5 opex F G V
6 5 a1i φ F G V
7 6 2 resfval φ F G f H = 1 st F G dom dom H z dom H 2 nd F G z H z
8 op1stg F V G X 1 st F G = F
9 1 3 8 syl2anc φ 1 st F G = F
10 fndm H Fn S × S dom H = S × S
11 4 10 syl φ dom H = S × S
12 11 dmeqd φ dom dom H = dom S × S
13 dmxpid dom S × S = S
14 12 13 syl6eq φ dom dom H = S
15 9 14 reseq12d φ 1 st F G dom dom H = F S
16 op2ndg F V G X 2 nd F G = G
17 1 3 16 syl2anc φ 2 nd F G = G
18 17 fveq1d φ 2 nd F G z = G z
19 18 reseq1d φ 2 nd F G z H z = G z H z
20 11 19 mpteq12dv φ z dom H 2 nd F G z H z = z S × S G z H z
21 fveq2 z = x y G z = G x y
22 df-ov x G y = G x y
23 21 22 syl6eqr z = x y G z = x G y
24 fveq2 z = x y H z = H x y
25 df-ov x H y = H x y
26 24 25 syl6eqr z = x y H z = x H y
27 23 26 reseq12d z = x y G z H z = x G y x H y
28 27 mpompt z S × S G z H z = x S , y S x G y x H y
29 20 28 syl6eq φ z dom H 2 nd F G z H z = x S , y S x G y x H y
30 15 29 opeq12d φ 1 st F G dom dom H z dom H 2 nd F G z H z = F S x S , y S x G y x H y
31 7 30 eqtrd φ F G f H = F S x S , y S x G y x H y