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 = x V y G Y | φ
fvmptrabdm.r x = X φ ψ
fvmptrabdm.v Y dom G X dom F
Assertion fvmptrabdm F X = y G Y | ψ

Proof

Step Hyp Ref Expression
1 fvmptrabdm.f F = x V y G Y | φ
2 fvmptrabdm.r x = X φ ψ
3 fvmptrabdm.v Y dom G X dom F
4 pm2.1 ¬ X dom F X dom F
5 imor Y dom G X dom F ¬ Y dom G X dom F
6 ordir ¬ X dom F ¬ Y dom G X dom F ¬ X dom F X dom F ¬ Y dom G X dom F
7 ndmfv ¬ X dom F F X =
8 ndmfv ¬ Y dom G G Y =
9 8 rabeqdv ¬ Y dom G y G Y | ψ = y | ψ
10 rab0 y | ψ =
11 9 10 syl6req ¬ Y dom G = y G Y | ψ
12 7 11 sylan9eq ¬ X dom F ¬ Y dom G F X = y G Y | ψ
13 2 rabbidv x = X y G Y | φ = y G Y | ψ
14 1 dmmpt dom F = x V | y G Y | φ V
15 rabid2 V = x V | y G Y | φ V x V y G Y | φ V
16 fvex G Y V
17 16 rabex y G Y | φ V
18 17 a1i x V y G Y | φ V
19 15 18 mprgbir V = x V | y G Y | φ V
20 14 19 eqtr4i dom F = V
21 20 eleq2i X dom F X V
22 21 biimpi X dom F X V
23 16 rabex y G Y | ψ V
24 23 a1i X dom F y G Y | ψ V
25 1 13 22 24 fvmptd3 X dom F F X = y G Y | ψ
26 12 25 jaoi ¬ X dom F ¬ Y dom G X dom F F X = y G Y | ψ
27 6 26 sylbir ¬ X dom F X dom F ¬ Y dom G X dom F F X = y G Y | ψ
28 27 expcom ¬ Y dom G X dom F ¬ X dom F X dom F F X = y G Y | ψ
29 5 28 sylbi Y dom G X dom F ¬ X dom F X dom F F X = y G Y | ψ
30 3 4 29 mp2 F X = y G Y | ψ