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 )