Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > resfunexg | Structured version Visualization version GIF version |
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 |
---|---|
resfunexg | ⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | funres 6390 | . . . . . . 7 ⊢ (Fun 𝐴 → Fun (𝐴 ↾ 𝐵)) | |
2 | 1 | adantr 481 | . . . . . 6 ⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → Fun (𝐴 ↾ 𝐵)) |
3 | 2 | funfnd 6379 | . . . . 5 ⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) Fn dom (𝐴 ↾ 𝐵)) |
4 | dffn5 6717 | . . . . 5 ⊢ ((𝐴 ↾ 𝐵) Fn dom (𝐴 ↾ 𝐵) ↔ (𝐴 ↾ 𝐵) = (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ ((𝐴 ↾ 𝐵)‘𝑥))) | |
5 | 3, 4 | sylib 219 | . . . 4 ⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) = (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ ((𝐴 ↾ 𝐵)‘𝑥))) |
6 | fvex 6676 | . . . . 5 ⊢ ((𝐴 ↾ 𝐵)‘𝑥) ∈ V | |
7 | 6 | fnasrn 6899 | . . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ ((𝐴 ↾ 𝐵)‘𝑥)) = ran (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) |
8 | 5, 7 | syl6eq 2869 | . . 3 ⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) = ran (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉)) |
9 | opex 5347 | . . . . . 6 ⊢ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉 ∈ V | |
10 | eqid 2818 | . . . . . 6 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) = (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) | |
11 | 9, 10 | dmmpti 6485 | . . . . 5 ⊢ dom (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) = dom (𝐴 ↾ 𝐵) |
12 | 11 | imaeq2i 5920 | . . . 4 ⊢ ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) “ dom (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉)) = ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) “ dom (𝐴 ↾ 𝐵)) |
13 | imadmrn 5932 | . . . 4 ⊢ ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) “ dom (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉)) = ran (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) | |
14 | 12, 13 | eqtr3i 2843 | . . 3 ⊢ ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) “ dom (𝐴 ↾ 𝐵)) = ran (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) |
15 | 8, 14 | syl6eqr 2871 | . 2 ⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) = ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) “ dom (𝐴 ↾ 𝐵))) |
16 | funmpt 6386 | . . 3 ⊢ Fun (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) | |
17 | dmresexg 5870 | . . . 4 ⊢ (𝐵 ∈ 𝐶 → dom (𝐴 ↾ 𝐵) ∈ V) | |
18 | 17 | adantl 482 | . . 3 ⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → dom (𝐴 ↾ 𝐵) ∈ V) |
19 | funimaexg 6433 | . . 3 ⊢ ((Fun (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) ∧ dom (𝐴 ↾ 𝐵) ∈ V) → ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) “ dom (𝐴 ↾ 𝐵)) ∈ V) | |
20 | 16, 18, 19 | sylancr 587 | . 2 ⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) “ dom (𝐴 ↾ 𝐵)) ∈ V) |
21 | 15, 20 | eqeltrd 2910 | 1 ⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1528 ∈ wcel 2105 Vcvv 3492 〈cop 4563 ↦ cmpt 5137 dom cdm 5548 ran crn 5549 ↾ cres 5550 “ cima 5551 Fun wfun 6342 Fn wfn 6343 ‘cfv 6348 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-rep 5181 ax-sep 5194 ax-nul 5201 ax-pr 5320 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2615 df-eu 2647 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ne 3014 df-ral 3140 df-rex 3141 df-reu 3142 df-rab 3144 df-v 3494 df-sbc 3770 df-csb 3881 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4831 df-iun 4912 df-br 5058 df-opab 5120 df-mpt 5138 df-id 5453 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-rn 5559 df-res 5560 df-ima 5561 df-iota 6307 df-fun 6350 df-fn 6351 df-f 6352 df-f1 6353 df-fo 6354 df-f1o 6355 df-fv 6356 |
This theorem is referenced by: resiexd 6970 fnex 6971 ofexg 7402 cofunexg 7639 dfac8alem 9443 dfac12lem1 9557 cfsmolem 9680 alephsing 9686 itunifval 9826 zorn2lem1 9906 ttukeylem3 9921 imadomg 9944 wunex2 10148 inar1 10185 axdc4uzlem 13339 hashf1rn 13701 bpolylem 15390 1stf1 17430 1stf2 17431 2ndf1 17433 2ndf2 17434 1stfcl 17435 2ndfcl 17436 gsumzadd 18971 satf 32497 frrlem13 33032 madeval 33186 tendo02 37803 dnnumch1 39522 aomclem6 39537 dfrngc2 44171 dfringc2 44217 rngcresringcat 44229 fdivval 44527 |
Copyright terms: Public domain | W3C validator |