![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ffnfv | Structured version Visualization version GIF version |
Description: A function maps to a class to which all values belong. (Contributed by NM, 3-Dec-2003.) |
Ref | Expression |
---|---|
ffnfv | ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ffn 6282 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) | |
2 | ffvelrn 6611 | . . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) | |
3 | 2 | ralrimiva 3175 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) |
4 | 1, 3 | jca 507 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) |
5 | simpl 476 | . . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴) | |
6 | fvelrnb 6494 | . . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦)) | |
7 | 6 | biimpd 221 | . . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦)) |
8 | nfra1 3150 | . . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 | |
9 | nfv 2013 | . . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵 | |
10 | rsp 3138 | . . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵)) | |
11 | eleq1 2894 | . . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)) | |
12 | 11 | biimpcd 241 | . . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐵 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)) |
13 | 10, 12 | syl6 35 | . . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))) |
14 | 8, 9, 13 | rexlimd 3235 | . . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)) |
15 | 7, 14 | sylan9 503 | . . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐵)) |
16 | 15 | ssrdv 3833 | . . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵) |
17 | df-f 6131 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) | |
18 | 5, 16, 17 | sylanbrc 578 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹:𝐴⟶𝐵) |
19 | 4, 18 | impbii 201 | 1 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 = wceq 1656 ∈ wcel 2164 ∀wral 3117 ∃wrex 3118 ⊆ wss 3798 ran crn 5347 Fn wfn 6122 ⟶wf 6123 ‘cfv 6127 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-13 2389 ax-ext 2803 ax-sep 5007 ax-nul 5015 ax-pr 5129 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-3an 1113 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-mo 2605 df-eu 2640 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-ral 3122 df-rex 3123 df-rab 3126 df-v 3416 df-sbc 3663 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-nul 4147 df-if 4309 df-sn 4400 df-pr 4402 df-op 4406 df-uni 4661 df-br 4876 df-opab 4938 df-mpt 4955 df-id 5252 df-xp 5352 df-rel 5353 df-cnv 5354 df-co 5355 df-dm 5356 df-rn 5357 df-iota 6090 df-fun 6129 df-fn 6130 df-f 6131 df-fv 6135 |
This theorem is referenced by: ffnfvf 6643 fnfvrnss 6644 frnssb 6645 fmpt2d 6647 fconstfv 6737 ffnov 7029 seqomlem2 7817 elixpconst 8189 elixpsn 8220 unblem4 8490 ordtypelem4 8702 oismo 8721 cantnfvalf 8846 rankf 8941 alephon 9212 alephf1 9228 alephf1ALT 9246 alephfplem4 9250 cfsmolem 9414 infpssrlem3 9449 axcc4 9583 domtriomlem 9586 axdclem2 9664 pwfseqlem3 9804 gch3 9820 inar1 9919 peano5nni 11360 cnref1o 12114 seqf2 13121 hashkf 13419 iswrdsymb 13598 ccatrn 13656 shftf 14203 sqrtf 14487 isercoll2 14783 eff2 15208 reeff1 15229 1arith 16009 ramcl 16111 xpscf 16586 dmaf 17058 cdaf 17059 coapm 17080 odf 18314 gsumpt 18721 dprdff 18772 dprdfcntz 18775 dprdfadd 18780 dprdlub 18786 mgpf 18920 prdscrngd 18974 isabvd 19183 psrbagcon 19739 subrgmvrf 19830 mplbas2 19838 mvrf2 19859 psgnghm 20292 frlmsslsp 20509 kqf 21928 fmf 22126 tmdgsum2 22277 prdstmdd 22304 prdstgpd 22305 prdsxmslem2 22711 metdsre 23033 evth 23135 evthicc2 23633 ovolfsf 23644 ovolf 23655 vitalilem2 23782 vitalilem5 23785 0plef 23845 mbfi1fseqlem4 23891 xrge0f 23904 itg2addlem 23931 dvfre 24120 dvne0 24180 mdegxrf 24234 mtest 24564 psercn 24586 recosf1o 24688 logcn 24799 amgm 25137 emcllem7 25148 dchrfi 25400 dchr1re 25408 dchrisum0re 25622 padicabvf 25740 vtxdgfisf 26781 wlkresOLD 26978 hlimf 28645 pjrni 29112 pjmf1 29126 reprinfz1 31245 reprdifc 31250 bnj149 31487 subfacp1lem3 31706 mrsubrn 31952 msrf 31981 mclsind 32009 neibastop2lem 32888 rrncmslem 34168 cdlemk56 37041 hbtlem7 38533 dgraaf 38555 deg1mhm 38623 elixpconstg 40078 elmapsnd 40197 unirnmap 40201 resincncf 40877 dvnprodlem1 40950 volioof 40992 voliooicof 41001 qndenserrnbllem 41299 subsaliuncllem 41360 fge0iccico 41372 elhoi 41544 ovnsubaddlem1 41572 hoiqssbllem3 41626 ovolval4lem1 41651 rrx2xpref1o 42276 |
Copyright terms: Public domain | W3C validator |