![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fnex | Structured version Visualization version GIF version |
Description: If the domain of a function is a set, the function is a set. Theorem 6.16(1) of [TakeutiZaring] p. 28. This theorem is derived using the Axiom of Replacement in the form of resfunexg 6753. See fnexALT 7413 for alternate proof. (Contributed by NM, 14-Aug-1994.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
Ref | Expression |
---|---|
fnex | ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵) → 𝐹 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fnrel 6236 | . 2 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹) | |
2 | df-fn 6140 | . . 3 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴)) | |
3 | eleq1a 2854 | . . . . . 6 ⊢ (𝐴 ∈ 𝐵 → (dom 𝐹 = 𝐴 → dom 𝐹 ∈ 𝐵)) | |
4 | 3 | impcom 398 | . . . . 5 ⊢ ((dom 𝐹 = 𝐴 ∧ 𝐴 ∈ 𝐵) → dom 𝐹 ∈ 𝐵) |
5 | resfunexg 6753 | . . . . 5 ⊢ ((Fun 𝐹 ∧ dom 𝐹 ∈ 𝐵) → (𝐹 ↾ dom 𝐹) ∈ V) | |
6 | 4, 5 | sylan2 586 | . . . 4 ⊢ ((Fun 𝐹 ∧ (dom 𝐹 = 𝐴 ∧ 𝐴 ∈ 𝐵)) → (𝐹 ↾ dom 𝐹) ∈ V) |
7 | 6 | anassrs 461 | . . 3 ⊢ (((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ∧ 𝐴 ∈ 𝐵) → (𝐹 ↾ dom 𝐹) ∈ V) |
8 | 2, 7 | sylanb 576 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵) → (𝐹 ↾ dom 𝐹) ∈ V) |
9 | resdm 5693 | . . . 4 ⊢ (Rel 𝐹 → (𝐹 ↾ dom 𝐹) = 𝐹) | |
10 | 9 | eleq1d 2844 | . . 3 ⊢ (Rel 𝐹 → ((𝐹 ↾ dom 𝐹) ∈ V ↔ 𝐹 ∈ V)) |
11 | 10 | biimpa 470 | . 2 ⊢ ((Rel 𝐹 ∧ (𝐹 ↾ dom 𝐹) ∈ V) → 𝐹 ∈ V) |
12 | 1, 8, 11 | syl2an2r 675 | 1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐵) → 𝐹 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 = wceq 1601 ∈ wcel 2107 Vcvv 3398 dom cdm 5357 ↾ cres 5359 Rel wrel 5362 Fun wfun 6131 Fn wfn 6132 |
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: funex 6756 fex 6763 offval 7183 ofrfval 7184 suppvalfn 7585 suppfnss 7603 suppfnssOLD 7604 fnsuppeq0 7607 wfrlem15 7714 fndmeng 8321 fdmfifsupp 8575 cfsmolem 9429 axcc2lem 9595 unirnfdomd 9726 prdsbas2 16526 prdsplusgval 16530 prdsmulrval 16532 prdsleval 16534 prdsdsval 16535 prdsvscaval 16536 brssc 16870 sscpwex 16871 ssclem 16875 isssc 16876 rescval2 16884 reschom 16886 rescabs 16889 isfuncd 16921 dprdw 18807 prdsmgp 19008 dsmmbas2 20491 dsmmelbas 20493 ptval 21793 elptr 21796 prdstopn 21851 qtoptop 21923 imastopn 21943 fnpreimac 30053 suppss3 30085 ofcfval 30766 dya2iocuni 30951 trpredex 32333 fnexd 40263 stoweidlem27 41185 stoweidlem59 41217 omeiunle 41672 |
Copyright terms: Public domain | W3C validator |