This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fvmptss2

Description: A mapping always evaluates to a subset of the substituted expression in the mapping, even if this is a proper class, or we are out of the domain. (Contributed by Mario Carneiro, 13-Feb-2015)

Ref Expression
Hypotheses fvmptn.1 
|- ( x = D -> B = C )
fvmptn.2 
|- F = ( x e. A |-> B )
Assertion fvmptss2 
|- ( F ` D ) C_ C

Proof

Step Hyp Ref Expression
1 fvmptn.1 
 |-  ( x = D -> B = C )
2 fvmptn.2 
 |-  F = ( x e. A |-> B )
3 1 eleq1d 
 |-  ( x = D -> ( B e. _V <-> C e. _V ) )
4 2 dmmpt 
 |-  dom F = { x e. A | B e. _V }
5 3 4 elrab2 
 |-  ( D e. dom F <-> ( D e. A /\ C e. _V ) )
6 1 2 fvmptg 
 |-  ( ( D e. A /\ C e. _V ) -> ( F ` D ) = C )
7 eqimss 
 |-  ( ( F ` D ) = C -> ( F ` D ) C_ C )
8 6 7 syl 
 |-  ( ( D e. A /\ C e. _V ) -> ( F ` D ) C_ C )
9 5 8 sylbi 
 |-  ( D e. dom F -> ( F ` D ) C_ C )
10 ndmfv 
 |-  ( -. D e. dom F -> ( F ` D ) = (/) )
11 0ss 
 |-  (/) C_ C
12 10 11 eqsstrdi 
 |-  ( -. D e. dom F -> ( F ` D ) C_ C )
13 9 12 pm2.61i 
 |-  ( F ` D ) C_ C