Metamath Proof Explorer

Theorem f1imass

Description: Taking images under a one-to-one function preserves subsets. (Contributed by Stefan O'Rear, 30-Oct-2014)

Ref Expression
Assertion f1imass 
|- ( ( F : A -1-1-> B /\ ( C C_ A /\ D C_ A ) ) -> ( ( F " C ) C_ ( F " D ) <-> C C_ D ) )

Proof

Step Hyp Ref Expression
1 simplrl 
 |-  ( ( ( F : A -1-1-> B /\ ( C C_ A /\ D C_ A ) ) /\ ( F " C ) C_ ( F " D ) ) -> C C_ A )
2 1 sseld 
 |-  ( ( ( F : A -1-1-> B /\ ( C C_ A /\ D C_ A ) ) /\ ( F " C ) C_ ( F " D ) ) -> ( a e. C -> a e. A ) )
3 simplr 
 |-  ( ( ( ( F : A -1-1-> B /\ ( C C_ A /\ D C_ A ) ) /\ ( F " C ) C_ ( F " D ) ) /\ a e. A ) -> ( F " C ) C_ ( F " D ) )
4 3 sseld 
 |-  ( ( ( ( F : A -1-1-> B /\ ( C C_ A /\ D C_ A ) ) /\ ( F " C ) C_ ( F " D ) ) /\ a e. A ) -> ( ( F ` a ) e. ( F " C ) -> ( F ` a ) e. ( F " D ) ) )
5 simplll 
 |-  ( ( ( ( F : A -1-1-> B /\ ( C C_ A /\ D C_ A ) ) /\ ( F " C ) C_ ( F " D ) ) /\ a e. A ) -> F : A -1-1-> B )
6 simpr 
 |-  ( ( ( ( F : A -1-1-> B /\ ( C C_ A /\ D C_ A ) ) /\ ( F " C ) C_ ( F " D ) ) /\ a e. A ) -> a e. A )
7 simp1rl 
 |-  ( ( ( F : A -1-1-> B /\ ( C C_ A /\ D C_ A ) ) /\ ( F " C ) C_ ( F " D ) /\ a e. A ) -> C C_ A )
8 7 3expa 
 |-  ( ( ( ( F : A -1-1-> B /\ ( C C_ A /\ D C_ A ) ) /\ ( F " C ) C_ ( F " D ) ) /\ a e. A ) -> C C_ A )
9 f1elima 
 |-  ( ( F : A -1-1-> B /\ a e. A /\ C C_ A ) -> ( ( F ` a ) e. ( F " C ) <-> a e. C ) )
10 5 6 8 9 syl3anc 
 |-  ( ( ( ( F : A -1-1-> B /\ ( C C_ A /\ D C_ A ) ) /\ ( F " C ) C_ ( F " D ) ) /\ a e. A ) -> ( ( F ` a ) e. ( F " C ) <-> a e. C ) )
11 simp1rr 
 |-  ( ( ( F : A -1-1-> B /\ ( C C_ A /\ D C_ A ) ) /\ ( F " C ) C_ ( F " D ) /\ a e. A ) -> D C_ A )
12 11 3expa 
 |-  ( ( ( ( F : A -1-1-> B /\ ( C C_ A /\ D C_ A ) ) /\ ( F " C ) C_ ( F " D ) ) /\ a e. A ) -> D C_ A )
13 f1elima 
 |-  ( ( F : A -1-1-> B /\ a e. A /\ D C_ A ) -> ( ( F ` a ) e. ( F " D ) <-> a e. D ) )
14 5 6 12 13 syl3anc 
 |-  ( ( ( ( F : A -1-1-> B /\ ( C C_ A /\ D C_ A ) ) /\ ( F " C ) C_ ( F " D ) ) /\ a e. A ) -> ( ( F ` a ) e. ( F " D ) <-> a e. D ) )
15 4 10 14 3imtr3d 
 |-  ( ( ( ( F : A -1-1-> B /\ ( C C_ A /\ D C_ A ) ) /\ ( F " C ) C_ ( F " D ) ) /\ a e. A ) -> ( a e. C -> a e. D ) )
16 15 ex 
 |-  ( ( ( F : A -1-1-> B /\ ( C C_ A /\ D C_ A ) ) /\ ( F " C ) C_ ( F " D ) ) -> ( a e. A -> ( a e. C -> a e. D ) ) )
17 2 16 syld 
 |-  ( ( ( F : A -1-1-> B /\ ( C C_ A /\ D C_ A ) ) /\ ( F " C ) C_ ( F " D ) ) -> ( a e. C -> ( a e. C -> a e. D ) ) )
18 17 pm2.43d 
 |-  ( ( ( F : A -1-1-> B /\ ( C C_ A /\ D C_ A ) ) /\ ( F " C ) C_ ( F " D ) ) -> ( a e. C -> a e. D ) )
19 18 ssrdv 
 |-  ( ( ( F : A -1-1-> B /\ ( C C_ A /\ D C_ A ) ) /\ ( F " C ) C_ ( F " D ) ) -> C C_ D )
20 19 ex 
 |-  ( ( F : A -1-1-> B /\ ( C C_ A /\ D C_ A ) ) -> ( ( F " C ) C_ ( F " D ) -> C C_ D ) )
21 imass2 
 |-  ( C C_ D -> ( F " C ) C_ ( F " D ) )
22 20 21 impbid1 
 |-  ( ( F : A -1-1-> B /\ ( C C_ A /\ D C_ A ) ) -> ( ( F " C ) C_ ( F " D ) <-> C C_ D ) )