| 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 6659 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) | |
| 2 | ffvelcdm 7023 | . . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) | |
| 3 | 2 | ralrimiva 3126 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) |
| 4 | 1, 3 | jca 511 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) |
| 5 | simpl 482 | . . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴) | |
| 6 | fvelrnb 6891 | . . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦)) | |
| 7 | 6 | biimpd 229 | . . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦)) |
| 8 | nfra1 3258 | . . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 | |
| 9 | nfv 1915 | . . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵 | |
| 10 | rsp 3222 | . . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵)) | |
| 11 | eleq1 2821 | . . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)) | |
| 12 | 11 | biimpcd 249 | . . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐵 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)) |
| 13 | 10, 12 | syl6 35 | . . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))) |
| 14 | 8, 9, 13 | rexlimd 3241 | . . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)) |
| 15 | 7, 14 | sylan9 507 | . . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐵)) |
| 16 | 15 | ssrdv 3937 | . . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵) |
| 17 | df-f 6493 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) | |
| 18 | 5, 16, 17 | sylanbrc 583 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹:𝐴⟶𝐵) |
| 19 | 4, 18 | impbii 209 | 1 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1541 ∈ wcel 2113 ∀wral 3049 ∃wrex 3058 ⊆ wss 3899 ran crn 5622 Fn wfn 6484 ⟶wf 6485 ‘cfv 6489 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-sep 5238 ax-nul 5248 ax-pr 5374 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2883 df-ne 2931 df-ral 3050 df-rex 3059 df-rab 3398 df-v 3440 df-dif 3902 df-un 3904 df-ss 3916 df-nul 4285 df-if 4477 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4861 df-br 5096 df-opab 5158 df-mpt 5177 df-id 5516 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-iota 6445 df-fun 6491 df-fn 6492 df-f 6493 df-fv 6497 |
| This theorem is referenced by: ffnfvf 7062 fnfvrnss 7063 fcdmssb 7064 fmpt2d 7066 fssrescdmd 7068 fconstfv 7155 ffnov 7481 seqomlem2 8379 naddf 8605 elixpconst 8838 elixpsn 8870 unblem4 9189 ordtypelem4 9417 oismo 9436 cantnfvalf 9565 rankf 9697 alephon 9970 alephf1 9986 alephf1ALT 10004 alephfplem4 10008 cfsmolem 10171 infpssrlem3 10206 axcc4 10340 domtriomlem 10343 pwfseqlem3 10561 gch3 10577 inar1 10676 peano5nni 12138 cnref1o 12893 seqf2 13938 hashkf 14249 iswrdsymb 14448 ccatrn 14507 shftf 14996 sqrtf 15281 isercoll2 15586 eff2 16018 reeff1 16039 1arith 16849 ramcl 16951 xpscf 17479 dmaf 17966 cdaf 17967 coapm 17988 odf 19459 gsumpt 19884 dprdff 19936 dprdfcntz 19939 dprdfadd 19944 dprdlub 19950 rngmgpf 20085 mgpf 20176 prdscrngd 20250 isabvd 20737 psgnghm 21527 frlmsslsp 21743 psrbagcon 21872 mvrf2 21940 subrgmvrf 21979 mplbas2 21987 kqf 23672 fmf 23870 tmdgsum2 24021 prdstmdd 24049 prdstgpd 24050 prdsxmslem2 24454 metdsre 24779 evth 24895 evthicc2 25398 ovolfsf 25409 ovolf 25420 vitalilem2 25547 vitalilem5 25550 0plef 25610 mbfi1fseqlem4 25656 xrge0f 25669 itg2addlem 25696 dvfre 25892 dvne0 25953 mdegxrf 26010 mtest 26350 psercn 26373 recosf1o 26481 logcn 26593 amgm 26938 emcllem7 26949 dchrfi 27203 dchr1re 27211 dchrisum0re 27461 padicabvf 27579 addsf 27935 negsf 28004 noseqind 28232 vtxdgfisf 29466 hlimf 31228 pjrni 31693 pjmf1 31707 2ndresdju 32642 nsgmgc 33388 mplvrpmrhm 33588 reprinfz1 34646 reprdifc 34651 bnj149 34898 subfacp1lem3 35237 mrsubrn 35568 msrf 35597 mclsind 35625 neibastop2lem 36415 weiunlem2 36518 rrncmslem 37882 cdlemk56 41080 sticksstones22 42271 hbtlem7 43232 dgraaf 43254 deg1mhm 43307 elixpconstg 45200 elmapsnd 45315 unirnmap 45319 resincncf 45987 dvnprodlem1 46058 volioof 46099 voliooicof 46108 qndenserrnbllem 46406 subsaliuncllem 46469 fge0iccico 46482 elhoi 46654 ovnsubaddlem1 46682 hoiqssbllem3 46736 ovolval4lem1 46761 rrx2xpref1o 48833 oppff1 49263 fucofulem2 49426 |
| Copyright terms: Public domain | W3C validator |