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

Metamath Proof Explorer

Theorem wdomima2g

Description: A set is weakly dominant over its image under any function. This version of wdomimag is stated so as to avoid ax-rep . (Contributed by Mario Carneiro, 25-Jun-2015)

Ref Expression
Assertion wdomima2g 
|- ( ( Fun F /\ A e. V /\ ( F " A ) e. W ) -> ( F " A ) ~<_* A )

Proof

Step Hyp Ref Expression
1 df-ima 
 |-  ( F " A ) = ran ( F |` A )
2 funres 
 |-  ( Fun F -> Fun ( F |` A ) )
3 funforn 
 |-  ( Fun ( F |` A ) <-> ( F |` A ) : dom ( F |` A ) -onto-> ran ( F |` A ) )
4 2 3 sylib 
 |-  ( Fun F -> ( F |` A ) : dom ( F |` A ) -onto-> ran ( F |` A ) )
5 4 3ad2ant1 
 |-  ( ( Fun F /\ A e. V /\ ( F " A ) e. W ) -> ( F |` A ) : dom ( F |` A ) -onto-> ran ( F |` A ) )
6 fof 
 |-  ( ( F |` A ) : dom ( F |` A ) -onto-> ran ( F |` A ) -> ( F |` A ) : dom ( F |` A ) --> ran ( F |` A ) )
7 5 6 syl 
 |-  ( ( Fun F /\ A e. V /\ ( F " A ) e. W ) -> ( F |` A ) : dom ( F |` A ) --> ran ( F |` A ) )
8 dmres 
 |-  dom ( F |` A ) = ( A i^i dom F )
9 inss1 
 |-  ( A i^i dom F ) C_ A
10 8 9 eqsstri 
 |-  dom ( F |` A ) C_ A
11 simp2 
 |-  ( ( Fun F /\ A e. V /\ ( F " A ) e. W ) -> A e. V )
12 ssexg 
 |-  ( ( dom ( F |` A ) C_ A /\ A e. V ) -> dom ( F |` A ) e. _V )
13 10 11 12 sylancr 
 |-  ( ( Fun F /\ A e. V /\ ( F " A ) e. W ) -> dom ( F |` A ) e. _V )
14 simp3 
 |-  ( ( Fun F /\ A e. V /\ ( F " A ) e. W ) -> ( F " A ) e. W )
15 1 14 eqeltrrid 
 |-  ( ( Fun F /\ A e. V /\ ( F " A ) e. W ) -> ran ( F |` A ) e. W )
16 fex2 
 |-  ( ( ( F |` A ) : dom ( F |` A ) --> ran ( F |` A ) /\ dom ( F |` A ) e. _V /\ ran ( F |` A ) e. W ) -> ( F |` A ) e. _V )
17 7 13 15 16 syl3anc 
 |-  ( ( Fun F /\ A e. V /\ ( F " A ) e. W ) -> ( F |` A ) e. _V )
18 fowdom 
 |-  ( ( ( F |` A ) e. _V /\ ( F |` A ) : dom ( F |` A ) -onto-> ran ( F |` A ) ) -> ran ( F |` A ) ~<_* dom ( F |` A ) )
19 17 5 18 syl2anc 
 |-  ( ( Fun F /\ A e. V /\ ( F " A ) e. W ) -> ran ( F |` A ) ~<_* dom ( F |` A ) )
20 ssdomg 
 |-  ( A e. V -> ( dom ( F |` A ) C_ A -> dom ( F |` A ) ~<_ A ) )
21 10 20 mpi 
 |-  ( A e. V -> dom ( F |` A ) ~<_ A )
22 domwdom 
 |-  ( dom ( F |` A ) ~<_ A -> dom ( F |` A ) ~<_* A )
23 21 22 syl 
 |-  ( A e. V -> dom ( F |` A ) ~<_* A )
24 23 3ad2ant2 
 |-  ( ( Fun F /\ A e. V /\ ( F " A ) e. W ) -> dom ( F |` A ) ~<_* A )
25 wdomtr 
 |-  ( ( ran ( F |` A ) ~<_* dom ( F |` A ) /\ dom ( F |` A ) ~<_* A ) -> ran ( F |` A ) ~<_* A )
26 19 24 25 syl2anc 
 |-  ( ( Fun F /\ A e. V /\ ( F " A ) e. W ) -> ran ( F |` A ) ~<_* A )
27 1 26 eqbrtrid 
 |-  ( ( Fun F /\ A e. V /\ ( F " A ) e. W ) -> ( F " A ) ~<_* A )