![]() |
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 6278 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) | |
2 | ffvelrn 6606 | . . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) | |
3 | 2 | ralrimiva 3175 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) |
4 | 1, 3 | jca 509 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) |
5 | simpl 476 | . . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴) | |
6 | fvelrnb 6490 | . . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦)) | |
7 | 6 | biimpd 221 | . . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦)) |
8 | nfra1 3150 | . . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 | |
9 | nfv 2015 | . . . . . 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 505 | . . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐵)) |
16 | 15 | ssrdv 3833 | . . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵) |
17 | df-f 6127 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) | |
18 | 5, 16, 17 | sylanbrc 580 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹:𝐴⟶𝐵) |
19 | 4, 18 | impbii 201 | 1 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 = wceq 1658 ∈ wcel 2166 ∀wral 3117 ∃wrex 3118 ⊆ wss 3798 ran crn 5343 Fn wfn 6118 ⟶wf 6119 ‘cfv 6123 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2803 ax-sep 5005 ax-nul 5013 ax-pr 5127 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 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 4145 df-if 4307 df-sn 4398 df-pr 4400 df-op 4404 df-uni 4659 df-br 4874 df-opab 4936 df-mpt 4953 df-id 5250 df-xp 5348 df-rel 5349 df-cnv 5350 df-co 5351 df-dm 5352 df-rn 5353 df-iota 6086 df-fun 6125 df-fn 6126 df-f 6127 df-fv 6131 |
This theorem is referenced by: ffnfvf 6638 fnfvrnss 6639 frnssb 6640 fmpt2d 6642 fconstfv 6732 ffnov 7024 seqomlem2 7812 elixpconst 8183 elixpsn 8214 unblem4 8484 ordtypelem4 8695 oismo 8714 cantnfvalf 8839 rankf 8934 alephon 9205 alephf1 9221 alephf1ALT 9239 alephfplem4 9243 cfsmolem 9407 infpssrlem3 9442 axcc4 9576 domtriomlem 9579 axdclem2 9657 pwfseqlem3 9797 gch3 9813 inar1 9912 peano5nni 11353 cnref1o 12107 seqf2 13114 hashkf 13412 iswrdsymb 13591 ccatrn 13649 shftf 14196 sqrtf 14480 isercoll2 14776 eff2 15201 reeff1 15222 1arith 16002 ramcl 16104 xpscf 16579 dmaf 17051 cdaf 17052 coapm 17073 odf 18307 gsumpt 18714 dprdff 18765 dprdfcntz 18768 dprdfadd 18773 dprdlub 18779 mgpf 18913 prdscrngd 18967 isabvd 19176 psrbagcon 19732 subrgmvrf 19823 mplbas2 19831 mvrf2 19852 psgnghm 20285 frlmsslsp 20502 kqf 21921 fmf 22119 tmdgsum2 22270 prdstmdd 22297 prdstgpd 22298 prdsxmslem2 22704 metdsre 23026 evth 23128 evthicc2 23626 ovolfsf 23637 ovolf 23648 vitalilem2 23775 vitalilem5 23778 0plef 23838 mbfi1fseqlem4 23884 xrge0f 23897 itg2addlem 23924 dvfre 24113 dvne0 24173 mdegxrf 24227 mtest 24557 psercn 24579 recosf1o 24681 logcn 24792 amgm 25130 emcllem7 25141 dchrfi 25393 dchr1re 25401 dchrisum0re 25615 padicabvf 25733 vtxdgfisf 26774 wlkresOLD 26971 hlimf 28649 pjrni 29116 pjmf1 29130 reprinfz1 31249 reprdifc 31254 bnj149 31491 subfacp1lem3 31710 mrsubrn 31956 msrf 31985 mclsind 32013 neibastop2lem 32893 rrncmslem 34173 cdlemk56 37046 hbtlem7 38538 dgraaf 38560 deg1mhm 38628 elixpconstg 40083 elmapsnd 40202 unirnmap 40206 resincncf 40883 dvnprodlem1 40956 volioof 40998 voliooicof 41007 qndenserrnbllem 41305 subsaliuncllem 41366 fge0iccico 41378 elhoi 41550 ovnsubaddlem1 41578 hoiqssbllem3 41632 ovolval4lem1 41657 |
Copyright terms: Public domain | W3C validator |