![]() |
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 6179 | . . . . . . 7 ⊢ (Fun 𝐴 → Fun (𝐴 ↾ 𝐵)) | |
2 | 1 | adantr 474 | . . . . . 6 ⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → Fun (𝐴 ↾ 𝐵)) |
3 | 2 | funfnd 6168 | . . . . 5 ⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) Fn dom (𝐴 ↾ 𝐵)) |
4 | dffn5 6503 | . . . . 5 ⊢ ((𝐴 ↾ 𝐵) Fn dom (𝐴 ↾ 𝐵) ↔ (𝐴 ↾ 𝐵) = (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ ((𝐴 ↾ 𝐵)‘𝑥))) | |
5 | 3, 4 | sylib 210 | . . . 4 ⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) = (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ ((𝐴 ↾ 𝐵)‘𝑥))) |
6 | fvex 6461 | . . . . 5 ⊢ ((𝐴 ↾ 𝐵)‘𝑥) ∈ V | |
7 | 6 | fnasrn 6678 | . . . 4 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ ((𝐴 ↾ 𝐵)‘𝑥)) = ran (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) |
8 | 5, 7 | syl6eq 2830 | . . 3 ⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) = ran (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉)) |
9 | opex 5166 | . . . . . 6 ⊢ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉 ∈ V | |
10 | eqid 2778 | . . . . . 6 ⊢ (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) = (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) | |
11 | 9, 10 | dmmpti 6271 | . . . . 5 ⊢ dom (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) = dom (𝐴 ↾ 𝐵) |
12 | 11 | imaeq2i 5720 | . . . 4 ⊢ ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) “ dom (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉)) = ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) “ dom (𝐴 ↾ 𝐵)) |
13 | imadmrn 5732 | . . . 4 ⊢ ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) “ dom (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉)) = ran (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) | |
14 | 12, 13 | eqtr3i 2804 | . . 3 ⊢ ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) “ dom (𝐴 ↾ 𝐵)) = ran (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) |
15 | 8, 14 | syl6eqr 2832 | . 2 ⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) = ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) “ dom (𝐴 ↾ 𝐵))) |
16 | funmpt 6175 | . . 3 ⊢ Fun (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) | |
17 | dmresexg 5672 | . . . 4 ⊢ (𝐵 ∈ 𝐶 → dom (𝐴 ↾ 𝐵) ∈ V) | |
18 | 17 | adantl 475 | . . 3 ⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → dom (𝐴 ↾ 𝐵) ∈ V) |
19 | funimaexg 6222 | . . 3 ⊢ ((Fun (𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) ∧ dom (𝐴 ↾ 𝐵) ∈ V) → ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) “ dom (𝐴 ↾ 𝐵)) ∈ V) | |
20 | 16, 18, 19 | sylancr 581 | . 2 ⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → ((𝑥 ∈ dom (𝐴 ↾ 𝐵) ↦ 〈𝑥, ((𝐴 ↾ 𝐵)‘𝑥)〉) “ dom (𝐴 ↾ 𝐵)) ∈ V) |
21 | 15, 20 | eqeltrd 2859 | 1 ⊢ ((Fun 𝐴 ∧ 𝐵 ∈ 𝐶) → (𝐴 ↾ 𝐵) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 = wceq 1601 ∈ wcel 2107 Vcvv 3398 〈cop 4404 ↦ cmpt 4967 dom cdm 5357 ran crn 5358 ↾ cres 5359 “ cima 5360 Fun wfun 6131 Fn wfn 6132 ‘cfv 6137 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-rep 5008 ax-sep 5019 ax-nul 5027 ax-pr 5140 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ne 2970 df-ral 3095 df-rex 3096 df-reu 3097 df-rab 3099 df-v 3400 df-sbc 3653 df-csb 3752 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4674 df-iun 4757 df-br 4889 df-opab 4951 df-mpt 4968 df-id 5263 df-xp 5363 df-rel 5364 df-cnv 5365 df-co 5366 df-dm 5367 df-rn 5368 df-res 5369 df-ima 5370 df-iota 6101 df-fun 6139 df-fn 6140 df-f 6141 df-f1 6142 df-fo 6143 df-f1o 6144 df-fv 6145 |
This theorem is referenced by: resiexd 6754 fnex 6755 ofexg 7180 cofunexg 7411 dfac8alem 9187 dfac12lem1 9302 cfsmolem 9429 alephsing 9435 itunifval 9575 zorn2lem1 9655 ttukeylem3 9670 imadomg 9693 wunex2 9897 inar1 9934 axdc4uzlem 13105 hashf1rn 13462 bpolylem 15185 1stf1 17222 1stf2 17223 2ndf1 17225 2ndf2 17226 1stfcl 17227 2ndfcl 17228 gsumzadd 18712 wlkreslemOLD 27024 madeval 32528 tendo02 36946 dnnumch1 38583 aomclem6 38598 dfrngc2 42997 dfringc2 43043 rngcresringcat 43055 fdivval 43358 |
Copyright terms: Public domain | W3C validator |