Metamath Proof Explorer


Theorem fvmptopab

Description: The function value of a mapping M to a restricted binary relation expressed as an ordered-pair class abstraction: The restricted binary relation is a binary relation given as value of a function F restricted by the condition ps . (Contributed by AV, 31-Jan-2021) (Revised by AV, 29-Oct-2021) Add disjoint variable condition on F , x , y to remove a sethood hypothesis. (Revised by SN, 13-Dec-2024)

Ref Expression
Hypotheses fvmptopab.1 z = Z φ ψ
fvmptopab.m M = z V x y | x F z y φ
Assertion fvmptopab M Z = x y | x F Z y ψ

Proof

Step Hyp Ref Expression
1 fvmptopab.1 z = Z φ ψ
2 fvmptopab.m M = z V x y | x F z y φ
3 fveq2 z = Z F z = F Z
4 3 breqd z = Z x F z y x F Z y
5 4 1 anbi12d z = Z x F z y φ x F Z y ψ
6 5 opabbidv z = Z x y | x F z y φ = x y | x F Z y ψ
7 opabresex2 x y | x F Z y ψ V
8 6 2 7 fvmpt Z V M Z = x y | x F Z y ψ
9 fvprc ¬ Z V M Z =
10 elopabran z x y | x F Z y ψ z F Z
11 10 ssriv x y | x F Z y ψ F Z
12 fvprc ¬ Z V F Z =
13 11 12 sseqtrid ¬ Z V x y | x F Z y ψ
14 ss0 x y | x F Z y ψ x y | x F Z y ψ =
15 13 14 syl ¬ Z V x y | x F Z y ψ =
16 9 15 eqtr4d ¬ Z V M Z = x y | x F Z y ψ
17 8 16 pm2.61i M Z = x y | x F Z y ψ