Metamath Proof Explorer

Theorem fvmptss

Description: If all the values of the mapping are subsets of a class C , then so is any evaluation of the mapping, even if D is not in the base set A . (Contributed by Mario Carneiro, 13-Feb-2015)

Ref Expression
Hypothesis mptrcl.1 
|- F = ( x e. A |-> B )
Assertion fvmptss 
|- ( A. x e. A B C_ C -> ( F ` D ) C_ C )

Proof

Step Hyp Ref Expression
1 mptrcl.1 
 |-  F = ( x e. A |-> B )
2 1 dmmptss 
 |-  dom F C_ A
3 2 sseli 
 |-  ( D e. dom F -> D e. A )
4 fveq2 
 |-  ( y = D -> ( F ` y ) = ( F ` D ) )
5 4 sseq1d 
 |-  ( y = D -> ( ( F ` y ) C_ C <-> ( F ` D ) C_ C ) )
6 5 imbi2d 
 |-  ( y = D -> ( ( A. x e. A B C_ C -> ( F ` y ) C_ C ) <-> ( A. x e. A B C_ C -> ( F ` D ) C_ C ) ) )
7 nfcv 
 |-  F/_ x y
8 nfra1 
 |-  F/ x A. x e. A B C_ C
9 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
10 1 9 nfcxfr 
 |-  F/_ x F
11 10 7 nffv 
 |-  F/_ x ( F ` y )
12 nfcv 
 |-  F/_ x C
13 11 12 nfss 
 |-  F/ x ( F ` y ) C_ C
14 8 13 nfim 
 |-  F/ x ( A. x e. A B C_ C -> ( F ` y ) C_ C )
15 fveq2 
 |-  ( x = y -> ( F ` x ) = ( F ` y ) )
16 15 sseq1d 
 |-  ( x = y -> ( ( F ` x ) C_ C <-> ( F ` y ) C_ C ) )
17 16 imbi2d 
 |-  ( x = y -> ( ( A. x e. A B C_ C -> ( F ` x ) C_ C ) <-> ( A. x e. A B C_ C -> ( F ` y ) C_ C ) ) )
18 1 dmmpt 
 |-  dom F = { x e. A | B e. _V }
19 18 reqabi 
 |-  ( x e. dom F <-> ( x e. A /\ B e. _V ) )
20 1 fvmpt2 
 |-  ( ( x e. A /\ B e. _V ) -> ( F ` x ) = B )
21 eqimss 
 |-  ( ( F ` x ) = B -> ( F ` x ) C_ B )
22 20 21 syl 
 |-  ( ( x e. A /\ B e. _V ) -> ( F ` x ) C_ B )
23 19 22 sylbi 
 |-  ( x e. dom F -> ( F ` x ) C_ B )
24 ndmfv 
 |-  ( -. x e. dom F -> ( F ` x ) = (/) )
25 0ss 
 |-  (/) C_ B
26 24 25 eqsstrdi 
 |-  ( -. x e. dom F -> ( F ` x ) C_ B )
27 23 26 pm2.61i 
 |-  ( F ` x ) C_ B
28 rsp 
 |-  ( A. x e. A B C_ C -> ( x e. A -> B C_ C ) )
29 28 impcom 
 |-  ( ( x e. A /\ A. x e. A B C_ C ) -> B C_ C )
30 27 29 sstrid 
 |-  ( ( x e. A /\ A. x e. A B C_ C ) -> ( F ` x ) C_ C )
31 30 ex 
 |-  ( x e. A -> ( A. x e. A B C_ C -> ( F ` x ) C_ C ) )
32 7 14 17 31 vtoclgaf 
 |-  ( y e. A -> ( A. x e. A B C_ C -> ( F ` y ) C_ C ) )
33 6 32 vtoclga 
 |-  ( D e. A -> ( A. x e. A B C_ C -> ( F ` D ) C_ C ) )
34 33 impcom 
 |-  ( ( A. x e. A B C_ C /\ D e. A ) -> ( F ` D ) C_ C )
35 3 34 sylan2 
 |-  ( ( A. x e. A B C_ C /\ D e. dom F ) -> ( F ` D ) C_ C )
36 ndmfv 
 |-  ( -. D e. dom F -> ( F ` D ) = (/) )
37 36 adantl 
 |-  ( ( A. x e. A B C_ C /\ -. D e. dom F ) -> ( F ` D ) = (/) )
38 0ss 
 |-  (/) C_ C
39 37 38 eqsstrdi 
 |-  ( ( A. x e. A B C_ C /\ -. D e. dom F ) -> ( F ` D ) C_ C )
40 35 39 pm2.61dan 
 |-  ( A. x e. A B C_ C -> ( F ` D ) C_ C )