Metamath Proof Explorer

Theorem k0004lem1

Description: Application of ssin to range of a function. (Contributed by RP, 1-Apr-2021)

Ref Expression
Assertion k0004lem1 
|- ( D = ( B i^i C ) -> ( ( F : A --> B /\ ( F " A ) C_ C ) <-> F : A --> D ) )

Proof

Step Hyp Ref Expression
1 fnima 
 |-  ( F Fn A -> ( F " A ) = ran F )
2 1 sseq1d 
 |-  ( F Fn A -> ( ( F " A ) C_ C <-> ran F C_ C ) )
3 2 anbi2d 
 |-  ( F Fn A -> ( ( ran F C_ B /\ ( F " A ) C_ C ) <-> ( ran F C_ B /\ ran F C_ C ) ) )
4 ssin 
 |-  ( ( ran F C_ B /\ ran F C_ C ) <-> ran F C_ ( B i^i C ) )
5 3 4 bitrdi 
 |-  ( F Fn A -> ( ( ran F C_ B /\ ( F " A ) C_ C ) <-> ran F C_ ( B i^i C ) ) )
6 5 pm5.32i 
 |-  ( ( F Fn A /\ ( ran F C_ B /\ ( F " A ) C_ C ) ) <-> ( F Fn A /\ ran F C_ ( B i^i C ) ) )
7 df-f 
 |-  ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
8 7 anbi1i 
 |-  ( ( F : A --> B /\ ( F " A ) C_ C ) <-> ( ( F Fn A /\ ran F C_ B ) /\ ( F " A ) C_ C ) )
9 anass 
 |-  ( ( ( F Fn A /\ ran F C_ B ) /\ ( F " A ) C_ C ) <-> ( F Fn A /\ ( ran F C_ B /\ ( F " A ) C_ C ) ) )
10 8 9 bitri 
 |-  ( ( F : A --> B /\ ( F " A ) C_ C ) <-> ( F Fn A /\ ( ran F C_ B /\ ( F " A ) C_ C ) ) )
11 df-f 
 |-  ( F : A --> ( B i^i C ) <-> ( F Fn A /\ ran F C_ ( B i^i C ) ) )
12 6 10 11 3bitr4i 
 |-  ( ( F : A --> B /\ ( F " A ) C_ C ) <-> F : A --> ( B i^i C ) )
13 feq3 
 |-  ( D = ( B i^i C ) -> ( F : A --> D <-> F : A --> ( B i^i C ) ) )
14 12 13 bitr4id 
 |-  ( D = ( B i^i C ) -> ( ( F : A --> B /\ ( F " A ) C_ C ) <-> F : A --> D ) )