This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem maprnin

Description: Restricting the range of the mapping operator. (Contributed by Thierry Arnoux, 30-Aug-2017)

Ref Expression
Hypotheses maprnin.1 
|- A e. _V
maprnin.2 
|- B e. _V
Assertion maprnin 
|- ( ( B i^i C ) ^m A ) = { f e. ( B ^m A ) | ran f C_ C }

Proof

Step Hyp Ref Expression
1 maprnin.1 
 |-  A e. _V
2 maprnin.2 
 |-  B e. _V
3 ffn 
 |-  ( f : A --> B -> f Fn A )
4 df-f 
 |-  ( f : A --> C <-> ( f Fn A /\ ran f C_ C ) )
5 4 baibr 
 |-  ( f Fn A -> ( ran f C_ C <-> f : A --> C ) )
6 3 5 syl 
 |-  ( f : A --> B -> ( ran f C_ C <-> f : A --> C ) )
7 6 pm5.32i 
 |-  ( ( f : A --> B /\ ran f C_ C ) <-> ( f : A --> B /\ f : A --> C ) )
8 2 1 elmap 
 |-  ( f e. ( B ^m A ) <-> f : A --> B )
9 8 anbi1i 
 |-  ( ( f e. ( B ^m A ) /\ ran f C_ C ) <-> ( f : A --> B /\ ran f C_ C ) )
10 fin 
 |-  ( f : A --> ( B i^i C ) <-> ( f : A --> B /\ f : A --> C ) )
11 7 9 10 3bitr4ri 
 |-  ( f : A --> ( B i^i C ) <-> ( f e. ( B ^m A ) /\ ran f C_ C ) )
12 11 abbii 
 |-  { f | f : A --> ( B i^i C ) } = { f | ( f e. ( B ^m A ) /\ ran f C_ C ) }
13 2 inex1 
 |-  ( B i^i C ) e. _V
14 13 1 mapval 
 |-  ( ( B i^i C ) ^m A ) = { f | f : A --> ( B i^i C ) }
15 df-rab 
 |-  { f e. ( B ^m A ) | ran f C_ C } = { f | ( f e. ( B ^m A ) /\ ran f C_ C ) }
16 12 14 15 3eqtr4i 
 |-  ( ( B i^i C ) ^m A ) = { f e. ( B ^m A ) | ran f C_ C }