Metamath Proof Explorer

Theorem pmresg

Description: Elementhood of a restricted function in the set of partial functions. (Contributed by Mario Carneiro, 31-Dec-2013)

Ref Expression
Assertion pmresg 
|- ( ( B e. V /\ F e. ( A ^pm C ) ) -> ( F |` B ) e. ( A ^pm B ) )

Proof

Step Hyp Ref Expression
1 n0i 
 |-  ( F e. ( A ^pm C ) -> -. ( A ^pm C ) = (/) )
2 fnpm 
 |-  ^pm Fn ( _V X. _V )
3 2 fndmi 
 |-  dom ^pm = ( _V X. _V )
4 3 ndmov 
 |-  ( -. ( A e. _V /\ C e. _V ) -> ( A ^pm C ) = (/) )
5 1 4 nsyl2 
 |-  ( F e. ( A ^pm C ) -> ( A e. _V /\ C e. _V ) )
6 5 simpld 
 |-  ( F e. ( A ^pm C ) -> A e. _V )
7 6 adantl 
 |-  ( ( B e. V /\ F e. ( A ^pm C ) ) -> A e. _V )
8 simpl 
 |-  ( ( B e. V /\ F e. ( A ^pm C ) ) -> B e. V )
9 elpmi 
 |-  ( F e. ( A ^pm C ) -> ( F : dom F --> A /\ dom F C_ C ) )
10 9 simpld 
 |-  ( F e. ( A ^pm C ) -> F : dom F --> A )
11 10 adantl 
 |-  ( ( B e. V /\ F e. ( A ^pm C ) ) -> F : dom F --> A )
12 inss1 
 |-  ( dom F i^i B ) C_ dom F
13 fssres 
 |-  ( ( F : dom F --> A /\ ( dom F i^i B ) C_ dom F ) -> ( F |` ( dom F i^i B ) ) : ( dom F i^i B ) --> A )
14 11 12 13 sylancl 
 |-  ( ( B e. V /\ F e. ( A ^pm C ) ) -> ( F |` ( dom F i^i B ) ) : ( dom F i^i B ) --> A )
15 ffun 
 |-  ( F : dom F --> A -> Fun F )
16 resres 
 |-  ( ( F |` dom F ) |` B ) = ( F |` ( dom F i^i B ) )
17 funrel 
 |-  ( Fun F -> Rel F )
18 resdm 
 |-  ( Rel F -> ( F |` dom F ) = F )
19 reseq1 
 |-  ( ( F |` dom F ) = F -> ( ( F |` dom F ) |` B ) = ( F |` B ) )
20 17 18 19 3syl 
 |-  ( Fun F -> ( ( F |` dom F ) |` B ) = ( F |` B ) )
21 16 20 eqtr3id 
 |-  ( Fun F -> ( F |` ( dom F i^i B ) ) = ( F |` B ) )
22 11 15 21 3syl 
 |-  ( ( B e. V /\ F e. ( A ^pm C ) ) -> ( F |` ( dom F i^i B ) ) = ( F |` B ) )
23 22 feq1d 
 |-  ( ( B e. V /\ F e. ( A ^pm C ) ) -> ( ( F |` ( dom F i^i B ) ) : ( dom F i^i B ) --> A <-> ( F |` B ) : ( dom F i^i B ) --> A ) )
24 14 23 mpbid 
 |-  ( ( B e. V /\ F e. ( A ^pm C ) ) -> ( F |` B ) : ( dom F i^i B ) --> A )
25 inss2 
 |-  ( dom F i^i B ) C_ B
26 elpm2r 
 |-  ( ( ( A e. _V /\ B e. V ) /\ ( ( F |` B ) : ( dom F i^i B ) --> A /\ ( dom F i^i B ) C_ B ) ) -> ( F |` B ) e. ( A ^pm B ) )
27 25 26 mpanr2 
 |-  ( ( ( A e. _V /\ B e. V ) /\ ( F |` B ) : ( dom F i^i B ) --> A ) -> ( F |` B ) e. ( A ^pm B ) )
28 7 8 24 27 syl21anc 
 |-  ( ( B e. V /\ F e. ( A ^pm C ) ) -> ( F |` B ) e. ( A ^pm B ) )