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	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐶 )
	mptelpm.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝐷 )
	mptelpm.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
	mptelpm.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
Assertion	mptelpm	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( 𝐶 ↑pm 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		mptelpm.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐶 )
2		mptelpm.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝐷 )
3		mptelpm.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
4		mptelpm.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
5	1	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ 𝐶 )
6		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
7	6 1	dmmptd	⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
8	7	eqcomd	⊢ ( 𝜑 → 𝐴 = dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
9	8	feq2d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ 𝐶 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⟶ 𝐶 ) )
10	5 9	mpbid	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⟶ 𝐶 )
11	7 2	eqsstrd	⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝐷 )
12	10 11	jca	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⟶ 𝐶 ∧ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝐷 ) )
13		elpm2g	⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( 𝐶 ↑pm 𝐷 ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⟶ 𝐶 ∧ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝐷 ) ) )
14	3 4 13	syl2anc	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( 𝐶 ↑pm 𝐷 ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⟶ 𝐶 ∧ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝐷 ) ) )
15	12 14	mpbird	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( 𝐶 ↑pm 𝐷 ) )