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