Metamath Proof Explorer

Theorem relmptopab

Description: Any function to sets of ordered pairs produces a relation on function value unconditionally. (Contributed by Mario Carneiro, 7-Aug-2014) (Proof shortened by Mario Carneiro, 24-Dec-2016)

Ref Expression
Hypothesis relmptopab.1 ${⊢}{F}=\left({x}\in {A}⟼\left\{⟨{y},{z}⟩|{\phi }\right\}\right)$
Assertion relmptopab ${⊢}\mathrm{Rel}{F}\left({B}\right)$

Proof

Step Hyp Ref Expression
1 relmptopab.1 ${⊢}{F}=\left({x}\in {A}⟼\left\{⟨{y},{z}⟩|{\phi }\right\}\right)$
2 1 fvmptss ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left\{⟨{y},{z}⟩|{\phi }\right\}\subseteq \mathrm{V}×\mathrm{V}\to {F}\left({B}\right)\subseteq \mathrm{V}×\mathrm{V}$
3 relopab ${⊢}\mathrm{Rel}\left\{⟨{y},{z}⟩|{\phi }\right\}$
4 df-rel ${⊢}\mathrm{Rel}\left\{⟨{y},{z}⟩|{\phi }\right\}↔\left\{⟨{y},{z}⟩|{\phi }\right\}\subseteq \mathrm{V}×\mathrm{V}$
5 3 4 mpbi ${⊢}\left\{⟨{y},{z}⟩|{\phi }\right\}\subseteq \mathrm{V}×\mathrm{V}$
6 5 a1i ${⊢}{x}\in {A}\to \left\{⟨{y},{z}⟩|{\phi }\right\}\subseteq \mathrm{V}×\mathrm{V}$
7 2 6 mprg ${⊢}{F}\left({B}\right)\subseteq \mathrm{V}×\mathrm{V}$
8 df-rel ${⊢}\mathrm{Rel}{F}\left({B}\right)↔{F}\left({B}\right)\subseteq \mathrm{V}×\mathrm{V}$
9 7 8 mpbir ${⊢}\mathrm{Rel}{F}\left({B}\right)$