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 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐶 )
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 𝐷 ) )