Theorem resfval2 17862

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

Hypotheses

Ref	Expression
resfval.c	⊢ (𝜑 → 𝐹 ∈ 𝑉)
resfval.d	⊢ (𝜑 → 𝐻 ∈ 𝑊)
resfval2.g	⊢ (𝜑 → 𝐺 ∈ 𝑋)
resfval2.d	⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))

Assertion

Ref	Expression
resfval2	⊢ (𝜑 → (⟨𝐹, 𝐺⟩ ↾f 𝐻) = ⟨(𝐹 ↾ 𝑆), (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ((𝑥𝐺𝑦) ↾ (𝑥𝐻𝑦)))⟩)

Distinct variable groups:   𝑥,𝐹   𝑥,𝑦,𝐺   𝑥,𝐻,𝑦   𝜑,𝑥   𝑥,𝑆,𝑦

Allowed substitution hints:   𝜑(𝑦)   𝐹(𝑦)   𝑉(𝑥,𝑦)   𝑊(𝑥,𝑦)   𝑋(𝑥,𝑦)

Proof of Theorem resfval2

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		opex 5427	. . . 4 ⊢ ⟨𝐹, 𝐺⟩ ∈ V
2	1	a1i 11	. . 3 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩ ∈ V)
3		resfval.d	. . 3 ⊢ (𝜑 → 𝐻 ∈ 𝑊)
4	2, 3	resfval 17861	. 2 ⊢ (𝜑 → (⟨𝐹, 𝐺⟩ ↾f 𝐻) = ⟨((1st ‘⟨𝐹, 𝐺⟩) ↾ dom dom 𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd ‘⟨𝐹, 𝐺⟩)‘𝑧) ↾ (𝐻‘𝑧)))⟩)
5		resfval.c	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ 𝑉)
6		resfval2.g	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ 𝑋)
7		op1stg 7983	. . . . 5 ⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑋) → (1st ‘⟨𝐹, 𝐺⟩) = 𝐹)
8	5, 6, 7	syl2anc 584	. . . 4 ⊢ (𝜑 → (1st ‘⟨𝐹, 𝐺⟩) = 𝐹)
9		resfval2.d	. . . . . . 7 ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))
10	9	fndmd 6626	. . . . . 6 ⊢ (𝜑 → dom 𝐻 = (𝑆 × 𝑆))
11	10	dmeqd 5872	. . . . 5 ⊢ (𝜑 → dom dom 𝐻 = dom (𝑆 × 𝑆))
12		dmxpid 5897	. . . . 5 ⊢ dom (𝑆 × 𝑆) = 𝑆
13	11, 12	eqtrdi 2781	. . . 4 ⊢ (𝜑 → dom dom 𝐻 = 𝑆)
14	8, 13	reseq12d 5954	. . 3 ⊢ (𝜑 → ((1st ‘⟨𝐹, 𝐺⟩) ↾ dom dom 𝐻) = (𝐹 ↾ 𝑆))
15		op2ndg 7984	. . . . . . . 8 ⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑋) → (2nd ‘⟨𝐹, 𝐺⟩) = 𝐺)
16	5, 6, 15	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (2nd ‘⟨𝐹, 𝐺⟩) = 𝐺)
17	16	fveq1d 6863	. . . . . 6 ⊢ (𝜑 → ((2nd ‘⟨𝐹, 𝐺⟩)‘𝑧) = (𝐺‘𝑧))
18	17	reseq1d 5952	. . . . 5 ⊢ (𝜑 → (((2nd ‘⟨𝐹, 𝐺⟩)‘𝑧) ↾ (𝐻‘𝑧)) = ((𝐺‘𝑧) ↾ (𝐻‘𝑧)))
19	10, 18	mpteq12dv 5197	. . . 4 ⊢ (𝜑 → (𝑧 ∈ dom 𝐻 ↦ (((2nd ‘⟨𝐹, 𝐺⟩)‘𝑧) ↾ (𝐻‘𝑧))) = (𝑧 ∈ (𝑆 × 𝑆) ↦ ((𝐺‘𝑧) ↾ (𝐻‘𝑧))))
20		fveq2 6861	. . . . . . 7 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐺‘𝑧) = (𝐺‘⟨𝑥, 𝑦⟩))
21		df-ov 7393	. . . . . . 7 ⊢ (𝑥𝐺𝑦) = (𝐺‘⟨𝑥, 𝑦⟩)
22	20, 21	eqtr4di 2783	. . . . . 6 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐺‘𝑧) = (𝑥𝐺𝑦))
23		fveq2 6861	. . . . . . 7 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐻‘𝑧) = (𝐻‘⟨𝑥, 𝑦⟩))
24		df-ov 7393	. . . . . . 7 ⊢ (𝑥𝐻𝑦) = (𝐻‘⟨𝑥, 𝑦⟩)
25	23, 24	eqtr4di 2783	. . . . . 6 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐻‘𝑧) = (𝑥𝐻𝑦))
26	22, 25	reseq12d 5954	. . . . 5 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((𝐺‘𝑧) ↾ (𝐻‘𝑧)) = ((𝑥𝐺𝑦) ↾ (𝑥𝐻𝑦)))
27	26	mpompt 7506	. . . 4 ⊢ (𝑧 ∈ (𝑆 × 𝑆) ↦ ((𝐺‘𝑧) ↾ (𝐻‘𝑧))) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ((𝑥𝐺𝑦) ↾ (𝑥𝐻𝑦)))
28	19, 27	eqtrdi 2781	. . 3 ⊢ (𝜑 → (𝑧 ∈ dom 𝐻 ↦ (((2nd ‘⟨𝐹, 𝐺⟩)‘𝑧) ↾ (𝐻‘𝑧))) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ((𝑥𝐺𝑦) ↾ (𝑥𝐻𝑦))))
29	14, 28	opeq12d 4848	. 2 ⊢ (𝜑 → ⟨((1st ‘⟨𝐹, 𝐺⟩) ↾ dom dom 𝐻), (𝑧 ∈ dom 𝐻 ↦ (((2nd ‘⟨𝐹, 𝐺⟩)‘𝑧) ↾ (𝐻‘𝑧)))⟩ = ⟨(𝐹 ↾ 𝑆), (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ((𝑥𝐺𝑦) ↾ (𝑥𝐻𝑦)))⟩)
30	4, 29	eqtrd 2765	1 ⊢ (𝜑 → (⟨𝐹, 𝐺⟩ ↾f 𝐻) = ⟨(𝐹 ↾ 𝑆), (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ((𝑥𝐺𝑦) ↾ (𝑥𝐻𝑦)))⟩)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3450  ⟨cop 4598   ↦ cmpt 5191   × cxp 5639  dom cdm 5641   ↾ cres 5643   Fn wfn 6509  ‘cfv 6514  (class class class)co 7390   ∈ cmpo 7392  1^st c1st 7969  2^nd c2nd 7970   ↾_f cresf 17826

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-iota 6467  df-fun 6516  df-fn 6517  df-fv 6522  df-ov 7393  df-oprab 7394  df-mpo 7395  df-1st 7971  df-2nd 7972  df-resf 17830

This theorem is referenced by:  funcrngcsetc  20556  funcringcsetc  20590