Metamath Proof Explorer

Theorem ffnfv

Description: A function maps to a class to which all values belong. (Contributed by NM, 3-Dec-2003)

Ref Expression
Assertion ffnfv ${⊢}{F}:{A}⟶{B}↔\left({F}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}\right)$

Proof

Step Hyp Ref Expression
1 ffn ${⊢}{F}:{A}⟶{B}\to {F}Fn{A}$
2 ffvelrn ${⊢}\left({F}:{A}⟶{B}\wedge {x}\in {A}\right)\to {F}\left({x}\right)\in {B}$
3 2 ralrimiva ${⊢}{F}:{A}⟶{B}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}$
4 1 3 jca ${⊢}{F}:{A}⟶{B}\to \left({F}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}\right)$
5 simpl ${⊢}\left({F}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}\right)\to {F}Fn{A}$
6 fvelrnb ${⊢}{F}Fn{A}\to \left({y}\in \mathrm{ran}{F}↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={y}\right)$
7 6 biimpd ${⊢}{F}Fn{A}\to \left({y}\in \mathrm{ran}{F}\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={y}\right)$
8 nfra1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}$
9 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}\in {B}$
10 rsp ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}\to \left({x}\in {A}\to {F}\left({x}\right)\in {B}\right)$
11 eleq1 ${⊢}{F}\left({x}\right)={y}\to \left({F}\left({x}\right)\in {B}↔{y}\in {B}\right)$
12 11 biimpcd ${⊢}{F}\left({x}\right)\in {B}\to \left({F}\left({x}\right)={y}\to {y}\in {B}\right)$
13 10 12 syl6 ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}\to \left({x}\in {A}\to \left({F}\left({x}\right)={y}\to {y}\in {B}\right)\right)$
14 8 9 13 rexlimd ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={y}\to {y}\in {B}\right)$
15 7 14 sylan9 ${⊢}\left({F}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}\right)\to \left({y}\in \mathrm{ran}{F}\to {y}\in {B}\right)$
16 15 ssrdv ${⊢}\left({F}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}\right)\to \mathrm{ran}{F}\subseteq {B}$
17 df-f ${⊢}{F}:{A}⟶{B}↔\left({F}Fn{A}\wedge \mathrm{ran}{F}\subseteq {B}\right)$
18 5 16 17 sylanbrc ${⊢}\left({F}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}\right)\to {F}:{A}⟶{B}$
19 4 18 impbii ${⊢}{F}:{A}⟶{B}↔\left({F}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}\right)$