Metamath Proof Explorer

Theorem elpm2r

Description: Sufficient condition for being a partial function. (Contributed by NM, 31-Dec-2013)

Ref Expression
Assertion elpm2r ⊢ A ∈ V ∧ B ∈ W ∧ F : C ⟶ A ∧ C ⊆ B → F ∈ A ↑ 𝑝𝑚 B

Proof

Step Hyp Ref Expression
1 fdm ⊢ F : C ⟶ A → dom ⁡ F = C
2 1 feq2d ⊢ F : C ⟶ A → F : dom ⁡ F ⟶ A ↔ F : C ⟶ A
3 1 sseq1d ⊢ F : C ⟶ A → dom ⁡ F ⊆ B ↔ C ⊆ B
4 2 3 anbi12d ⊢ F : C ⟶ A → F : dom ⁡ F ⟶ A ∧ dom ⁡ F ⊆ B ↔ F : C ⟶ A ∧ C ⊆ B
5 4 adantr ⊢ F : C ⟶ A ∧ C ⊆ B → F : dom ⁡ F ⟶ A ∧ dom ⁡ F ⊆ B ↔ F : C ⟶ A ∧ C ⊆ B
6 5 ibir ⊢ F : C ⟶ A ∧ C ⊆ B → F : dom ⁡ F ⟶ A ∧ dom ⁡ F ⊆ B
7 elpm2g ⊢ A ∈ V ∧ B ∈ W → F ∈ A ↑ 𝑝𝑚 B ↔ F : dom ⁡ F ⟶ A ∧ dom ⁡ F ⊆ B
8 6 7 syl5ibr ⊢ A ∈ V ∧ B ∈ W → F : C ⟶ A ∧ C ⊆ B → F ∈ A ↑ 𝑝𝑚 B
9 8 imp ⊢ A ∈ V ∧ B ∈ W ∧ F : C ⟶ A ∧ C ⊆ B → F ∈ A ↑ 𝑝𝑚 B