Metamath Proof Explorer

Theorem imasless

Description: The order relation defined on an image set is a subset of the base set. (Contributed by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypotheses imasless.u 
|- ( ph -> U = ( F "s R ) )
imasless.v 
|- ( ph -> V = ( Base ` R ) )
imasless.f 
|- ( ph -> F : V -onto-> B )
imasless.r 
|- ( ph -> R e. Z )
imasless.l 
|- .<_ = ( le ` U )
Assertion imasless 
|- ( ph -> .<_ C_ ( B X. B ) )

Proof

Step Hyp Ref Expression
1 imasless.u 
 |-  ( ph -> U = ( F "s R ) )
2 imasless.v 
 |-  ( ph -> V = ( Base ` R ) )
3 imasless.f 
 |-  ( ph -> F : V -onto-> B )
4 imasless.r 
 |-  ( ph -> R e. Z )
5 imasless.l 
 |-  .<_ = ( le ` U )
6 eqid 
 |-  ( le ` R ) = ( le ` R )
7 1 2 3 4 6 5 imasle 
 |-  ( ph -> .<_ = ( ( F o. ( le ` R ) ) o. `' F ) )
8 relco 
 |-  Rel ( ( F o. ( le ` R ) ) o. `' F )
9 relssdmrn 
 |-  ( Rel ( ( F o. ( le ` R ) ) o. `' F ) -> ( ( F o. ( le ` R ) ) o. `' F ) C_ ( dom ( ( F o. ( le ` R ) ) o. `' F ) X. ran ( ( F o. ( le ` R ) ) o. `' F ) ) )
10 8 9 ax-mp 
 |-  ( ( F o. ( le ` R ) ) o. `' F ) C_ ( dom ( ( F o. ( le ` R ) ) o. `' F ) X. ran ( ( F o. ( le ` R ) ) o. `' F ) )
11 dmco 
 |-  dom ( ( F o. ( le ` R ) ) o. `' F ) = ( `' `' F " dom ( F o. ( le ` R ) ) )
12 fof 
 |-  ( F : V -onto-> B -> F : V --> B )
13 frel 
 |-  ( F : V --> B -> Rel F )
14 3 12 13 3syl 
 |-  ( ph -> Rel F )
15 dfrel2 
 |-  ( Rel F <-> `' `' F = F )
16 14 15 sylib 
 |-  ( ph -> `' `' F = F )
17 16 imaeq1d 
 |-  ( ph -> ( `' `' F " dom ( F o. ( le ` R ) ) ) = ( F " dom ( F o. ( le ` R ) ) ) )
18 imassrn 
 |-  ( F " dom ( F o. ( le ` R ) ) ) C_ ran F
19 forn 
 |-  ( F : V -onto-> B -> ran F = B )
20 3 19 syl 
 |-  ( ph -> ran F = B )
21 18 20 sseqtrid 
 |-  ( ph -> ( F " dom ( F o. ( le ` R ) ) ) C_ B )
22 17 21 eqsstrd 
 |-  ( ph -> ( `' `' F " dom ( F o. ( le ` R ) ) ) C_ B )
23 11 22 eqsstrid 
 |-  ( ph -> dom ( ( F o. ( le ` R ) ) o. `' F ) C_ B )
24 rncoss 
 |-  ran ( ( F o. ( le ` R ) ) o. `' F ) C_ ran ( F o. ( le ` R ) )
25 rnco2 
 |-  ran ( F o. ( le ` R ) ) = ( F " ran ( le ` R ) )
26 imassrn 
 |-  ( F " ran ( le ` R ) ) C_ ran F
27 26 20 sseqtrid 
 |-  ( ph -> ( F " ran ( le ` R ) ) C_ B )
28 25 27 eqsstrid 
 |-  ( ph -> ran ( F o. ( le ` R ) ) C_ B )
29 24 28 sstrid 
 |-  ( ph -> ran ( ( F o. ( le ` R ) ) o. `' F ) C_ B )
30 xpss12 
 |-  ( ( dom ( ( F o. ( le ` R ) ) o. `' F ) C_ B /\ ran ( ( F o. ( le ` R ) ) o. `' F ) C_ B ) -> ( dom ( ( F o. ( le ` R ) ) o. `' F ) X. ran ( ( F o. ( le ` R ) ) o. `' F ) ) C_ ( B X. B ) )
31 23 29 30 syl2anc 
 |-  ( ph -> ( dom ( ( F o. ( le ` R ) ) o. `' F ) X. ran ( ( F o. ( le ` R ) ) o. `' F ) ) C_ ( B X. B ) )
32 10 31 sstrid 
 |-  ( ph -> ( ( F o. ( le ` R ) ) o. `' F ) C_ ( B X. B ) )
33 7 32 eqsstrd 
 |-  ( ph -> .<_ C_ ( B X. B ) )