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

Metamath Proof Explorer

Theorem mptelpm

Description: A function in maps-to notation is a partial map . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses mptelpm.b 
|- ( ( ph /\ x e. A ) -> B e. C )
mptelpm.a 
|- ( ph -> A C_ D )
mptelpm.c 
|- ( ph -> C e. V )
mptelpm.d 
|- ( ph -> D e. W )
Assertion mptelpm 
|- ( ph -> ( x e. A |-> B ) e. ( C ^pm D ) )

Proof

Step Hyp Ref Expression
1 mptelpm.b 
 |-  ( ( ph /\ x e. A ) -> B e. C )
2 mptelpm.a 
 |-  ( ph -> A C_ D )
3 mptelpm.c 
 |-  ( ph -> C e. V )
4 mptelpm.d 
 |-  ( ph -> D e. W )
5 1 fmpttd 
 |-  ( ph -> ( x e. A |-> B ) : A --> C )
6 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
7 6 1 dmmptd 
 |-  ( ph -> dom ( x e. A |-> B ) = A )
8 7 eqcomd 
 |-  ( ph -> A = dom ( x e. A |-> B ) )
9 8 feq2d 
 |-  ( ph -> ( ( x e. A |-> B ) : A --> C <-> ( x e. A |-> B ) : dom ( x e. A |-> B ) --> C ) )
10 5 9 mpbid 
 |-  ( ph -> ( x e. A |-> B ) : dom ( x e. A |-> B ) --> C )
11 7 2 eqsstrd 
 |-  ( ph -> dom ( x e. A |-> B ) C_ D )
12 10 11 jca 
 |-  ( ph -> ( ( x e. A |-> B ) : dom ( x e. A |-> B ) --> C /\ dom ( x e. A |-> B ) C_ D ) )
13 elpm2g 
 |-  ( ( C e. V /\ D e. W ) -> ( ( x e. A |-> B ) e. ( C ^pm D ) <-> ( ( x e. A |-> B ) : dom ( x e. A |-> B ) --> C /\ dom ( x e. A |-> B ) C_ D ) ) )
14 3 4 13 syl2anc 
 |-  ( ph -> ( ( x e. A |-> B ) e. ( C ^pm D ) <-> ( ( x e. A |-> B ) : dom ( x e. A |-> B ) --> C /\ dom ( x e. A |-> B ) C_ D ) ) )
15 12 14 mpbird 
 |-  ( ph -> ( x e. A |-> B ) e. ( C ^pm D ) )