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 φ x A B C
mptelpm.a φ A D
mptelpm.c φ C V
mptelpm.d φ D W
Assertion mptelpm φ x A B C 𝑝𝑚 D

Proof

Step Hyp Ref Expression
1 mptelpm.b φ x A B C
2 mptelpm.a φ A D
3 mptelpm.c φ C V
4 mptelpm.d φ D W
5 1 fmpttd φ x A B : A C
6 eqid x A B = x A B
7 6 1 dmmptd φ dom x A B = A
8 7 eqcomd φ A = dom x A B
9 8 feq2d φ x A B : A C x A B : dom x A B C
10 5 9 mpbid φ x A B : dom x A B C
11 7 2 eqsstrd φ dom x A B D
12 10 11 jca φ x A B : dom x A B C dom x A B D
13 elpm2g C V D W x A B C 𝑝𝑚 D x A B : dom x A B C dom x A B D
14 3 4 13 syl2anc φ x A B C 𝑝𝑚 D x A B : dom x A B C dom x A B D
15 12 14 mpbird φ x A B C 𝑝𝑚 D