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 ) )