# Metamath Proof Explorer

## Theorem fvmptrabdm

Description: Value of a function mapping a set to a class abstraction restricting the value of another function. See also fvmptrabfv . (Suggested by BJ, 18-Feb-2022.) (Contributed by AV, 18-Feb-2022)

Ref Expression
Hypotheses fvmptrabdm.f ${⊢}{F}=\left({x}\in {V}⟼\left\{{y}\in {G}\left({Y}\right)|{\phi }\right\}\right)$
fvmptrabdm.r ${⊢}{x}={X}\to \left({\phi }↔{\psi }\right)$
fvmptrabdm.v ${⊢}{Y}\in \mathrm{dom}{G}\to {X}\in \mathrm{dom}{F}$
Assertion fvmptrabdm ${⊢}{F}\left({X}\right)=\left\{{y}\in {G}\left({Y}\right)|{\psi }\right\}$

### Proof

Step Hyp Ref Expression
1 fvmptrabdm.f ${⊢}{F}=\left({x}\in {V}⟼\left\{{y}\in {G}\left({Y}\right)|{\phi }\right\}\right)$
2 fvmptrabdm.r ${⊢}{x}={X}\to \left({\phi }↔{\psi }\right)$
3 fvmptrabdm.v ${⊢}{Y}\in \mathrm{dom}{G}\to {X}\in \mathrm{dom}{F}$
4 pm2.1 ${⊢}\left(¬{X}\in \mathrm{dom}{F}\vee {X}\in \mathrm{dom}{F}\right)$
5 imor ${⊢}\left({Y}\in \mathrm{dom}{G}\to {X}\in \mathrm{dom}{F}\right)↔\left(¬{Y}\in \mathrm{dom}{G}\vee {X}\in \mathrm{dom}{F}\right)$
6 ordir ${⊢}\left(\left(¬{X}\in \mathrm{dom}{F}\wedge ¬{Y}\in \mathrm{dom}{G}\right)\vee {X}\in \mathrm{dom}{F}\right)↔\left(\left(¬{X}\in \mathrm{dom}{F}\vee {X}\in \mathrm{dom}{F}\right)\wedge \left(¬{Y}\in \mathrm{dom}{G}\vee {X}\in \mathrm{dom}{F}\right)\right)$
7 ndmfv ${⊢}¬{X}\in \mathrm{dom}{F}\to {F}\left({X}\right)=\varnothing$
8 ndmfv ${⊢}¬{Y}\in \mathrm{dom}{G}\to {G}\left({Y}\right)=\varnothing$
9 8 rabeqdv ${⊢}¬{Y}\in \mathrm{dom}{G}\to \left\{{y}\in {G}\left({Y}\right)|{\psi }\right\}=\left\{{y}\in \varnothing |{\psi }\right\}$
10 rab0 ${⊢}\left\{{y}\in \varnothing |{\psi }\right\}=\varnothing$
11 9 10 syl6req ${⊢}¬{Y}\in \mathrm{dom}{G}\to \varnothing =\left\{{y}\in {G}\left({Y}\right)|{\psi }\right\}$
12 7 11 sylan9eq ${⊢}\left(¬{X}\in \mathrm{dom}{F}\wedge ¬{Y}\in \mathrm{dom}{G}\right)\to {F}\left({X}\right)=\left\{{y}\in {G}\left({Y}\right)|{\psi }\right\}$
13 2 rabbidv ${⊢}{x}={X}\to \left\{{y}\in {G}\left({Y}\right)|{\phi }\right\}=\left\{{y}\in {G}\left({Y}\right)|{\psi }\right\}$
14 1 dmmpt ${⊢}\mathrm{dom}{F}=\left\{{x}\in {V}|\left\{{y}\in {G}\left({Y}\right)|{\phi }\right\}\in \mathrm{V}\right\}$
15 rabid2 ${⊢}{V}=\left\{{x}\in {V}|\left\{{y}\in {G}\left({Y}\right)|{\phi }\right\}\in \mathrm{V}\right\}↔\forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\left\{{y}\in {G}\left({Y}\right)|{\phi }\right\}\in \mathrm{V}$
16 fvex ${⊢}{G}\left({Y}\right)\in \mathrm{V}$
17 16 rabex ${⊢}\left\{{y}\in {G}\left({Y}\right)|{\phi }\right\}\in \mathrm{V}$
18 17 a1i ${⊢}{x}\in {V}\to \left\{{y}\in {G}\left({Y}\right)|{\phi }\right\}\in \mathrm{V}$
19 15 18 mprgbir ${⊢}{V}=\left\{{x}\in {V}|\left\{{y}\in {G}\left({Y}\right)|{\phi }\right\}\in \mathrm{V}\right\}$
20 14 19 eqtr4i ${⊢}\mathrm{dom}{F}={V}$
21 20 eleq2i ${⊢}{X}\in \mathrm{dom}{F}↔{X}\in {V}$
22 21 biimpi ${⊢}{X}\in \mathrm{dom}{F}\to {X}\in {V}$
23 16 rabex ${⊢}\left\{{y}\in {G}\left({Y}\right)|{\psi }\right\}\in \mathrm{V}$
24 23 a1i ${⊢}{X}\in \mathrm{dom}{F}\to \left\{{y}\in {G}\left({Y}\right)|{\psi }\right\}\in \mathrm{V}$
25 1 13 22 24 fvmptd3 ${⊢}{X}\in \mathrm{dom}{F}\to {F}\left({X}\right)=\left\{{y}\in {G}\left({Y}\right)|{\psi }\right\}$
26 12 25 jaoi ${⊢}\left(\left(¬{X}\in \mathrm{dom}{F}\wedge ¬{Y}\in \mathrm{dom}{G}\right)\vee {X}\in \mathrm{dom}{F}\right)\to {F}\left({X}\right)=\left\{{y}\in {G}\left({Y}\right)|{\psi }\right\}$
27 6 26 sylbir ${⊢}\left(\left(¬{X}\in \mathrm{dom}{F}\vee {X}\in \mathrm{dom}{F}\right)\wedge \left(¬{Y}\in \mathrm{dom}{G}\vee {X}\in \mathrm{dom}{F}\right)\right)\to {F}\left({X}\right)=\left\{{y}\in {G}\left({Y}\right)|{\psi }\right\}$
28 27 expcom ${⊢}\left(¬{Y}\in \mathrm{dom}{G}\vee {X}\in \mathrm{dom}{F}\right)\to \left(\left(¬{X}\in \mathrm{dom}{F}\vee {X}\in \mathrm{dom}{F}\right)\to {F}\left({X}\right)=\left\{{y}\in {G}\left({Y}\right)|{\psi }\right\}\right)$
29 5 28 sylbi ${⊢}\left({Y}\in \mathrm{dom}{G}\to {X}\in \mathrm{dom}{F}\right)\to \left(\left(¬{X}\in \mathrm{dom}{F}\vee {X}\in \mathrm{dom}{F}\right)\to {F}\left({X}\right)=\left\{{y}\in {G}\left({Y}\right)|{\psi }\right\}\right)$
30 3 4 29 mp2 ${⊢}{F}\left({X}\right)=\left\{{y}\in {G}\left({Y}\right)|{\psi }\right\}$