Metamath Proof Explorer

Theorem k0004lem2

Description: A mapping with a particular restricted range is also a mapping to that range. (Contributed by RP, 1-Apr-2021)

Ref Expression
Assertion k0004lem2 
|- ( ( A e. U /\ B e. V /\ C C_ B ) -> ( ( F e. ( B ^m A ) /\ ( F " A ) C_ C ) <-> F e. ( C ^m A ) ) )

Proof

Step Hyp Ref Expression
1 simp3 
 |-  ( ( A e. U /\ B e. V /\ C C_ B ) -> C C_ B )
2 sseqin2 
 |-  ( C C_ B <-> ( B i^i C ) = C )
3 2 biimpi 
 |-  ( C C_ B -> ( B i^i C ) = C )
4 3 eqcomd 
 |-  ( C C_ B -> C = ( B i^i C ) )
5 k0004lem1 
 |-  ( C = ( B i^i C ) -> ( ( F : A --> B /\ ( F " A ) C_ C ) <-> F : A --> C ) )
6 1 4 5 3syl 
 |-  ( ( A e. U /\ B e. V /\ C C_ B ) -> ( ( F : A --> B /\ ( F " A ) C_ C ) <-> F : A --> C ) )
7 simp2 
 |-  ( ( A e. U /\ B e. V /\ C C_ B ) -> B e. V )
8 simp1 
 |-  ( ( A e. U /\ B e. V /\ C C_ B ) -> A e. U )
9 7 8 elmapd 
 |-  ( ( A e. U /\ B e. V /\ C C_ B ) -> ( F e. ( B ^m A ) <-> F : A --> B ) )
10 9 anbi1d 
 |-  ( ( A e. U /\ B e. V /\ C C_ B ) -> ( ( F e. ( B ^m A ) /\ ( F " A ) C_ C ) <-> ( F : A --> B /\ ( F " A ) C_ C ) ) )
11 7 1 ssexd 
 |-  ( ( A e. U /\ B e. V /\ C C_ B ) -> C e. _V )
12 11 8 elmapd 
 |-  ( ( A e. U /\ B e. V /\ C C_ B ) -> ( F e. ( C ^m A ) <-> F : A --> C ) )
13 6 10 12 3bitr4d 
 |-  ( ( A e. U /\ B e. V /\ C C_ B ) -> ( ( F e. ( B ^m A ) /\ ( F " A ) C_ C ) <-> F e. ( C ^m A ) ) )