resfval

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

	Ref	Expression
Hypotheses	resfval.c	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
	resfval.d	⊢ ( 𝜑 → 𝐻 ∈ 𝑊 )
Assertion	resfval	⊢ ( 𝜑 → ( 𝐹 ↾_f 𝐻 ) = ⟨ ( ( 1^st ‘ 𝐹 ) ↾ dom dom 𝐻 ) , ( 𝑥 ∈ dom 𝐻 ↦ ( ( ( 2^nd ‘ 𝐹 ) ‘ 𝑥 ) ↾ ( 𝐻 ‘ 𝑥 ) ) ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		resfval.c	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
2		resfval.d	⊢ ( 𝜑 → 𝐻 ∈ 𝑊 )
3		df-resf	⊢ ↾_f = ( 𝑓 ∈ V , ℎ ∈ V ↦ ⟨ ( ( 1^st ‘ 𝑓 ) ↾ dom dom ℎ ) , ( 𝑥 ∈ dom ℎ ↦ ( ( ( 2^nd ‘ 𝑓 ) ‘ 𝑥 ) ↾ ( ℎ ‘ 𝑥 ) ) ) ⟩ )
4	3	a1i	⊢ ( 𝜑 → ↾_f = ( 𝑓 ∈ V , ℎ ∈ V ↦ ⟨ ( ( 1^st ‘ 𝑓 ) ↾ dom dom ℎ ) , ( 𝑥 ∈ dom ℎ ↦ ( ( ( 2^nd ‘ 𝑓 ) ‘ 𝑥 ) ↾ ( ℎ ‘ 𝑥 ) ) ) ⟩ ) )
5		simprl	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ ℎ = 𝐻 ) ) → 𝑓 = 𝐹 )
6	5	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ ℎ = 𝐻 ) ) → ( 1^st ‘ 𝑓 ) = ( 1^st ‘ 𝐹 ) )
7		simprr	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ ℎ = 𝐻 ) ) → ℎ = 𝐻 )
8	7	dmeqd	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ ℎ = 𝐻 ) ) → dom ℎ = dom 𝐻 )
9	8	dmeqd	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ ℎ = 𝐻 ) ) → dom dom ℎ = dom dom 𝐻 )
10	6 9	reseq12d	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ ℎ = 𝐻 ) ) → ( ( 1^st ‘ 𝑓 ) ↾ dom dom ℎ ) = ( ( 1^st ‘ 𝐹 ) ↾ dom dom 𝐻 ) )
11	5	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ ℎ = 𝐻 ) ) → ( 2^nd ‘ 𝑓 ) = ( 2^nd ‘ 𝐹 ) )
12	11	fveq1d	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ ℎ = 𝐻 ) ) → ( ( 2^nd ‘ 𝑓 ) ‘ 𝑥 ) = ( ( 2^nd ‘ 𝐹 ) ‘ 𝑥 ) )
13	7	fveq1d	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ ℎ = 𝐻 ) ) → ( ℎ ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) )
14	12 13	reseq12d	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ ℎ = 𝐻 ) ) → ( ( ( 2^nd ‘ 𝑓 ) ‘ 𝑥 ) ↾ ( ℎ ‘ 𝑥 ) ) = ( ( ( 2^nd ‘ 𝐹 ) ‘ 𝑥 ) ↾ ( 𝐻 ‘ 𝑥 ) ) )
15	8 14	mpteq12dv	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ ℎ = 𝐻 ) ) → ( 𝑥 ∈ dom ℎ ↦ ( ( ( 2^nd ‘ 𝑓 ) ‘ 𝑥 ) ↾ ( ℎ ‘ 𝑥 ) ) ) = ( 𝑥 ∈ dom 𝐻 ↦ ( ( ( 2^nd ‘ 𝐹 ) ‘ 𝑥 ) ↾ ( 𝐻 ‘ 𝑥 ) ) ) )
16	10 15	opeq12d	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ ℎ = 𝐻 ) ) → ⟨ ( ( 1^st ‘ 𝑓 ) ↾ dom dom ℎ ) , ( 𝑥 ∈ dom ℎ ↦ ( ( ( 2^nd ‘ 𝑓 ) ‘ 𝑥 ) ↾ ( ℎ ‘ 𝑥 ) ) ) ⟩ = ⟨ ( ( 1^st ‘ 𝐹 ) ↾ dom dom 𝐻 ) , ( 𝑥 ∈ dom 𝐻 ↦ ( ( ( 2^nd ‘ 𝐹 ) ‘ 𝑥 ) ↾ ( 𝐻 ‘ 𝑥 ) ) ) ⟩ )
17	1	elexd	⊢ ( 𝜑 → 𝐹 ∈ V )
18	2	elexd	⊢ ( 𝜑 → 𝐻 ∈ V )
19		opex	⊢ ⟨ ( ( 1^st ‘ 𝐹 ) ↾ dom dom 𝐻 ) , ( 𝑥 ∈ dom 𝐻 ↦ ( ( ( 2^nd ‘ 𝐹 ) ‘ 𝑥 ) ↾ ( 𝐻 ‘ 𝑥 ) ) ) ⟩ ∈ V
20	19	a1i	⊢ ( 𝜑 → ⟨ ( ( 1^st ‘ 𝐹 ) ↾ dom dom 𝐻 ) , ( 𝑥 ∈ dom 𝐻 ↦ ( ( ( 2^nd ‘ 𝐹 ) ‘ 𝑥 ) ↾ ( 𝐻 ‘ 𝑥 ) ) ) ⟩ ∈ V )
21	4 16 17 18 20	ovmpod	⊢ ( 𝜑 → ( 𝐹 ↾_f 𝐻 ) = ⟨ ( ( 1^st ‘ 𝐹 ) ↾ dom dom 𝐻 ) , ( 𝑥 ∈ dom 𝐻 ↦ ( ( ( 2^nd ‘ 𝐹 ) ‘ 𝑥 ) ↾ ( 𝐻 ‘ 𝑥 ) ) ) ⟩ )

Metamath Proof Explorer

Theorem resfval

Proof