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