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 e. V |-> { y e. ( G ` Y ) | ph } )
fvmptrabdm.r 
|- ( x = X -> ( ph <-> ps ) )
fvmptrabdm.v 
|- ( Y e. dom G -> X e. dom F )
Assertion fvmptrabdm 
|- ( F ` X ) = { y e. ( G ` Y ) | ps }

Proof

Step Hyp Ref Expression
1 fvmptrabdm.f 
 |-  F = ( x e. V |-> { y e. ( G ` Y ) | ph } )
2 fvmptrabdm.r 
 |-  ( x = X -> ( ph <-> ps ) )
3 fvmptrabdm.v 
 |-  ( Y e. dom G -> X e. dom F )
4 pm2.1 
 |-  ( -. X e. dom F \/ X e. dom F )
5 imor 
 |-  ( ( Y e. dom G -> X e. dom F ) <-> ( -. Y e. dom G \/ X e. dom F ) )
6 ordir 
 |-  ( ( ( -. X e. dom F /\ -. Y e. dom G ) \/ X e. dom F ) <-> ( ( -. X e. dom F \/ X e. dom F ) /\ ( -. Y e. dom G \/ X e. dom F ) ) )
7 ndmfv 
 |-  ( -. X e. dom F -> ( F ` X ) = (/) )
8 ndmfv 
 |-  ( -. Y e. dom G -> ( G ` Y ) = (/) )
9 8 rabeqdv 
 |-  ( -. Y e. dom G -> { y e. ( G ` Y ) | ps } = { y e. (/) | ps } )
10 rab0 
 |-  { y e. (/) | ps } = (/)
11 9 10 eqtr2di 
 |-  ( -. Y e. dom G -> (/) = { y e. ( G ` Y ) | ps } )
12 7 11 sylan9eq 
 |-  ( ( -. X e. dom F /\ -. Y e. dom G ) -> ( F ` X ) = { y e. ( G ` Y ) | ps } )
13 2 rabbidv 
 |-  ( x = X -> { y e. ( G ` Y ) | ph } = { y e. ( G ` Y ) | ps } )
14 1 dmmpt 
 |-  dom F = { x e. V | { y e. ( G ` Y ) | ph } e. _V }
15 rabid2 
 |-  ( V = { x e. V | { y e. ( G ` Y ) | ph } e. _V } <-> A. x e. V { y e. ( G ` Y ) | ph } e. _V )
16 fvex 
 |-  ( G ` Y ) e. _V
17 16 rabex 
 |-  { y e. ( G ` Y ) | ph } e. _V
18 17 a1i 
 |-  ( x e. V -> { y e. ( G ` Y ) | ph } e. _V )
19 15 18 mprgbir 
 |-  V = { x e. V | { y e. ( G ` Y ) | ph } e. _V }
20 14 19 eqtr4i 
 |-  dom F = V
21 20 eleq2i 
 |-  ( X e. dom F <-> X e. V )
22 21 biimpi 
 |-  ( X e. dom F -> X e. V )
23 16 rabex 
 |-  { y e. ( G ` Y ) | ps } e. _V
24 23 a1i 
 |-  ( X e. dom F -> { y e. ( G ` Y ) | ps } e. _V )
25 1 13 22 24 fvmptd3 
 |-  ( X e. dom F -> ( F ` X ) = { y e. ( G ` Y ) | ps } )
26 12 25 jaoi 
 |-  ( ( ( -. X e. dom F /\ -. Y e. dom G ) \/ X e. dom F ) -> ( F ` X ) = { y e. ( G ` Y ) | ps } )
27 6 26 sylbir 
 |-  ( ( ( -. X e. dom F \/ X e. dom F ) /\ ( -. Y e. dom G \/ X e. dom F ) ) -> ( F ` X ) = { y e. ( G ` Y ) | ps } )
28 27 expcom 
 |-  ( ( -. Y e. dom G \/ X e. dom F ) -> ( ( -. X e. dom F \/ X e. dom F ) -> ( F ` X ) = { y e. ( G ` Y ) | ps } ) )
29 5 28 sylbi 
 |-  ( ( Y e. dom G -> X e. dom F ) -> ( ( -. X e. dom F \/ X e. dom F ) -> ( F ` X ) = { y e. ( G ` Y ) | ps } ) )
30 3 4 29 mp2 
 |-  ( F ` X ) = { y e. ( G ` Y ) | ps }