![]() |
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 6673 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) | |
2 | ffvelcdm 7037 | . . . 4 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) | |
3 | 2 | ralrimiva 3144 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) |
4 | 1, 3 | jca 513 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) |
5 | simpl 484 | . . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹 Fn 𝐴) | |
6 | fvelrnb 6908 | . . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦)) | |
7 | 6 | biimpd 228 | . . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦)) |
8 | nfra1 3270 | . . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 | |
9 | nfv 1918 | . . . . . 6 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵 | |
10 | rsp 3233 | . . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → (𝐹‘𝑥) ∈ 𝐵)) | |
11 | eleq1 2826 | . . . . . . . 8 ⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)) | |
12 | 11 | biimpcd 249 | . . . . . . 7 ⊢ ((𝐹‘𝑥) ∈ 𝐵 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)) |
13 | 10, 12 | syl6 35 | . . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵))) |
14 | 8, 9, 13 | rexlimd 3252 | . . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵 → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦 → 𝑦 ∈ 𝐵)) |
15 | 7, 14 | sylan9 509 | . . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝐵)) |
16 | 15 | ssrdv 3955 | . . 3 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → ran 𝐹 ⊆ 𝐵) |
17 | df-f 6505 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) | |
18 | 5, 16, 17 | sylanbrc 584 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) → 𝐹:𝐴⟶𝐵) |
19 | 4, 18 | impbii 208 | 1 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 ∈ wcel 2107 ∀wral 3065 ∃wrex 3074 ⊆ wss 3915 ran crn 5639 Fn wfn 6496 ⟶wf 6497 ‘cfv 6501 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2708 ax-sep 5261 ax-nul 5268 ax-pr 5389 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2890 df-ne 2945 df-ral 3066 df-rex 3075 df-rab 3411 df-v 3450 df-dif 3918 df-un 3920 df-in 3922 df-ss 3932 df-nul 4288 df-if 4492 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4871 df-br 5111 df-opab 5173 df-mpt 5194 df-id 5536 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-iota 6453 df-fun 6503 df-fn 6504 df-f 6505 df-fv 6509 |
This theorem is referenced by: ffnfvf 7072 fnfvrnss 7073 fcdmssb 7074 fmpt2d 7076 fconstfv 7167 ffnov 7488 seqomlem2 8402 naddf 8632 elixpconst 8850 elixpsn 8882 unblem4 9249 ordtypelem4 9464 oismo 9483 cantnfvalf 9608 rankf 9737 alephon 10012 alephf1 10028 alephf1ALT 10046 alephfplem4 10050 cfsmolem 10213 infpssrlem3 10248 axcc4 10382 domtriomlem 10385 pwfseqlem3 10603 gch3 10619 inar1 10718 peano5nni 12163 cnref1o 12917 seqf2 13934 hashkf 14239 iswrdsymb 14426 ccatrn 14484 shftf 14971 sqrtf 15255 isercoll2 15560 eff2 15988 reeff1 16009 1arith 16806 ramcl 16908 xpscf 17454 dmaf 17942 cdaf 17943 coapm 17964 odf 19326 gsumpt 19746 dprdff 19798 dprdfcntz 19801 dprdfadd 19806 dprdlub 19812 mgpf 19986 prdscrngd 20044 isabvd 20295 psgnghm 21000 frlmsslsp 21218 psrbagcon 21348 psrbagconOLD 21349 subrgmvrf 21451 mplbas2 21459 mvrf2 21484 kqf 23114 fmf 23312 tmdgsum2 23463 prdstmdd 23491 prdstgpd 23492 prdsxmslem2 23901 metdsre 24232 evth 24338 evthicc2 24840 ovolfsf 24851 ovolf 24862 vitalilem2 24989 vitalilem5 24992 0plef 25052 mbfi1fseqlem4 25099 xrge0f 25112 itg2addlem 25139 dvfre 25331 dvne0 25391 mdegxrf 25449 mtest 25779 psercn 25801 recosf1o 25907 logcn 26018 amgm 26356 emcllem7 26367 dchrfi 26619 dchr1re 26627 dchrisum0re 26877 padicabvf 26995 addsf 27314 negsf 27369 vtxdgfisf 28466 hlimf 30221 pjrni 30686 pjmf1 30700 2ndresdju 31607 nsgmgc 32230 reprinfz1 33275 reprdifc 33280 bnj149 33527 subfacp1lem3 33816 mrsubrn 34147 msrf 34176 mclsind 34204 neibastop2lem 34861 rrncmslem 36320 cdlemk56 39463 sticksstones22 40605 hbtlem7 41481 dgraaf 41503 deg1mhm 41563 elixpconstg 43373 elmapsnd 43499 unirnmap 43503 resincncf 44190 dvnprodlem1 44261 volioof 44302 voliooicof 44311 qndenserrnbllem 44609 subsaliuncllem 44672 fge0iccico 44685 elhoi 44857 ovnsubaddlem1 44885 hoiqssbllem3 44939 ovolval4lem1 44964 rrx2xpref1o 46878 |
Copyright terms: Public domain | W3C validator |