# Metamath Proof Explorer

## Theorem resfunexg

Description: The restriction of a function to a set exists. Compare Proposition 6.17 of TakeutiZaring p. 28. (Contributed by NM, 7-Apr-1995) (Revised by Mario Carneiro, 22-Jun-2013)

Ref Expression
Assertion resfunexg ${⊢}\left(\mathrm{Fun}{A}\wedge {B}\in {C}\right)\to {{A}↾}_{{B}}\in \mathrm{V}$

### Proof

Step Hyp Ref Expression
1 funres ${⊢}\mathrm{Fun}{A}\to \mathrm{Fun}\left({{A}↾}_{{B}}\right)$
2 1 adantr ${⊢}\left(\mathrm{Fun}{A}\wedge {B}\in {C}\right)\to \mathrm{Fun}\left({{A}↾}_{{B}}\right)$
3 2 funfnd ${⊢}\left(\mathrm{Fun}{A}\wedge {B}\in {C}\right)\to \left({{A}↾}_{{B}}\right)Fn\mathrm{dom}\left({{A}↾}_{{B}}\right)$
4 dffn5 ${⊢}\left({{A}↾}_{{B}}\right)Fn\mathrm{dom}\left({{A}↾}_{{B}}\right)↔{{A}↾}_{{B}}=\left({x}\in \mathrm{dom}\left({{A}↾}_{{B}}\right)⟼\left({{A}↾}_{{B}}\right)\left({x}\right)\right)$
5 3 4 sylib ${⊢}\left(\mathrm{Fun}{A}\wedge {B}\in {C}\right)\to {{A}↾}_{{B}}=\left({x}\in \mathrm{dom}\left({{A}↾}_{{B}}\right)⟼\left({{A}↾}_{{B}}\right)\left({x}\right)\right)$
6 fvex ${⊢}\left({{A}↾}_{{B}}\right)\left({x}\right)\in \mathrm{V}$
7 6 fnasrn ${⊢}\left({x}\in \mathrm{dom}\left({{A}↾}_{{B}}\right)⟼\left({{A}↾}_{{B}}\right)\left({x}\right)\right)=\mathrm{ran}\left({x}\in \mathrm{dom}\left({{A}↾}_{{B}}\right)⟼⟨{x},\left({{A}↾}_{{B}}\right)\left({x}\right)⟩\right)$
8 5 7 syl6eq ${⊢}\left(\mathrm{Fun}{A}\wedge {B}\in {C}\right)\to {{A}↾}_{{B}}=\mathrm{ran}\left({x}\in \mathrm{dom}\left({{A}↾}_{{B}}\right)⟼⟨{x},\left({{A}↾}_{{B}}\right)\left({x}\right)⟩\right)$
9 opex ${⊢}⟨{x},\left({{A}↾}_{{B}}\right)\left({x}\right)⟩\in \mathrm{V}$
10 eqid ${⊢}\left({x}\in \mathrm{dom}\left({{A}↾}_{{B}}\right)⟼⟨{x},\left({{A}↾}_{{B}}\right)\left({x}\right)⟩\right)=\left({x}\in \mathrm{dom}\left({{A}↾}_{{B}}\right)⟼⟨{x},\left({{A}↾}_{{B}}\right)\left({x}\right)⟩\right)$
11 9 10 dmmpti ${⊢}\mathrm{dom}\left({x}\in \mathrm{dom}\left({{A}↾}_{{B}}\right)⟼⟨{x},\left({{A}↾}_{{B}}\right)\left({x}\right)⟩\right)=\mathrm{dom}\left({{A}↾}_{{B}}\right)$
12 11 imaeq2i ${⊢}\left({x}\in \mathrm{dom}\left({{A}↾}_{{B}}\right)⟼⟨{x},\left({{A}↾}_{{B}}\right)\left({x}\right)⟩\right)\left[\mathrm{dom}\left({x}\in \mathrm{dom}\left({{A}↾}_{{B}}\right)⟼⟨{x},\left({{A}↾}_{{B}}\right)\left({x}\right)⟩\right)\right]=\left({x}\in \mathrm{dom}\left({{A}↾}_{{B}}\right)⟼⟨{x},\left({{A}↾}_{{B}}\right)\left({x}\right)⟩\right)\left[\mathrm{dom}\left({{A}↾}_{{B}}\right)\right]$
13 imadmrn ${⊢}\left({x}\in \mathrm{dom}\left({{A}↾}_{{B}}\right)⟼⟨{x},\left({{A}↾}_{{B}}\right)\left({x}\right)⟩\right)\left[\mathrm{dom}\left({x}\in \mathrm{dom}\left({{A}↾}_{{B}}\right)⟼⟨{x},\left({{A}↾}_{{B}}\right)\left({x}\right)⟩\right)\right]=\mathrm{ran}\left({x}\in \mathrm{dom}\left({{A}↾}_{{B}}\right)⟼⟨{x},\left({{A}↾}_{{B}}\right)\left({x}\right)⟩\right)$
14 12 13 eqtr3i ${⊢}\left({x}\in \mathrm{dom}\left({{A}↾}_{{B}}\right)⟼⟨{x},\left({{A}↾}_{{B}}\right)\left({x}\right)⟩\right)\left[\mathrm{dom}\left({{A}↾}_{{B}}\right)\right]=\mathrm{ran}\left({x}\in \mathrm{dom}\left({{A}↾}_{{B}}\right)⟼⟨{x},\left({{A}↾}_{{B}}\right)\left({x}\right)⟩\right)$
15 8 14 syl6eqr ${⊢}\left(\mathrm{Fun}{A}\wedge {B}\in {C}\right)\to {{A}↾}_{{B}}=\left({x}\in \mathrm{dom}\left({{A}↾}_{{B}}\right)⟼⟨{x},\left({{A}↾}_{{B}}\right)\left({x}\right)⟩\right)\left[\mathrm{dom}\left({{A}↾}_{{B}}\right)\right]$
16 funmpt ${⊢}\mathrm{Fun}\left({x}\in \mathrm{dom}\left({{A}↾}_{{B}}\right)⟼⟨{x},\left({{A}↾}_{{B}}\right)\left({x}\right)⟩\right)$
17 dmresexg ${⊢}{B}\in {C}\to \mathrm{dom}\left({{A}↾}_{{B}}\right)\in \mathrm{V}$
18 17 adantl ${⊢}\left(\mathrm{Fun}{A}\wedge {B}\in {C}\right)\to \mathrm{dom}\left({{A}↾}_{{B}}\right)\in \mathrm{V}$
19 funimaexg ${⊢}\left(\mathrm{Fun}\left({x}\in \mathrm{dom}\left({{A}↾}_{{B}}\right)⟼⟨{x},\left({{A}↾}_{{B}}\right)\left({x}\right)⟩\right)\wedge \mathrm{dom}\left({{A}↾}_{{B}}\right)\in \mathrm{V}\right)\to \left({x}\in \mathrm{dom}\left({{A}↾}_{{B}}\right)⟼⟨{x},\left({{A}↾}_{{B}}\right)\left({x}\right)⟩\right)\left[\mathrm{dom}\left({{A}↾}_{{B}}\right)\right]\in \mathrm{V}$
20 16 18 19 sylancr ${⊢}\left(\mathrm{Fun}{A}\wedge {B}\in {C}\right)\to \left({x}\in \mathrm{dom}\left({{A}↾}_{{B}}\right)⟼⟨{x},\left({{A}↾}_{{B}}\right)\left({x}\right)⟩\right)\left[\mathrm{dom}\left({{A}↾}_{{B}}\right)\right]\in \mathrm{V}$
21 15 20 eqeltrd ${⊢}\left(\mathrm{Fun}{A}\wedge {B}\in {C}\right)\to {{A}↾}_{{B}}\in \mathrm{V}$