Theorem resfunexg 7220

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.)

Assertion

Ref	Expression
resfunexg	⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) ∈ V)

Proof of Theorem resfunexg

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		funres 6585	. . . . . . 7 ⊢ (Fun 𝐴 → Fun (𝐴 ↾ 𝐵))
2	1	adantr 486	. . . . . 6 ⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → Fun (𝐴 ↾ 𝐵))
3	2	funfnd 6574	. . . . 5 ⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) Fn dom (𝐴 ↾ 𝐵))
4		dffn5 6946	. . . . 5 ⊢ ((𝐴 ↾ 𝐵) Fn dom (𝐴 ↾ 𝐵) ↔ (𝐴 ↾ 𝐵) = (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ ((𝐴 ↾ 𝐵)‘𝑥)))
5	3, 4	sylib 221	. . . 4 ⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) = (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ ((𝐴 ↾ 𝐵)‘𝑥)))
6		fvex 6901	. . . . 5 ⊢ ((𝐴 ↾ 𝐵)‘𝑥) ∈ V
7	6	fnasrn 7148	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ ((𝐴 ↾ 𝐵)‘𝑥)) = ran (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ ⟨𝑥, ((𝐴 ↾ 𝐵)‘𝑥)⟩)
8	5, 7	eqtrdi 2817	. . 3 ⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) = ran (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ ⟨𝑥, ((𝐴 ↾ 𝐵)‘𝑥)⟩))
9		opex 5450	. . . . . 6 ⊢ ⟨𝑥, ((𝐴 ↾ 𝐵)‘𝑥)⟩ ∈ V
10		eqid 2766	. . . . . 6 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ ⟨𝑥, ((𝐴 ↾ 𝐵)‘𝑥)⟩) = (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ ⟨𝑥, ((𝐴 ↾ 𝐵)‘𝑥)⟩)
11	9, 10	dmmpti 6686	. . . . 5 ⊢ dom (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ ⟨𝑥, ((𝐴 ↾ 𝐵)‘𝑥)⟩) = dom (𝐴 ↾ 𝐵)
12	11	imaeq2i 6065	. . . 4 ⊢ ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ ⟨𝑥, ((𝐴 ↾ 𝐵)‘𝑥)⟩) “ dom (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ ⟨𝑥, ((𝐴 ↾ 𝐵)‘𝑥)⟩)) = ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ ⟨𝑥, ((𝐴 ↾ 𝐵)‘𝑥)⟩) “ dom (𝐴 ↾ 𝐵))
13		imadmrn 6077	. . . 4 ⊢ ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ ⟨𝑥, ((𝐴 ↾ 𝐵)‘𝑥)⟩) “ dom (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ ⟨𝑥, ((𝐴 ↾ 𝐵)‘𝑥)⟩)) = ran (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ ⟨𝑥, ((𝐴 ↾ 𝐵)‘𝑥)⟩)
14	12, 13	eqtr3i 2791	. . 3 ⊢ ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ ⟨𝑥, ((𝐴 ↾ 𝐵)‘𝑥)⟩) “ dom (𝐴 ↾ 𝐵)) = ran (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ ⟨𝑥, ((𝐴 ↾ 𝐵)‘𝑥)⟩)
15	8, 14	eqtr4di 2819	. 2 ⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) = ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ ⟨𝑥, ((𝐴 ↾ 𝐵)‘𝑥)⟩) “ dom (𝐴 ↾ 𝐵)))
16		funmpt 6581	. . 3 ⊢ Fun (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ ⟨𝑥, ((𝐴 ↾ 𝐵)‘𝑥)⟩)
17		dmresexg 6018	. . . 4 ⊢ (𝐵 ∈ 𝐶 → dom (𝐴 ↾ 𝐵) ∈ V)
18	17	adantl 487	. . 3 ⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → dom (𝐴 ↾ 𝐵) ∈ V)
19		funimaexg 6629	. . 3 ⊢ ((Fun (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ ⟨𝑥, ((𝐴 ↾ 𝐵)‘𝑥)⟩) ∧ dom (𝐴 ↾ 𝐵) ∈ V) → ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ ⟨𝑥, ((𝐴 ↾ 𝐵)‘𝑥)⟩) “ dom (𝐴 ↾ 𝐵)) ∈ V)
20	16, 18, 19	sylancr 599	. 2 ⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ ⟨𝑥, ((𝐴 ↾ 𝐵)‘𝑥)⟩) “ dom (𝐴 ↾ 𝐵)) ∈ V)
21	15, 20	eqeltrd 2866	1 ⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) ∈ V)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  Vcvv 3458  ⟨cop 4600   ↦ cmpt 5197  dom cdm 5666  ran crn 5667   ↾ cres 5668   “ cima 5669  Fun wfun 6537   Fn wfn 6538  ‘cfv 6543

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-rep 5243  ax-sep 5262  ax-nul 5274  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551

This theorem is used by:  resiexd  7221  fnex  7222  ofexg  7692  cofunexg  7955  frrlem13  8304  naddcllem  8671  dfac8alem  10032  dfac12lem1  10146  cfsmolem  10272  alephsing  10278  itunifval  10418  zorn2lem1  10498  ttukeylem3  10513  imadomg  10536  wunex2  10741  inar1  10778  axdc4uzlem  14039  hashf1rn  14408  bpolylem  16127  1stf1  18273  1stf2  18274  2ndf1  18276  2ndf2  18277  1stfcl  18278  2ndfcl  18279  gsumzadd  20023  dfrngc2  20764  dfringc2  20793  rngcresringcat  20805  madeval  28062  addsval  28192  negsval  28255  mulsval  28339  oldfib  28607  gblacfnacd  35610  onvf1odlem3  35613  satf  35866  nmulprop  36703  tendo02  41602  dnnumch1  43812  aomclem6  43827  grimidvtxedg  48691  uhgrimisgrgric  48737  fdivval  49360  fucoelvv  50139