Metamath Proof Explorer


Theorem fvmptrab

Description: Value of a function mapping a set to a class abstraction restricting a class depending on the argument of the function. More general version of fvmptrabfv , but relying on the fact that out-of-domain arguments evaluate to the empty set, which relies on set.mm's particular encoding. (Contributed by AV, 14-Feb-2022)

Ref Expression
Hypotheses fvmptrab.f F = x V y M | φ
fvmptrab.r x = X φ ψ
fvmptrab.s x = X M = N
fvmptrab.v X V N V
fvmptrab.n X V N =
Assertion fvmptrab F X = y N | ψ

Proof

Step Hyp Ref Expression
1 fvmptrab.f F = x V y M | φ
2 fvmptrab.r x = X φ ψ
3 fvmptrab.s x = X M = N
4 fvmptrab.v X V N V
5 fvmptrab.n X V N =
6 1 a1i X V F = x V y M | φ
7 3 2 rabeqbidv x = X y M | φ = y N | ψ
8 7 adantl X V x = X y M | φ = y N | ψ
9 id X V X V
10 eqid y N | ψ = y N | ψ
11 10 4 rabexd X V y N | ψ V
12 6 8 9 11 fvmptd X V F X = y N | ψ
13 1 fvmptndm ¬ X V F X =
14 df-nel X V ¬ X V
15 rabeq N = y N | ψ = y | ψ
16 rab0 y | ψ =
17 15 16 syl6req N = = y N | ψ
18 5 17 syl X V = y N | ψ
19 14 18 sylbir ¬ X V = y N | ψ
20 13 19 eqtrd ¬ X V F X = y N | ψ
21 12 20 pm2.61i F X = y N | ψ